Theorem MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone

Modification history

2026-03-23 08:24

Mathlib/MeasureTheory/Function/JacobianOneDim.lean

feat: more versions of the change of variables formula for monotone functions (#36855) …

Deleted MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone View on Github →

2025-06-24 07:54

Mathlib/MeasureTheory/Function/JacobianOneDim.lean

feat: change of variables formula in integrals for monotone functions (#26198) …

Added MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitone View on Github →