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

Specialized versions in one dimension (using the derivative instead of the determinant of the Fréchet derivative) can be found in the file `Mathlib/MeasureTheory/Function/JacobianOneDim.lean`, together with versions for monotone and antitone functions.

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

## References #

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

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

source
theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [SecondCountableTopology F] (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt 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 : ℕ), IsClosed (t n)) ∧ s ⊆ ⋃ (n : ℕ), t n ∧ (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ 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`.

source
theorem exists_partition_approximatesLinearOn_of_hasFDerivWithinAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology F] (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F) (hf' : ∀ x ∈ s, HasFDerivWithinAt 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 (Function.onFun Disjoint t) ∧ (∀ (n : ℕ), MeasurableSet (t n)) ∧ s ⊆ ⋃ (n : ℕ), t n ∧ (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ 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.

source
theorem MeasureTheory.addHaar_image_le_mul_of_det_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (A : E →L[ℝ] E) {m : NNReal} (hm : ENNReal.ofReal |A.det| < ↑m) :
∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0), ∀ (s : Set E) (f : E → E), ApproximatesLinearOn 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`.

source
theorem MeasureTheory.mul_le_addHaar_image_of_lt_det {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (A : E →L[ℝ] E) {m : NNReal} (hm : ↑m < ENNReal.ofReal |A.det|) :
∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0), ∀ (s : Set E) (f : E → E), ApproximatesLinearOn 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`.

source
theorem ApproximatesLinearOn.norm_fderiv_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {A : E →L[ℝ] E} {δ : NNReal} (hf : ApproximatesLinearOn f A s δ) (hs : MeasurableSet s) (f' : E → E →L[ℝ] E) (hf' : ∀ x ∈ s, HasFDerivWithinAt 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.

source
theorem MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hf : DifferentiableOn ℝ f s) (hs : μ s = 0) :
μ (f '' s) = 0

A differentiable function maps sets of measure zero to sets of measure zero.

source
theorem MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (R : ℝ) (hs : s ⊆ Metric.closedBall 0 R) (ε : NNReal) (εpos : 0 < ε) (h'f' : ∀ x ∈ s, (f' x).det = 0) :
μ (f '' s) ≤ ↑ε * μ (Metric.closedBall 0 R)

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.

source
theorem MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (h'f' : ∀ 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.

source
theorem MeasureTheory.aemeasurable_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
AEMeasurable f' (μ.restrict s)

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

source
theorem MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
AEMeasurable (fun (x : E) => ENNReal.ofReal |(f' x).det|) (μ.restrict s)
source
theorem MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
AEMeasurable (fun (x : E) => |(f' x).det|.toNNReal) (μ.restrict s)
source
theorem MeasureTheory.measurable_image_of_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
MeasurableSet (f '' s)

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

source
theorem MeasureTheory.nullMeasurable_image_of_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : NullMeasurableSet s μ) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
NullMeasurableSet (f '' s) μ

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

source
theorem MeasureTheory.measurableEmbedding_of_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
MeasurableEmbedding (s.restrict f)

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

source
theorem MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) {ε : NNReal} (εpos : 0 < ε) :
μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
source
theorem MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (h's : μ s ≠ ⊤) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
source
theorem MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
source
theorem MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) {ε : NNReal} (εpos : 0 < ε) :
∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
source
theorem MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (h's : μ s ≠ ⊤) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
source
theorem MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
source
theorem MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
∫⁻ (x : E) in s, ENNReal.ofReal |(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_fderivWithin`.

source
theorem MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : NullMeasurableSet s μ) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = μ (f '' s)

Change of variable formula for differentiable functions, set version: if a function `f` is injective and differentiable on a null measurable set `s`, then the measure of `f '' s` is given by the integral of `|(f' x).det|` on `s`. Note that the null-measurability of `f '' s` is given by `nullMeasurable_image_of_fderivWithin`.

source
theorem MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : NullMeasurableSet s μ) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
Measure.map f ((μ.restrict s).withDensity fun (x : E) => ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)

Change of variable formula for differentiable functions, set version: if a function `f` is injective and differentiable on a null measurable set `s`, then the pushforward of the measure with density `|(f' x).det|` on `s` is the Lebesgue measure on the image set.

source
theorem MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun (x : E) => ENNReal.ofReal |(f' x).det|)) = μ.restrict (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 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, see `map_withDensity_abs_det_fderiv_eq_addHaar`.

### Change of variable formulas in integrals #

source
theorem MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : E → ENNReal) :
∫⁻ (x : E) in f '' s, g x ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
source
theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : E → F) :
IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun (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`.

source
theorem MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn 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`.

source
theorem MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {f : OpenPartialHomeomorph E E} (hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x) (g : E → F) :
∫ (x : E) in f.target, g x ∂μ = ∫ (x : E) in f.source, |(f' x).det| • g (↑f x) ∂μ
source
theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf : MeasurableEmbedding f) {g : E → ℝ} (hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x) (hg_int : MeasureTheory.IntegrableOn g (f '' s) μ) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
(MeasureTheory.Measure.comap f (μ.withDensity fun (x : E) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
source
theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {f' : E → E →L[ℝ] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (f : E ≃ᵐ E) {g : E → ℝ} (hg : ∀ᵐ (x : E) ∂μ, x ∈ ⇑f '' s → 0 ≤ g x) (hg_int : MeasureTheory.IntegrableOn g (⇑f '' s) μ) (hf' : ∀ x ∈ s, HasFDerivWithinAt (⇑f) (f' x) s x) :
(MeasureTheory.Measure.map (⇑f.symm) (μ.withDensity fun (x : E) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)