Commit 2024-07-17 18:39 51801a27

View on Github →

feat(Integral/Lebesgue): add setLIntegral_biUnion_of_directed (#14740) also drop some unneeded measurability assumptions.

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

added theorem MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

deleted theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le'

deleted theorem MeasureTheory.lintegral_le_of_forall_fin_meas_le_of_measurable

added theorem MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le

added theorem MeasureTheory.setLIntegral_iUnion_of_directed