Commit 2025-06-25 15:49 60041760

View on Github →

feat: weaken assumption to NullMeasurableSet in some results on change of variables in integrals (#26362)

Estimated changes

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

added theorem MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀

modified theorem MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar

added theorem MeasureTheory.nullMeasurable_image_of_fderivWithin