Mellin inversion formula

We derive the Mellin inversion formula as a consequence of the Fourier inversion formula.

Main results

• mellin_inversion: The inverse Mellin transform of the Mellin transform applied to x > 0 is x.

theorem mellin_eq_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) {s : ℂ} : mellin f s = Real.fourierIntegral (fun (u : ℝ) => Real.exp (-s.re * u) • f (Real.exp (-u))) (s.im / (2 * Real.pi))

theorem mellinInv_eq_fourierIntegralInv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (σ : ℝ) (f : ℂ → E) {x : ℝ} (hx : 0 < x) : mellinInv σ f x = ↑x ^ (-↑σ) • Real.fourierIntegralInv (fun (y : ℝ) => f (↑σ + 2 * ↑Real.pi * ↑y * Complex.I)) (-Real.log x)

theorem mellin_inversion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (σ : ℝ) (f : ℝ → E) {x : ℝ} (hx : 0 < x) (hf : MellinConvergent f ↑σ) (hFf : Complex.VerticalIntegrable (mellin f) σ MeasureTheory.volume) (hfx : ContinuousAt f x) : mellinInv σ (mellin f) x = f x

The inverse Mellin transform of the Mellin transform applied to x > 0 is x.