Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-07 13:31
61adfa9f
View on Github →
feat: bound the measure of a set by the integral of a function, from above and from below (
#8123
) Also weaken some T2 space assumptions in some integration lemmas.
Estimated changes
Modified
Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
modified
theorem
Continuous.integrableOn_Icc
modified
theorem
Continuous.integrableOn_Ioc
modified
theorem
Continuous.integrableOn_uIcc
modified
theorem
Continuous.integrableOn_uIoc
modified
theorem
Continuous.locallyIntegrable
modified
theorem
ContinuousOn.integrableOn_Icc
added
theorem
ContinuousOn.integrableOn_compact'
modified
theorem
ContinuousOn.integrableOn_compact
modified
theorem
ContinuousOn.integrableOn_uIcc
modified
theorem
ContinuousOn.locallyIntegrableOn
Modified
Mathlib/MeasureTheory/Integral/Bochner.lean
added
theorem
MeasureTheory.integral_smul_nnreal_measure
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
added
theorem
MeasureTheory.lintegral_indicator_const_le
added
theorem
MeasureTheory.lintegral_indicator_le
added
theorem
MeasureTheory.lintegral_indicator_one_le
added
theorem
MeasureTheory.lintegral_indicator_one₀
added
theorem
MeasureTheory.lintegral_le_meas
added
theorem
MeasureTheory.meas_le_lintegral₀
Modified
Mathlib/MeasureTheory/Integral/SetIntegral.lean
added
theorem
MeasureTheory.Integrable.measure_le_integral
added
theorem
MeasureTheory.integral_le_measure