Integrals with exponential decay at ∞ #
As easy special cases of general theorems in the library, we prove the following test for integrability:
integrable_of_is_O_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_integrable_on_Ioi
(a : ℝ)
{b : ℝ}
(h : 0 < b) :
measure_theory.integrable_on (λ (x : ℝ), real.exp (-b * x)) (set.Ioi a) measure_theory.measure_space.volume
exp (-b * x)
is integrable on (a, ∞)
.
theorem
integrable_of_is_O_exp_neg
{f : ℝ → ℝ}
{a b : ℝ}
(h0 : 0 < b)
(h1 : continuous_on f (set.Ici a))
(h2 : f =O[filter.at_top] λ (x : ℝ), real.exp (-b * x)) :
If f
is continuous on [a, ∞)
, and is O (exp (-b * x))
at ∞
for some b > 0
, then
f
is integrable on (a, ∞)
.