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:

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