mathlib documentation

measure_theory.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_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 #

For the next statements, s is a measurable set and f is differentiable on s (with a derivative f') and injective 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).

theorem exists_closed_cover_approximates_linear_on_of_has_fderiv_within_at {E : Type u_1} {F : Type u_2} [normed_group E] [normed_space E] [finite_dimensional E] [normed_group F] [normed_space F] [topological_space.second_countable_topology F] (f : E → F) (s : set E) (f' : E → (E →L[] F)) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (r : (E →L[] F)nnreal) (rpos : ∀ (A : E →L[] F), r A 0) :
∃ (t : set E) (A : (E →L[] F)), (∀ (n : ), is_closed (t n)) (s ⋃ (n : ), t n) (∀ (n : ), approximates_linear_on f (A n) (s t n) (r (A n))) (s.nonempty∀ (n : ), ∃ (y : E) (H : y s), A n = f' y)

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.

theorem exists_partition_approximates_linear_on_of_has_fderiv_within_at {E : Type u_1} {F : Type u_2} [normed_group E] [normed_space E] [finite_dimensional E] [normed_group F] [normed_space F] [measurable_space E] [borel_space E] [topological_space.second_countable_topology F] (f : E → F) (s : set E) (f' : E → (E →L[] F)) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (r : (E →L[] F)nnreal) (rpos : ∀ (A : E →L[] F), r A 0) :
∃ (t : set E) (A : (E →L[] F)), pairwise (disjoint on t) (∀ (n : ), measurable_set (t n)) (s ⋃ (n : ), t n) (∀ (n : ), approximates_linear_on f (A n) (s t n) (r (A n))) (s.nonempty∀ (n : ), ∃ (y : E) (H : y s), A n = f' y)

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.

theorem measure_theory.add_haar_image_le_mul_of_det_lt {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (A : E →L[] E) {m : nnreal} (hm : ennreal.of_real |A.det| < m) :
∀ᶠ (δ : nnreal) in nhds_within 0 (set.Ioi 0), ∀ (s : set E) (f : E → E), approximates_linear_on f A s δμ (f '' s) m * μ s

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.

theorem measure_theory.mul_le_add_haar_image_of_lt_det {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (A : E →L[] E) {m : nnreal} (hm : m < ennreal.of_real |A.det|) :
∀ᶠ (δ : nnreal) in nhds_within 0 (set.Ioi 0), ∀ (s : set E) (f : E → E), approximates_linear_on f A s δm * μ s μ (f '' s)

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.

theorem approximates_linear_on.norm_fderiv_sub_le {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] {A : E →L[] E} {δ : nnreal} (hf : approximates_linear_on f A s δ) (hs : measurable_set s) (f' : E → (E →L[] E)) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) :
∀ᵐ (x : E) ∂μ.restrict s, f' x - 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.

theorem measure_theory.add_haar_image_eq_zero_of_det_fderiv_within_eq_zero_aux {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (R : ) (hs : s metric.closed_ball 0 R) (ε : nnreal) (εpos : 0 < ε) (h'f' : ∀ (x : E), x s(f' x).det = 0) :
μ (f '' s) ε * μ (metric.closed_ball 0 R)

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. Here, we give an auxiliary statement towards this result.

theorem measure_theory.add_haar_image_eq_zero_of_det_fderiv_within_eq_zero {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (h'f' : ∀ (x : E), x s(f' x).det = 0) :
μ (f '' s) = 0

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.

theorem measure_theory.ae_measurable_fderiv_within {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) :

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).

theorem measure_theory.ae_measurable_of_real_abs_det_fderiv_within {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) :
ae_measurable (λ (x : E), ennreal.of_real |(f' x).det|) (μ.restrict s)
theorem measure_theory.ae_measurable_to_nnreal_abs_det_fderiv_within {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) :
ae_measurable (λ (x : E), |(f' x).det|.to_nnreal) (μ.restrict s)
theorem measure_theory.measurable_image_of_fderiv_within {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) :

If a function is differentiable and injective on a measurable set, then the image is measurable.

theorem measure_theory.measurable_embedding_of_fderiv_within {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) :

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.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.

theorem measure_theory.add_haar_image_le_lintegral_abs_det_fderiv_aux1 {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) {ε : nnreal} (εpos : 0 < ε) :
μ (f '' s) ∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ + 2 * ε * μ s
theorem measure_theory.add_haar_image_le_lintegral_abs_det_fderiv_aux2 {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (h's : μ s ) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) :
μ (f '' s) ∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ
theorem measure_theory.add_haar_image_le_lintegral_abs_det_fderiv {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) :
μ (f '' s) ∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ
theorem measure_theory.lintegral_abs_det_fderiv_le_add_haar_image_aux1 {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) {ε : nnreal} (εpos : 0 < ε) :
∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ μ (f '' s) + 2 * ε * μ s
theorem measure_theory.lintegral_abs_det_fderiv_le_add_haar_image_aux2 {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (h's : μ s ) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) :
∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ μ (f '' s)
theorem measure_theory.lintegral_abs_det_fderiv_le_add_haar_image {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) :
∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ μ (f '' s)
theorem measure_theory.lintegral_abs_det_fderiv_eq_add_haar_image {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) :
∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| μ = μ (f '' s)

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_fderiv_within.

theorem measure_theory.map_with_density_abs_det_fderiv_eq_add_haar {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) (h'f : measurable f) :

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_with_density_abs_det_fderiv_eq_add_haar.

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_with_density_abs_det_fderiv_eq_add_haar.

Change of variable formulas in integrals #

theorem measure_theory.lintegral_image_eq_lintegral_abs_det_fderiv_mul {E : Type u_1} [normed_group E] [normed_space E] [finite_dimensional E] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) (g : E → ennreal) :
∫⁻ (x : E) in f '' s, g x μ = ∫⁻ (x : E) in s, ennreal.of_real |(f' x).det| * g (f x) μ
theorem measure_theory.integrable_on_image_iff_integrable_on_abs_det_fderiv_smul {E : Type u_1} {F : Type u_2} [normed_group E] [normed_space E] [finite_dimensional E] [normed_group F] [normed_space F] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) (g : E → F) :
measure_theory.integrable_on g (f '' s) μ measure_theory.integrable_on (λ (x : E), |(f' x).det| g (f x)) s μ

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.

theorem measure_theory.integral_image_eq_integral_abs_det_fderiv_smul {E : Type u_1} {F : Type u_2} [normed_group E] [normed_space E] [finite_dimensional E] [normed_group F] [normed_space F] {s : set E} {f : E → E} {f' : E → (E →L[] E)} [measurable_space E] [borel_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] [complete_space F] (hs : measurable_set s) (hf' : ∀ (x : E), x shas_fderiv_within_at f (f' x) s x) (hf : set.inj_on f s) (g : E → F) :
(x : E) in f '' s, g x μ = (x : E) in s, |(f' x).det| g (f x) μ

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.