Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 07:09 399ce38e

View on Github →

feat(measure_theory/integral): continuous functions with exponential decay are integrable (#12539)

Estimated changes

Created src/measure_theory/integral/exp_decay.lean

added theorem exp_neg_integrable_on_Ioi

added theorem integrable_of_is_O_exp_neg

added theorem integral_exp_neg_le