mathlib

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