# Documentation

Mathlib.MeasureTheory.Function.Jacobian

# Change of variables in higher-dimensional integrals #

Let μ be a Lebesgue measure on a finite-dimensional real vector space E. Let f : E → E be a function which is injective and differentiable on a measurable set s, with derivative f'. Then we prove that f '' s is measurable, and its measure is given by the formula μ (f '' s) = ∫⁻ x in s, |(f' x).det| ∂μ (where (f' x).det is almost everywhere measurable, but not Borel-measurable in general). This formula is proved in lintegral_abs_det_fderiv_eq_addHaar_image. We deduce the change of variables formula for the Lebesgue and Bochner integrals, in lintegral_image_eq_lintegral_abs_det_fderiv_mul and integral_image_eq_integral_abs_det_fderiv_smul respectively.

## Main results #

• addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero: if f is differentiable on a set s with zero measure, then f '' s also has zero measure.
• addHaar_image_eq_zero_of_det_fderivWithin_eq_zero: if f is differentiable on a set s, and its derivative is never invertible, then f '' s has zero measure (a version of Sard's lemma).
• aemeasurable_fderivWithin: if f is differentiable on a measurable set s, then f' is almost everywhere measurable on s.

For the next statements, s is a measurable set and f is differentiable on s (with a derivative f') and injective on s.

• measurable_image_of_fderivWithin: the image f '' s is measurable.
• measurableEmbedding_of_fderivWithin: the function s.restrict f is a measurable embedding.
• lintegral_abs_det_fderiv_eq_addHaar_image: the image measure is given by μ (f '' s) = ∫⁻ x in s, |(f' x).det| ∂μ.
• lintegral_image_eq_lintegral_abs_det_fderiv_mul: for g : E → ℝ≥0∞, one has ∫⁻ x in f '' s, g x ∂μ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ.
• integral_image_eq_integral_abs_det_fderiv_smul: for g : E → F, one has ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ.
• integrableOn_image_iff_integrableOn_abs_det_fderiv_smul: for g : E → F, the function g is integrable on f '' s if and only if |(f' x).det| • g (f x)) is integrable on s.

## Implementation #

Typical versions of these results in the literature have much stronger assumptions: s would typically be open, and the derivative f' x would depend continuously on x and be invertible everywhere, to have the local inverse theorem at our disposal. The proof strategy under our weaker assumptions is more involved. We follow [Fremlin, Measure Theory (volume 2)][fremlin_vol2].

The first remark is that, if f is sufficiently well approximated by a linear map A on a set s, then f expands the volume of s by at least A.det - ε and at most A.det + ε, where the closeness condition depends on A in a non-explicit way (see addHaar_image_le_mul_of_det_lt and mul_le_addHaar_image_of_lt_det). This fact holds for balls by a simple inclusion argument, and follows for general sets using the Besicovitch covering theorem to cover the set by balls with measures adding up essentially to μ s.

When f is differentiable on s, one may partition s into countably many subsets s ∩ t n (where t n is measurable), on each of which f is well approximated by a linear map, so that the above results apply. See exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, which follows from the pointwise differentiability (in a non-completely trivial way, as one should ensure a form of uniformity on the sets of the partition).

Combining the above two results would give the conclusion, except for two difficulties: it is not obvious why f '' s and f' should be measurable, which prevents us from using countable additivity for the measure and the integral. It turns out that f '' s is indeed measurable, and that f' is almost everywhere measurable, which is enough to recover countable additivity.

The measurability of f '' s follows from the deep Lusin-Souslin theorem ensuring that, in a Polish space, a continuous injective image of a measurable set is measurable.

The key point to check the almost everywhere measurability of f' is that, if f is approximated up to δ by a linear map on a set s, then f' is within δ of A on a full measure subset of s (namely, its density points). With the above approximation argument, it follows that f' is the almost everywhere limit of a sequence of measurable functions (which are constant on the pieces of the good discretization), and is therefore almost everywhere measurable.

## Tags #

Change of variables in integrals

[Fremlin, Measure Theory (volume 2)][fremlin_vol2]