Theorems · Theorem · integral transforms

mellinConvergent_of_isBigO_rpow

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    (f =O[Filter.atTop] fun x => x ^ (-a)) →
      s.re < a → (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → MellinConvergent f s

Defined in

Mathlib.Analysis.MellinTransform

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace