mathlib3 documentation


Integrals with exponential decay at ∞ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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