Mellin Convolution Symmetric

@[blueprint  (title := "MellinConvolutionSymmetric")  (statement := /--  Let $f$ and $g$ be functions from $\mathbb{R}_{>0}$ to $\mathbb{R}$ or $\mathbb{C}$, for $x\neq0$,  $$    (f\ast g)(x)=(g\ast f)(x)    .  $$  -/)  (proof := /--  By Definition \ref{MellinConvolution},  $$    (f\ast g)(x) = \int_0^\infty f(y)g(x/y)\frac{dy}{y}  $$  in which we change variables to $z=x/y$:  $$    (f\ast g)(x) = \int_0^\infty f(x/z)g(z)\frac{dz}{z}    =(g\ast f)(x)    .  $$  -/)  (latexEnv := "lemma")]lemma MellinConvolutionSymmetric (f g : ℝ → 𝕂) {x : ℝ} (xpos : 0 < x) :    MellinConvolution f g x = MellinConvolution g f x := by  unfold MellinConvolution  calc    _ = ∫ y in Ioi 0, f (y * x) * g (1 / y) / y := ?_    _ = _ := ?_  · rw [← integral_comp_mul_right_I0i_haar (fun y ↦ f y * g (x / y)) xpos]    simp [div_mul_cancel_right₀ <| ne_of_gt xpos]  · convert (integral_comp_inv_I0i_haar fun y ↦ f (y * x) * g (1 / y)).symm using 3    rw [one_div_one_div, mul_comm, mul_comm_div, one_mul]