Documentation

Mathlib.Analysis.MellinInversion

Mellin inversion formula #

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

Main results #

theorem mellinInv_eq_fourierIntegralInv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (σ : ) (f : E) {x : } (hx : 0 < 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.