# mathlibdocumentation

measure_theory.integral.exp_decay

# 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: If f is continuous on [a,∞), for some a ∈ ℝ, and there exists b > 0 such that f(x) = O(exp(-b x)) as x → ∞, then f is integrable on (a, ∞).
theorem integral_exp_neg_le {b : } (a X : ) (h2 : 0 < b) :
∫ (x : ) in a..X, real.exp (-b * x) real.exp (-b * a) / b

Integral of exp (-b * x) over (a, X) is bounded as X → ∞.

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

theorem integrable_of_is_O_exp_neg {f : } {a b : } (h0 : 0 < b) (h1 : (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, ∞).