MellinConvolutionTransform

@[blueprint  (title := "MellinConvolutionTransform")  (statement := /--  Let $f$ and $g$ be functions from $\mathbb{R}_{>0}$ to $\mathbb{C}$ such that  \begin{equation}    (x,y)\mapsto f(y)\frac{g(x/y)}yx^{s-1}    \label{eq:assm_integrable_Mconv}  \end{equation}  is absolutely integrable on $[0,\infty)^2$.  Then  $$\mathcal{M}(f\ast g)(s) = \mathcal{M}(f)(s)\mathcal{M}(g)(s).$$  -/)  (proof := /--  By Definitions \ref{MellinTransform} and \ref{MellinConvolution}  $$    \mathcal M(f\ast g)(s)=    \int_0^\infty \int_0^\infty f(y)g(x/y)x^{s-1}\frac{dy}ydx  $$  By (\ref{eq:assm_integrable_Mconv}) and Fubini's theorem,  $$    \mathcal M(f\ast g)(s)=    \int_0^\infty \int_0^\infty f(y)g(x/y)x^{s-1}dx\frac{dy}y  $$  in which we change variables from $x$ to $z=x/y$:  $$    \mathcal M(f\ast g)(s)=    \int_0^\infty \int_0^\infty f(y)g(z)y^{s-1}z^{s-1}dzdy  $$  which, by Definition \ref{MellinTransform}, is  $$    \mathcal M(f\ast g)(s)=    \mathcal M(f)(s)\mathcal M(g)(s)    .  $$  -/)]lemma MellinConvolutionTransform (f g : ℝ → ℂ) (s : ℂ)    (hf : IntegrableOn (fun x y ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)).uncurry      (Ioi 0 ×ˢ Ioi 0)) :    𝓜 (MellinConvolution f g) s = 𝓜 f s * 𝓜 g s := by  dsimp [mellin, MellinConvolution]  set f₁ : ℝ × ℝ → ℂ :=    fun ⟨x, y⟩ ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)  calc    _ = ∫ (x : ℝ) in Ioi 0, ∫ (y : ℝ) in Ioi 0, f₁ (x, y) := ?_    _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f₁ (x, y) :=        setIntegral_integral_swap _ hf    _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0,        f y * g (x / y) / ↑y * ↑x ^ (s - 1) := rfl    _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0,        f y * g (x * y / y) / ↑y * ↑(x * y) ^ (s - 1) * y := ?_    _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0,        f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) := ?_    _ = ∫ (y : ℝ) in Ioi 0,        f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1) := ?_    _ = _ := integral_mul_const _ _  <;> try (rw [setIntegral_congr_fun (by simp)]; intro y hy; simp only [ofReal_mul])  · simp only [integral_mul_const, f₁, mul_comm]  · simp only [integral_mul_const]    have := integral_comp_mul_right_Ioi      (fun x ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)) 0 hy    have y_ne_zeroℂ : (y : ℂ) ≠ 0 := slitPlane_ne_zero (Or.inl hy)    field_simp at this ⊢    simp only [ofReal_mul, one_div, mul_zero, real_smul, ofReal_inv, field] at this ⊢    rw [← this]    field_simp    congr with x    ring_nf  · rw [setIntegral_congr_fun (by simp)]    intro x hx    have y_ne_zeroℝ : y ≠ 0 := ne_of_gt (mem_Ioi.mp hy)    have y_ne_zeroℂ : (y : ℂ) ≠ 0 := by exact_mod_cast y_ne_zeroℝ    field_simp    rw [mul_cpow_ofReal_nonneg hy.le hx.le]    ring  · apply integral_const_mul  · congr <;> ext <;> ring