Documentation

Mathlib.MeasureTheory.Integral.ExpDecay

Integrals with exponential decay at ∞ #

As easy special cases of general theorems in the library, we prove the following test for integrability:

theorem exp_neg_integrableOn_Ioi (a : ) {b : } (h : 0 < b) :
MeasureTheory.IntegrableOn (fun (x : ) => Real.exp (-b * x)) (Set.Ioi a) MeasureTheory.volume

exp (-b * x) is integrable on (a, ∞).

theorem integrable_of_isBigO_exp_neg {f : } {a : } {b : } (h0 : 0 < b) (hf : ContinuousOn f (Set.Ici a)) (ho : 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, ∞).