Theorems · Theorem · measure theory

integrable_of_isBigO_exp_neg

∀ {f : ℝ → ℝ} {a b : ℝ},
  0 < b →
    ContinuousOn f (Set.Ici a) →
      (f =O[Filter.atTop] fun x => Real.exp (-b * x)) → MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume

If f is continuous on [a, ∞), and is O (exp (-b * x)) at ∞ for some b > 0, then f is integrable on (a, ∞).

Defined in

Mathlib.MeasureTheory.Integral.ExpDecay

Cited by

1 results in Mathlib

Foundations

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