# Documentation

Mathlib.Analysis.MellinTransform

# 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.
theorem Complex.cpow_mul_ofReal_nonneg {x : } (hx : 0 x) (y : ) (z : ) :
x ^ (y * z) = ↑(x ^ y) ^ z
def MellinConvergent {E : Type u_1} [] (f : E) (s : ) :

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

Instances For
theorem MellinConvergent.const_smul {E : Type u_1} [] {f : E} {s : } (hf : ) {𝕜 : Type u_2} [] [] (c : 𝕜) :
MellinConvergent (fun t => c f t) s
theorem MellinConvergent.cpow_smul {E : Type u_1} [] {f : E} {s : } {a : } :
MellinConvergent (fun t => t ^ a f t) s MellinConvergent f (s + a)
theorem MellinConvergent.div_const {f : } {s : } (hf : ) (a : ) :
MellinConvergent (fun t => f t / a) s
theorem MellinConvergent.comp_mul_left {E : Type u_1} [] {f : E} {s : } {a : } (ha : 0 < a) :
MellinConvergent (fun t => f (a * t)) s
theorem MellinConvergent.comp_rpow {E : Type u_1} [] {f : E} {s : } {a : } (ha : a 0) :
MellinConvergent (fun t => f (t ^ a)) s MellinConvergent f (s / a)
def mellin {E : Type u_1} [] (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.

Instances For
theorem mellin_cpow_smul {E : Type u_1} [] (f : E) (s : ) (a : ) :
mellin (fun t => t ^ a f t) s = mellin f (s + a)
theorem mellin_const_smul {E : Type u_1} [] (f : E) (s : ) {𝕜 : Type u_2} [] [] (c : 𝕜) :
mellin (fun t => c f t) s = c mellin f s
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} [] [] (f : E) (s : ) {a : } (ha : a 0) :
mellin (fun t => f (t ^ a)) s = |a|⁻¹ mellin f (s / a)
theorem mellin_comp_mul_left {E : Type u_1} [] [] (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} [] [] (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} [] [] (f : E) (s : ) :
mellin (fun t => f t⁻¹) s = mellin f (-s)
def HasMellin {E : Type u_1} [] (f : E) (s : ) (m : E) :

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

Instances For
theorem hasMellin_add {E : Type u_1} [] {f : E} {g : E} {s : } (hf : ) (hg : ) :
HasMellin (fun t => f t + g t) s (mellin f s + mellin g s)
theorem hasMellin_sub {E : Type u_1} [] {f : E} {g : E} {s : } (hf : ) (hg : ) :
HasMellin (fun t => f t - g t) s (mellin f s - mellin g s)

## Convergence of Mellin transform integrals #

theorem mellin_convergent_iff_norm {E : Type u_1} [] {f : E} {T : } (hT : T ) (hT' : ) (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.restrict MeasureTheory.volume ())) {s : } :
MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) f t) T MeasureTheory.IntegrableOn (fun t => t ^ (s.re - 1) * f t) T

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.Measure.restrict MeasureTheory.volume ())) {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) ()

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.Measure.restrict MeasureTheory.volume ())) (hf : f =O[nhdsWithin 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)

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 : ) (hf_top : f =O[Filter.atTop] fun x => x ^ (-a)) (hs_top : s < a) (hf_bot : f =O[nhdsWithin 0 ()] fun x => x ^ (-b)) (hs_bot : b < s) :
MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) ()

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} [] {a : } {b : } {f : E} {s : } (hfc : ) (hf_top : f =O[Filter.atTop] fun x => x ^ (-a)) (hs_top : s.re < a) (hf_bot : f =O[nhdsWithin 0 ()] fun x => x ^ (-b)) (hs_bot : b < s.re) :
theorem isBigO_rpow_top_log_smul {E : Type u_1} [] {a : } {b : } {f : E} (hab : b < a) (hf : f =O[Filter.atTop] fun x => x ^ (-a)) :
(fun 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} [] {a : } {b : } {f : E} (hab : a < b) (hf : f =O[nhdsWithin 0 ()] fun x => x ^ (-a)) :
(fun t => f t) =O[nhdsWithin 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} [] [] {a : } {b : } {f : E} {s : } (hfc : ) (hf_top : f =O[Filter.atTop] fun x => x ^ (-a)) (hs_top : s.re < a) (hf_bot : f =O[nhdsWithin 0 ()] fun x => x ^ (-b)) (hs_bot : b < s.re) :
MellinConvergent (fun t => f t) s HasDerivAt () (mellin (fun 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} [] [] {a : } {b : } {f : E} {s : } (hfc : ) (hf_top : f =O[Filter.atTop] fun x => x ^ (-a)) (hs_top : s.re < a) (hf_bot : f =O[nhdsWithin 0 ()] fun x => x ^ (-b)) (hs_bot : b < s.re) :

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} [] {a : } {b : } (ha : 0 < a) {f : E} {s : } (hfc : ) (hf_top : f =O[Filter.atTop] fun t => Real.exp (-a * t)) (hf_bot : f =O[nhdsWithin 0 ()] fun x => x ^ (-b)) (hs_bot : b < s.re) :

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} [] [] {a : } {b : } (ha : 0 < a) {f : E} {s : } (hfc : ) (hf_top : f =O[Filter.atTop] fun t => Real.exp (-a * t)) (hf_bot : f =O[nhdsWithin 0 ()] fun x => x ^ (-b)) (hs_bot : b < s.re) :

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.indicator (Set.Ioc 0 1) 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.indicator (Set.Ioc 0 1) fun t => t ^ a) s (1 / (s + a))

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