mathlib

6ca5910f - feat(measure_theory/integral/lebesgue): approximate a function by a finite integral function in a sigma-finite measure space. (#14528)

feat(measure_theory/integral/lebesgue): approximate a function by a finite integral function in a sigma-finite measure space. (#14528) If `L < ∫⁻ x, f x ∂μ`, then there exists a measurable function `g ≤ f` (even a simple function) with finite integral and `L < ∫⁻ x, g x ∂μ`, if the measure is sigma-finite. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>