Change of variables in higher-dimensional integrals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_add_haar_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 #

• add_haar_image_eq_zero_of_differentiable_on_of_add_haar_eq_zero: if f is differentiable on a set s with zero measure, then f '' s also has zero measure.
• add_haar_image_eq_zero_of_det_fderiv_within_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).
• ae_measurable_fderiv_within: 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_fderiv_within: the image f '' s is measurable.
• measurable_embedding_of_fderiv_within: the function s.restrict f is a measurable embedding.
• lintegral_abs_det_fderiv_eq_add_haar_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.of_real (|(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) ∂μ.
• integrable_on_image_iff_integrable_on_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).

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 add_haar_image_le_mul_of_det_lt and mul_le_add_haar_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_approximates_linear_on_of_has_fderiv_within_at, 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

References #

Fremlin, Measure Theory (volume 2)

Decomposition lemmas #

We state lemmas ensuring that a differentiable function can be approximated, on countably many measurable pieces, by linear maps (with a prescribed precision depending on the linear map).

Local lemmas #

We check that a function which is well enough approximated by a linear map expands the volume essentially like this linear map, and that its derivative (if it exists) is almost everywhere close to the approximating linear map.

Measure zero of the image, over non-measurable sets #

If a set has measure 0, then its image under a differentiable map has measure zero. This doesn't require the set to be measurable. In the same way, if f is differentiable on a set s with non-invertible derivative everywhere, then f '' s has measure 0, again without measurability assumptions.

Weak measurability statements #

We show that the derivative of a function on a set is almost everywhere measurable, and that the image f '' s is measurable if f is injective on s. The latter statement follows from the Lusin-Souslin theorem.

Proving the estimate for the measure of the image #

We show the formula ∫⁻ x in s, ennreal.of_real (|(f' x).det|) ∂μ = μ (f '' s), in lintegral_abs_det_fderiv_eq_add_haar_image. For this, we show both inequalities in both directions, first up to controlled errors and then letting these errors tend to 0.

Change of variable formulas in integrals #