Commit 2025-06-18 09:26 a8f73118

View on Github →

chore: split the file MeasureTheory.Function.Jacobian (#26069) I will add later more material for the change of variables with respect to monotone functions, so better split the file in advance. The new file, named JacobianOneDim, contains the material originally in Jacobian but dealing with one-dimensional functions. Along the way, I add one lemma lintegral_image_eq_lintegral_abs_deriv_mul which was obviously missing.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

deleted theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul'

deleted theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul

deleted theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul'

deleted theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul

deleted theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul

deleted theorem MeasureTheory.integral_image_eq_integral_abs_deriv_smul

Created Mathlib/MeasureTheory/Function/JacobianOneDim.lean

added theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul'

added theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul

added theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul'

added theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul

added theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul

added theorem MeasureTheory.integral_image_eq_integral_abs_deriv_smul

added theorem MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean