Commit 2024-06-11 07:35 30fb6b87

View on Github →

chore: split application of the layer cake formula into its own file (#13702)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Created Mathlib/Analysis/SpecialFunctions/Pow/Integral.lean

added theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul

added theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

deleted theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul

deleted theorem MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean