The Mellin transform

We define the Mellin transform of a locally integrable function on Ioi 0, and show it is differentiable in a suitable vertical strip.

Main statements

• mellin : the Mellin transform ∫ (t : ℝ) in Ioi 0, t ^ (s - 1) • f t, where s is a complex number.
• HasMellin: shorthand asserting that the Mellin transform exists and has a given value (analogous to HasSum).
• mellin_differentiableAt_of_isBigO_rpow : if f is O(x ^ (-a)) at infinity, and O(x ^ (-b)) at 0, then mellin f is holomorphic on the domain b < re s < a.

def MellinConvergent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) : Prop

Predicate on f and s asserting that the Mellin integral is well-defined.

theorem MellinConvergent.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) {𝕜 : Type u_2} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] [SMulCommClass ℂ 𝕜 E] (c : 𝕜) : MellinConvergent (fun (t : ℝ) => c • f t) s

theorem MellinConvergent.cpow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {s a : ℂ} : MellinConvergent (fun (t : ℝ) => ↑t ^ a • f t) s ↔ MellinConvergent f (s + a)

theorem MellinConvergent.div_const {f : ℝ → ℂ} {s : ℂ} (hf : MellinConvergent f s) (a : ℂ) : MellinConvergent (fun (t : ℝ) => f t / a) s

theorem MellinConvergent.comp_mul_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} {a : ℝ} (ha : 0 < a) : MellinConvergent (fun (t : ℝ) => f (a * t)) s ↔ MellinConvergent f s

theorem MellinConvergent.comp_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} {a : ℝ} (ha : a ≠ 0) : MellinConvergent (fun (t : ℝ) => f (t ^ a)) s ↔ MellinConvergent f (s / ↑a)

def Complex.VerticalIntegrable {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (σ : ℝ) (μ : MeasureTheory.Measure ℝ := by volume_tac) : Prop

A function f is VerticalIntegrable at σ if y ↦ f(σ + yi) is integrable.

def mellin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) : E

The Mellin transform of a function f (for a complex exponent s), defined as the integral of t ^ (s - 1) • f over Ioi 0.

def mellinInv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (σ : ℝ) (f : ℂ → E) (x : ℝ) : E

The Mellin inverse transform of a function f, defined as 1 / (2π) times the integral of y ↦ x ^ -(σ + yi) • f (σ + yi).

theorem mellin_cpow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s a : ℂ) : mellin (fun (t : ℝ) => ↑t ^ a • f t) s = mellin f (s + a)

theorem mellin_const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) {𝕜 : Type u_2} [NormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] (c : 𝕜) : mellin (fun (t : ℝ) => c • f t) s = c • mellin f s

Compatibility with scalar multiplication by a normed field. For scalar multiplication by more general rings assuming a priori that the Mellin transform is defined, see hasMellin_const_smul.

theorem mellin_div_const (f : ℝ → ℂ) (s a : ℂ) : mellin (fun (t : ℝ) => f t / a) s = mellin f s / a

theorem mellin_comp_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) (a : ℝ) : mellin (fun (t : ℝ) => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)

theorem mellin_comp_mul_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : 0 < a) : mellin (fun (t : ℝ) => f (a * t)) s = ↑a ^ (-s) • mellin f s

theorem mellin_comp_mul_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : 0 < a) : mellin (fun (t : ℝ) => f (t * a)) s = ↑a ^ (-s) • mellin f s

theorem mellin_comp_inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) : mellin (fun (t : ℝ) => f t⁻¹) s = mellin f (-s)

def HasMellin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) (m : E) : Prop

Predicate standing for "the Mellin transform of f is defined at s and equal to m". This shortens some arguments.

theorem hasMellin_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) (hg : MellinConvergent g s) : HasMellin (fun (t : ℝ) => f t + g t) s (mellin f s + mellin g s)

theorem hasMellin_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) (hg : MellinConvergent g s) : HasMellin (fun (t : ℝ) => f t - g t) s (mellin f s - mellin g s)

theorem hasMellin_const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) {R : Type u_2} [NormedRing R] [Module R E] [IsBoundedSMul R E] [SMulCommClass ℂ R E] (c : R) : HasMellin (fun (t : ℝ) => c • f t) s (c • mellin f s)

Convergence of Mellin transform integrals

theorem mellin_convergent_iff_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {T : Set ℝ} (hT : T ⊆ Set.Ioi 0) (hT' : MeasurableSet T) (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))) {s : ℂ} : MeasureTheory.IntegrableOn (fun (t : ℝ) => ↑t ^ (s - 1) • f t) T MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (s.re - 1) * ‖f t‖) T MeasureTheory.volume

Auxiliary lemma to reduce convergence statements from vector-valued functions to real scalar-valued functions.

theorem mellin_convergent_top_of_isBigO {f : ℝ → ℝ} (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))) {a s : ℝ} (hf : f =O[Filter.atTop] fun (x : ℝ) => x ^ (-a)) (hs : s < a) : ∃ (c : ℝ), 0 < c ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (s - 1) * f t) (Set.Ioi c) MeasureTheory.volume

If f is a locally integrable real-valued function which is O(x ^ (-a)) at ∞, then for any s < a, its Mellin transform converges on some neighbourhood of +∞.

theorem mellin_convergent_zero_of_isBigO {b : ℝ} {f : ℝ → ℝ} (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))) (hf : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) {s : ℝ} (hs : b < s) : ∃ (c : ℝ), 0 < c ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (s - 1) * f t) (Set.Ioc 0 c) MeasureTheory.volume

If f is a locally integrable real-valued function which is O(x ^ (-b)) at 0, then for any b < s, its Mellin transform converges on some right neighbourhood of 0.

theorem mellin_convergent_of_isBigO_scalar {a b : ℝ} {f : ℝ → ℝ} {s : ℝ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (hf_top : f =O[Filter.atTop] fun (x : ℝ) => x ^ (-a)) (hs_top : s < a) (hf_bot : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) (hs_bot : b < s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (s - 1) * f t) (Set.Ioi 0) MeasureTheory.volume

If f is a locally integrable real-valued function on Ioi 0 which is O(x ^ (-a)) at ∞ and O(x ^ (-b)) at 0, then its Mellin transform integral converges for b < s < a.

theorem mellinConvergent_of_isBigO_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (hf_top : f =O[Filter.atTop] fun (x : ℝ) => x ^ (-a)) (hs_top : s.re < a) (hf_bot : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) (hs_bot : b < s.re) : MellinConvergent f s

theorem isBigO_rpow_top_log_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : b < a) (hf : f =O[Filter.atTop] fun (x : ℝ) => x ^ (-a)) : (fun (t : ℝ) => Real.log t • f t) =O[Filter.atTop] fun (x : ℝ) => x ^ (-b)

If f is O(x ^ (-a)) as x → +∞, then log • f is O(x ^ (-b)) for every b < a.

theorem isBigO_rpow_zero_log_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : a < b) (hf : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-a)) : (fun (t : ℝ) => Real.log t • f t) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)

If f is O(x ^ (-a)) as x → 0, then log • f is O(x ^ (-b)) for every a < b.

theorem mellin_hasDerivAt_of_isBigO_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (hf_top : f =O[Filter.atTop] fun (x : ℝ) => x ^ (-a)) (hs_top : s.re < a) (hf_bot : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) (hs_bot : b < s.re) : MellinConvergent (fun (t : ℝ) => Real.log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun (t : ℝ) => Real.log t • f t) s) s

Suppose f is locally integrable on (0, ∞), is O(x ^ (-a)) as x → ∞, and is O(x ^ (-b)) as x → 0. Then its Mellin transform is differentiable on the domain b < re s < a, with derivative equal to the Mellin transform of log • f.

theorem mellin_differentiableAt_of_isBigO_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (hf_top : f =O[Filter.atTop] fun (x : ℝ) => x ^ (-a)) (hs_top : s.re < a) (hf_bot : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) (hs_bot : b < s.re) : DifferentiableAt ℂ (mellin f) s

Suppose f is locally integrable on (0, ∞), is O(x ^ (-a)) as x → ∞, and is O(x ^ (-b)) as x → 0. Then its Mellin transform is differentiable on the domain b < re s < a.

theorem mellinConvergent_of_isBigO_rpow_exp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} (ha : 0 < a) {f : ℝ → E} {s : ℂ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (hf_top : f =O[Filter.atTop] fun (t : ℝ) => Real.exp (-a * t)) (hf_bot : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) (hs_bot : b < s.re) : MellinConvergent f s

If f is locally integrable, decays exponentially at infinity, and is O(x ^ (-b)) at 0, then its Mellin transform converges for b < s.re.

theorem mellin_differentiableAt_of_isBigO_rpow_exp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} (ha : 0 < a) {f : ℝ → E} {s : ℂ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (hf_top : f =O[Filter.atTop] fun (t : ℝ) => Real.exp (-a * t)) (hf_bot : f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)) (hs_bot : b < s.re) : DifferentiableAt ℂ (mellin f) s

If f is locally integrable, decays exponentially at infinity, and is O(x ^ (-b)) at 0, then its Mellin transform is holomorphic on b < s.re.

Mellin transforms of functions on Ioc 0 1

theorem hasMellin_one_Ioc {s : ℂ} (hs : 0 < s.re) : HasMellin ((Set.Ioc 0 1).indicator fun (x : ℝ) => 1) s (1 / s)

The Mellin transform of the indicator function of Ioc 0 1.

theorem hasMellin_cpow_Ioc (a : ℂ) {s : ℂ} (hs : 0 < s.re + a.re) : HasMellin ((Set.Ioc 0 1).indicator fun (t : ℝ) => ↑t ^ a) s (1 / (s + a))

The Mellin transform of a power function restricted to Ioc 0 1.