Commit 2023-06-08 04:46 0674e58f

View on Github →

feat: port MeasureTheory.Function.Jacobian (#4839)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/Jacobian.lean

added theorem ApproximatesLinearOn.norm_fderiv_sub_le

added theorem MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero

added theorem MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux

added theorem MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero

added theorem MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv

added theorem MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux1

added theorem MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2

added theorem MeasureTheory.addHaar_image_le_mul_of_det_lt

added theorem MeasureTheory.aemeasurable_fderivWithin

added theorem MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin

added theorem MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin

added theorem MeasureTheory.det_one_smulRight

added theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul

added theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul

added theorem MeasureTheory.integral_image_eq_integral_abs_deriv_smul

added theorem MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul

added theorem MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul

added theorem MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image

added theorem MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image

added theorem MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1

added theorem MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2

added theorem MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul

added theorem MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar

added theorem MeasureTheory.measurableEmbedding_of_fderivWithin

added theorem MeasureTheory.measurable_image_of_fderivWithin

added theorem MeasureTheory.mul_le_addHaar_image_of_lt_det

added theorem MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar

added theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt

added theorem exists_partition_approximatesLinearOn_of_hasFDerivWithinAt