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_fourier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) {s : ℂ} : mellin f s = FourierTransform.fourier (fun (u : ℝ) => Real.exp (-s.re * u) • f (Real.exp (-u))) (s.im / (2 * Real.pi))

@[deprecated mellin_eq_fourier (since := "2025-11-16")]

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

Alias of mellin_eq_fourier.

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

@[deprecated mellinInv_eq_fourierInv (since := "2025-11-16")]

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

Alias of mellinInv_eq_fourierInv.

theorem mellinInv_mellin_eq {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.

@[deprecated mellinInv_mellin_eq (since := "2025-11-16")]

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

Alias of mellinInv_mellin_eq.

---

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