Commit 2024-11-07 15:53 b14fe2c8

View on Github →

feat: induction principle for ENNReal-valued measurable functions from a sigma-finite space (#17835) From GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

modified theorem Measurable.ennreal_induction

added theorem Measurable.ennreal_sigmaFinite_induction

deleted theorem MeasureTheory.SimpleFunc.coe_le

added theorem MeasureTheory.SimpleFunc.coe_le_coe

added theorem MeasureTheory.SimpleFunc.coe_lt_coe

added theorem MeasureTheory.SimpleFunc.eapprox_mono

added theorem MeasureTheory.SimpleFunc.iSup_coe_eapprox

modified theorem MeasureTheory.SimpleFunc.iSup_eapprox_apply

added theorem MeasureTheory.SimpleFunc.mk_le_mk

added theorem MeasureTheory.SimpleFunc.mk_lt_mk

added theorem MeasureTheory.SimpleFunc.piecewise_mono

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Probability/Kernel/Composition.lean

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean