Commit 2024-11-28 14:24 19f864c3

View on Github →

feat(MeasureTheory): integrability lemmas (#19439) Mostly about the relation between Integrable and the Lebesgue integral for real/ennreal functions. From the TestingLowerBounds project.

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.Integrable.neg'

added theorem MeasureTheory.hasFiniteIntegral_toReal_iff

modified theorem MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top

added theorem MeasureTheory.integrable_add_iff_integrable_left'

added theorem MeasureTheory.integrable_add_iff_integrable_right'

added theorem MeasureTheory.integrable_of_le_of_le

added theorem MeasureTheory.integrable_toReal_iff

added theorem MeasureTheory.lintegral_ofReal_ne_top_iff_integrable