mathlib documentation

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:

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, ∞).

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