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 Complex E] (f : Real → E) (s : Complex) : Prop

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

Equations

• Eq (MellinConvergent f s) (MeasureTheory.IntegrableOn (fun (t : Real) => HSMul.hSMul (HPow.hPow (Complex.ofReal t) (HSub.hSub s 1)) (f t)) (Set.Ioi 0) MeasureTheory.MeasureSpace.volume)

theorem MellinConvergent.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f : Real → E} {s : Complex} (hf : MellinConvergent f s) {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass Complex 𝕜 E] (c : 𝕜) : MellinConvergent (fun (t : Real) => HSMul.hSMul c (f t)) s

theorem MellinConvergent.cpow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f : Real → E} {s a : Complex} : Iff (MellinConvergent (fun (t : Real) => HSMul.hSMul (HPow.hPow (Complex.ofReal t) a) (f t)) s) (MellinConvergent f (HAdd.hAdd s a))

theorem MellinConvergent.div_const {f : Real → Complex} {s : Complex} (hf : MellinConvergent f s) (a : Complex) : MellinConvergent (fun (t : Real) => HDiv.hDiv (f t) a) s

theorem MellinConvergent.comp_mul_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f : Real → E} {s : Complex} {a : Real} (ha : LT.lt 0 a) : Iff (MellinConvergent (fun (t : Real) => f (HMul.hMul a t)) s) (MellinConvergent f s)

theorem MellinConvergent.comp_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f : Real → E} {s : Complex} {a : Real} (ha : Ne a 0) : Iff (MellinConvergent (fun (t : Real) => f (HPow.hPow t a)) s) (MellinConvergent f (HDiv.hDiv s (Complex.ofReal a)))

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

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

Equations

• Eq (Complex.VerticalIntegrable f σ μ) (MeasureTheory.Integrable (fun (y : Real) => f (HAdd.hAdd (Complex.ofReal σ) (HMul.hMul (Complex.ofReal y) Complex.I))) μ)

def mellin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s : Complex) : 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.

Equations

• Eq (mellin f s) (MeasureTheory.integral (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi 0)) fun (t : Real) => HSMul.hSMul (HPow.hPow (Complex.ofReal t) (HSub.hSub s 1)) (f t))

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem mellin_cpow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s a : Complex) : Eq (mellin (fun (t : Real) => HSMul.hSMul (HPow.hPow (Complex.ofReal t) a) (f t)) s) (mellin f (HAdd.hAdd s a))

theorem mellin_const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s : Complex) {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass Complex 𝕜 E] (c : 𝕜) : Eq (mellin (fun (t : Real) => HSMul.hSMul c (f t)) s) (HSMul.hSMul c (mellin f s))

theorem mellin_div_const (f : Real → Complex) (s a : Complex) : Eq (mellin (fun (t : Real) => HDiv.hDiv (f t) a) s) (HDiv.hDiv (mellin f s) a)

theorem mellin_comp_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s : Complex) (a : Real) : Eq (mellin (fun (t : Real) => f (HPow.hPow t a)) s) (HSMul.hSMul (Inv.inv (abs a)) (mellin f (HDiv.hDiv s (Complex.ofReal a))))

theorem mellin_comp_mul_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s : Complex) {a : Real} (ha : LT.lt 0 a) : Eq (mellin (fun (t : Real) => f (HMul.hMul a t)) s) (HSMul.hSMul (HPow.hPow (Complex.ofReal a) (Neg.neg s)) (mellin f s))

theorem mellin_comp_mul_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s : Complex) {a : Real} (ha : LT.lt 0 a) : Eq (mellin (fun (t : Real) => f (HMul.hMul t a)) s) (HSMul.hSMul (HPow.hPow (Complex.ofReal a) (Neg.neg s)) (mellin f s))

theorem mellin_comp_inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] (f : Real → E) (s : Complex) : Eq (mellin (fun (t : Real) => f (Inv.inv t)) s) (mellin f (Neg.neg s))

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

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

Equations

• Eq (HasMellin f s m) (And (MellinConvergent f s) (Eq (mellin f s) m))

theorem hasMellin_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f g : Real → E} {s : Complex} (hf : MellinConvergent f s) (hg : MellinConvergent g s) : HasMellin (fun (t : Real) => HAdd.hAdd (f t) (g t)) s (HAdd.hAdd (mellin f s) (mellin g s))

theorem hasMellin_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f g : Real → E} {s : Complex} (hf : MellinConvergent f s) (hg : MellinConvergent g s) : HasMellin (fun (t : Real) => HSub.hSub (f t) (g t)) s (HSub.hSub (mellin f s) (mellin g s))

Convergence of Mellin transform integrals

theorem mellin_convergent_iff_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Complex E] {f : Real → E} {T : Set Real} (hT : HasSubset.Subset T (Set.Ioi 0)) (hT' : MeasurableSet T) (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi 0))) {s : Complex} : Iff (MeasureTheory.IntegrableOn (fun (t : Real) => HSMul.hSMul (HPow.hPow (Complex.ofReal t) (HSub.hSub s 1)) (f t)) T MeasureTheory.MeasureSpace.volume) (MeasureTheory.IntegrableOn (fun (t : Real) => HMul.hMul (HPow.hPow t (HSub.hSub s.re 1)) (Norm.norm (f t))) T MeasureTheory.MeasureSpace.volume)

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

theorem mellin_convergent_top_of_isBigO {f : Real → Real} (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi 0))) {a s : Real} (hf : Asymptotics.IsBigO Filter.atTop f fun (x : Real) => HPow.hPow x (Neg.neg a)) (hs : LT.lt s a) : Exists fun (c : Real) => And (LT.lt 0 c) (MeasureTheory.IntegrableOn (fun (t : Real) => HMul.hMul (HPow.hPow t (HSub.hSub s 1)) (f t)) (Set.Ioi c) MeasureTheory.MeasureSpace.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 : Real} {f : Real → Real} (hfc : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.MeasureSpace.volume.restrict (Set.Ioi 0))) (hf : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) {s : Real} (hs : LT.lt b s) : Exists fun (c : Real) => And (LT.lt 0 c) (MeasureTheory.IntegrableOn (fun (t : Real) => HMul.hMul (HPow.hPow t (HSub.hSub s 1)) (f t)) (Set.Ioc 0 c) MeasureTheory.MeasureSpace.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 : Real} {f : Real → Real} {s : Real} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.MeasureSpace.volume) (hf_top : Asymptotics.IsBigO Filter.atTop f fun (x : Real) => HPow.hPow x (Neg.neg a)) (hs_top : LT.lt s a) (hf_bot : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) (hs_bot : LT.lt b s) : MeasureTheory.IntegrableOn (fun (t : Real) => HMul.hMul (HPow.hPow t (HSub.hSub s 1)) (f t)) (Set.Ioi 0) MeasureTheory.MeasureSpace.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 Complex E] {a b : Real} {f : Real → E} {s : Complex} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.MeasureSpace.volume) (hf_top : Asymptotics.IsBigO Filter.atTop f fun (x : Real) => HPow.hPow x (Neg.neg a)) (hs_top : LT.lt s.re a) (hf_bot : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) (hs_bot : LT.lt b s.re) : MellinConvergent f s

theorem isBigO_rpow_top_log_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace Real E] {a b : Real} {f : Real → E} (hab : LT.lt b a) (hf : Asymptotics.IsBigO Filter.atTop f fun (x : Real) => HPow.hPow x (Neg.neg a)) : Asymptotics.IsBigO Filter.atTop (fun (t : Real) => HSMul.hSMul (Real.log t) (f t)) fun (x : Real) => HPow.hPow x (Neg.neg 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 Real E] {a b : Real} {f : Real → E} (hab : LT.lt a b) (hf : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg a)) : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) (fun (t : Real) => HSMul.hSMul (Real.log t) (f t)) fun (x : Real) => HPow.hPow x (Neg.neg 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 Complex E] {a b : Real} {f : Real → E} {s : Complex} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.MeasureSpace.volume) (hf_top : Asymptotics.IsBigO Filter.atTop f fun (x : Real) => HPow.hPow x (Neg.neg a)) (hs_top : LT.lt s.re a) (hf_bot : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) (hs_bot : LT.lt b s.re) : And (MellinConvergent (fun (t : Real) => HSMul.hSMul (Real.log t) (f t)) s) (HasDerivAt (mellin f) (mellin (fun (t : Real) => HSMul.hSMul (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 Complex E] {a b : Real} {f : Real → E} {s : Complex} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.MeasureSpace.volume) (hf_top : Asymptotics.IsBigO Filter.atTop f fun (x : Real) => HPow.hPow x (Neg.neg a)) (hs_top : LT.lt s.re a) (hf_bot : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) (hs_bot : LT.lt b s.re) : DifferentiableAt Complex (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 Complex E] {a b : Real} (ha : LT.lt 0 a) {f : Real → E} {s : Complex} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.MeasureSpace.volume) (hf_top : Asymptotics.IsBigO Filter.atTop f fun (t : Real) => Real.exp (HMul.hMul (Neg.neg a) t)) (hf_bot : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) (hs_bot : LT.lt 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 Complex E] {a b : Real} (ha : LT.lt 0 a) {f : Real → E} {s : Complex} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.MeasureSpace.volume) (hf_top : Asymptotics.IsBigO Filter.atTop f fun (t : Real) => Real.exp (HMul.hMul (Neg.neg a) t)) (hf_bot : Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0)) f fun (x : Real) => HPow.hPow x (Neg.neg b)) (hs_bot : LT.lt b s.re) : DifferentiableAt Complex (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 : Complex} (hs : LT.lt 0 s.re) : HasMellin ((Set.Ioc 0 1).indicator fun (x : Real) => 1) s (HDiv.hDiv 1 s)

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

theorem hasMellin_cpow_Ioc (a : Complex) {s : Complex} (hs : LT.lt 0 (HAdd.hAdd s.re a.re)) : HasMellin ((Set.Ioc 0 1).indicator fun (t : Real) => HPow.hPow (Complex.ofReal t) a) s (HDiv.hDiv 1 (HAdd.hAdd s a))

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