Commit 2025-01-03 22:22 155a0a99

View on Github →

feat: add ENNReal.finStronglyMeasurable_of_measurable (#20404) A measurable function with finite Lebesgue integral can be approximated by simple functions whose support has finite measure. I created a new file StronglyMeasurable/ENNReal instead of using StronglyMeasurable/Lemmas because those lemmas will be useful in places that should not import things like the Bochner integral.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

added theorem MeasureTheory.SimpleFunc.measure_support_lt_top

added theorem MeasureTheory.SimpleFunc.measure_support_lt_top_of_lintegral_ne_top

added theorem MeasureTheory.SimpleFunc.tendsto_eapprox

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

deleted theorem MeasureTheory.SimpleFunc.measure_support_lt_top

Created Mathlib/MeasureTheory/Function/StronglyMeasurable/ENNReal.lean

added theorem ENNReal.aefinStronglyMeasurable_of_aemeasurable

added theorem ENNReal.finStronglyMeasurable_of_measurable

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.lintegral_eapprox_le_lintegral

added theorem MeasureTheory.measure_support_eapprox_lt_top