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: iffis differentiable on a setswith zero measure, thenf '' salso has zero measure.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero: iffis differentiable on a sets, and its derivative is never invertible, thenf '' shas zero measure (a version of Sard's lemma).aemeasurable_fderivWithin: iffis differentiable on a measurable sets, thenf'is almost everywhere measurable ons.
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 imagef '' sis measurable.measurableEmbedding_of_fderivWithin: the functions.restrict fis 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: forg : 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: forg : 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: forg : E → F, the functiongis integrable onf '' sif and only if|(f' x).det| • g (f x))is integrable ons.
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 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
References #
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).
Assume that a function f has a derivative at every point of a set s. Then one may cover s
with countably many closed sets t n on which f is well approximated by linear maps A n.
Assume that a function f has a derivative at every point of a set s. Then one may
partition s into countably many disjoint relatively measurable sets (i.e., intersections
of s with measurable sets t n) on which f is well approximated by linear maps A n.
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.
Let f be a function which is sufficiently close (in the Lipschitz sense) to a given linear
map A. Then it expands the volume of any set by at most m for any m > det A.
Let f be a function which is sufficiently close (in the Lipschitz sense) to a given linear
map A. Then it expands the volume of any set by at least m for any m < det A.
If a differentiable function f is approximated by a linear map A on a set s, up to δ,
then at almost every x in s one has ‖f' x - A‖ ≤ δ.
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.
A differentiable function maps sets of measure zero to sets of measure zero.
A version of Sard's lemma in fixed dimension: given a differentiable function from E
to E and a set where the differential is not invertible, then the image of this set has
zero measure. Here, we give an auxiliary statement towards this result.
A version of Sard lemma in fixed dimension: given a differentiable function from E to E and
a set where the differential is not invertible, then the image of this set has zero measure.
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.
The derivative of a function on a measurable set is almost everywhere measurable on this set
with respect to Lebesgue measure. Note that, in general, it is not genuinely measurable there,
as f' is not unique (but only on a set of measure 0, as the argument shows).
If a function is differentiable and injective on a measurable set, then the image is measurable.
If a function is differentiable and injective on a measurable set s, then its restriction
to s is a measurable embedding.
Proving the estimate for the measure of the image #
We show the formula ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ = μ (f '' s),
in lintegral_abs_det_fderiv_eq_addHaar_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 formula for differentiable functions, set version: if a function f is
injective and differentiable on a measurable set s, then the measure of f '' s is given by the
integral of |(f' x).det| on s.
Note that the measurability of f '' s is given by measurable_image_of_fderivWithin.
Change of variable formula for differentiable functions, set version: if a function f is
injective and differentiable on a measurable set s, then the pushforward of the measure with
density |(f' x).det| on s is the Lebesgue measure on the image set. This version requires
that f is measurable, as otherwise Measure.map f is zero per our definitions.
For a version without measurability assumption but dealing with the restricted
function s.restrict f, see restrict_map_withDensity_abs_det_fderiv_eq_addHaar.
Change of variable formula for differentiable functions, set version: if a function f is
injective and differentiable on a measurable set s, then the pushforward of the measure with
density |(f' x).det| on s is the Lebesgue measure on the image set. This version is expressed
in terms of the restricted function s.restrict f.
For a version for the original function, but with a measurability assumption,
see map_withDensity_abs_det_fderiv_eq_addHaar.
Change of variable formulas in integrals #
Integrability in the change of variable formula for differentiable functions: if a
function f is injective and differentiable on a measurable set s, then a function
g : E → F is integrable on f '' s if and only if |(f' x).det| • g ∘ f is
integrable on s.
Change of variable formula for differentiable functions: if a function f is
injective and differentiable on a measurable set s, then the Bochner integral of a function
g : E → F on f '' s coincides with the integral of |(f' x).det| • g ∘ f on s.
Integrability in the change of variable formula for differentiable functions (one-variable
version): if a function f is injective and differentiable on a measurable set s ⊆ ℝ, then a
function g : ℝ → F is integrable on f '' s if and only if |(f' x)| • g ∘ f is integrable on
s.
Change of variable formula for differentiable functions (one-variable version): if a function
f is injective and differentiable on a measurable set s ⊆ ℝ, then the Bochner integral of a
function g : ℝ → F on f '' s coincides with the integral of |(f' x)| • g ∘ f on s.