Commit 2024-10-09 19:21 c94e2488

View on Github →

feat: setLintegral for indicator function and le_meas (#15322) from GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.setLIntegral_indicator

added theorem MeasureTheory.setLIntegral_indicator₀

added theorem MeasureTheory.setLIntegral_le_meas