Theorems · Theorem · integral transforms

mellin_differentiableAt_of_isBigO_rpow_exp

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ},
  0 < a →
    ∀ {f : ℝ → E} {s : ℂ},
      MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
        (f =O[Filter.atTop] fun t => Real.exp (-a * t)) →
          (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → 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.

Defined in

Mathlib.Analysis.MellinTransform

Cited by

0 results in Mathlib

Foundations

Depth 276 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace