Commit 2023-09-30 17:02 86831e86

View on Github →

feat: Add a basic layercake formula for Bochner integral. (#7167) Layer cake formulas currently exist for ENNReal-valued functions and Lebesgue integrals. This PR adds the most common version of the layer cake formula for integrable a.e.-nonnegative real-valued functions and Bochner integrals.

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.HasFiniteIntegral.restrict

modified theorem MeasureTheory.Integrable.measure_ge_lt_top

added theorem MeasureTheory.Integrable.measure_gt_lt_top

added theorem MeasureTheory.Integrable.measure_le_lt_top

added theorem MeasureTheory.Integrable.measure_lt_lt_top

added theorem MeasureTheory.Integrable.measure_norm_ge_lt_top

added theorem MeasureTheory.Integrable.measure_norm_gt_lt_top

added theorem MeasureTheory.Integrable.restrict

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

added theorem MeasureTheory.Integrable.integral_eq_integral_meas_lt

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem MeasureTheory.ae_restrict_eq_const_iff_ae_eq_const_of_mem'

added theorem MeasureTheory.ae_restrict_eq_const_iff_ae_eq_const_of_mem

added theorem MeasureTheory.set_integral_eq_integral_of_ae_restrict_eq_zero

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const