Commit 2023-06-09 20:01 2770c2e8

View on Github →

feat: port MeasureTheory.Integral.Layercake (#4913)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/Layercake.lean

added theorem Measure.countable_meas_le_ne_meas_lt

added theorem Measure.meas_le_ae_eq_meas_lt

added theorem Measure.meas_le_ne_meas_lt_subset_meas_pos

added theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul

added theorem MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable

added theorem MeasureTheory.lintegral_eq_lintegral_meas_le

added theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul

added theorem lintegral_comp_eq_lintegral_meas_lt_mul

added theorem lintegral_eq_lintegral_meas_lt

added theorem lintegral_rpow_eq_lintegral_meas_lt_mul