Commit 2022-07-14 09:37 f3ae2d0d

View on Github →

feat(measure_theory/constructions/prod): The layercake integral. (#14424) Prove the layercake formula, a.k.a. Cavalieri's principle, often used in measure theory and probability theory. It will in particular be a part of the proof of the portmanteau theorem.

Estimated changes

Modified src/measure_theory/function/l1_space.lean

Modified src/measure_theory/function/strongly_measurable.lean

deleted theorem measure_theory.ae_measurable_zero_measure

added theorem measure_theory.ae_strongly_measurable_zero_measure

Created src/measure_theory/integral/layercake.lean

added theorem measure_theory.lintegral_comp_eq_lintegral_meas_le_mul

added theorem measure_theory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable

added theorem measure_theory.lintegral_eq_lintegral_meas_le

added theorem measure_theory.lintegral_rpow_eq_lintegral_meas_le_mul

Modified src/measure_theory/measure/ae_measurable.lean

added theorem ae_measurable.exists_measurable_nonneg

added theorem ae_measurable_Ioi_of_forall_Ioc

Modified src/measure_theory/measure/lebesgue.lean

added theorem measurable_set_graph

added theorem measurable_set_region_between_cc

added theorem measurable_set_region_between_co

added theorem measurable_set_region_between_oc