Integrals with exponential decay at ∞ #
As easy special cases of general theorems in the library, we prove the following test for integrability:
integrable_of_isBigO_exp_neg
: Iff
is continuous on[a,∞)
, for somea ∈ ℝ
, and there existsb > 0
such thatf(x) = O(exp(-b x))
asx → ∞
, thenf
is integrable on(a, ∞)
.
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, ∞)
.