Theorems · Theorem · integral transforms

mellin_convergent_zero_of_isBigO

∀ {b : ℝ} {f : ℝ → ℝ},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
    (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
      ∀ {s : ℝ},
        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.

Defined in

Mathlib.Analysis.MellinTransform

Cited by

1 results in Mathlib

Foundations

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