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 #

theorem Complex.cpow_mul_ofReal_nonneg {x : } (hx : 0 x) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ z
def MellinConvergent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (s : ) :

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

Equations
Instances For
    theorem MellinConvergent.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : } (hf : MellinConvergent f s) {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 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)

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

    Equations
    Instances For
      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.

      Equations
      Instances For
        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).

        Equations
        Instances For
          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} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 E] (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} [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) :

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

          Equations
          Instances For
            theorem hasMellin_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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 : E} {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)

            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.Measure.restrict MeasureTheory.volume (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.Measure.restrict MeasureTheory.volume (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.Measure.restrict MeasureTheory.volume (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) :
            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] [CompleteSpace 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] [CompleteSpace 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) :

            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) :

            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] [CompleteSpace 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) :

            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.