Commit 2025-06-24 07:54 edf2cbec

View on Github →

feat: change of variables formula in integrals for monotone functions (#26198) The good change of variables formula in integrals we have is for injective functions (in any dimension). In this PR, we show that the same formula holds for monotone functions (which are not necessarily injective) by reducing to the previous theorem.

Estimated changes

Modified Mathlib/MeasureTheory/Function/JacobianOneDim.lean

added theorem MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt

added theorem MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn

added theorem MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn

added theorem MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone

added theorem MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn

added theorem MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn

added theorem MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn

added theorem MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn

added theorem MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn