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 #

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

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 : EF) (s : Set E) (f' : EE →L[] F) (hf' : xs, 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 : ), ys, 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_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 : EF) (s : Set E) (f' : EE →L[] F) (hf' : xs, 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 (Disjoint on t) (∀ (n : ), MeasurableSet (t n)) s ⋃ (n : ), t n (∀ (n : ), ApproximatesLinearOn f (A n) (s t n) (r (A n))) (s.Nonempty∀ (n : ), ys, 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 MeasureTheory.addHaar_image_le_mul_of_det_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.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 : EE), 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.

theorem MeasureTheory.mul_le_addHaar_image_of_lt_det {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.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 : EE), 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.

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

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 : EE} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.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.

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 : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hf' : xs, HasFDerivWithinAt f (f' x) s x) (R : ) (hs : s Metric.closedBall 0 R) (ε : NNReal) (εpos : 0 < ε) (h'f' : xs, (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.

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 : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hf' : xs, HasFDerivWithinAt f (f' x) s x) (h'f' : xs, (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 MeasureTheory.aemeasurable_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Set E} {f : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : xs, 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).

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

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

theorem MeasureTheory.measurableEmbedding_of_fderivWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Set E} {f : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (hs : MeasurableSet s) (hf' : xs, 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.

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

theorem MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Set E} {f : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : xs, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (h'f : Measurable f) :
MeasureTheory.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 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.

theorem MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Set E} {f : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : xs, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) :
MeasureTheory.Measure.map (s.restrict f) (MeasureTheory.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, but with a measurability assumption, see map_withDensity_abs_det_fderiv_eq_addHaar.

Change of variable formulas in integrals #

theorem MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Set E} {f : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : xs, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : EENNReal) :
∫⁻ (x : E) in f '' s, g xμ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x)μ
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 : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : xs, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : EF) :
MeasureTheory.IntegrableOn g (f '' s) μ MeasureTheory.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.

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 : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf' : xs, HasFDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : EF) :
∫ (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.

theorem MeasureTheory.det_one_smulRight {𝕜 : Type u_3} [NormedField 𝕜] (v : 𝕜) :
theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {s : Set } {f : } {f' : } (hs : MeasurableSet s) (hf' : xs, HasDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : F) :
MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume MeasureTheory.IntegrableOn (fun (x : ) => |f' x| g (f x)) s MeasureTheory.volume

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.

theorem MeasureTheory.integral_image_eq_integral_abs_deriv_smul {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {s : Set } {f : } {f' : } (hs : MeasurableSet s) (hf' : xs, HasDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : F) :
∫ (x : ) in f '' s, g x = ∫ (x : ) in s, |f' x| g (f x)

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.

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' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : PartialHomeomorph E E} (hf' : xf.source, HasFDerivAt (↑f) (f' x) x) (g : EF) :
∫ (x : E) in f.target, g xμ = ∫ (x : E) in f.source, |(f' x).det| g (f x)μ
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 : EE} {f' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (hf : MeasurableEmbedding f) {g : E} (hg : ∀ᵐ (x : E) ∂μ, x f '' s0 g x) (hg_int : MeasureTheory.IntegrableOn g (f '' s) μ) (hf' : xs, 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)μ)
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' : EE →L[] E} [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hs : MeasurableSet s) (f : E ≃ᵐ E) {g : E} (hg : ∀ᵐ (x : E) ∂μ, x f '' s0 g x) (hg_int : MeasureTheory.IntegrableOn g (f '' s) μ) (hf' : xs, 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)μ)
theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul {f : } (hf : MeasurableEmbedding f) {s : Set } (hs : MeasurableSet s) {g : } (hg : ∀ᵐ (x : ), x f '' s0 g x) (hg_int : MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume) {f' : } (hf' : xs, HasDerivWithinAt f (f' x) s x) :
(MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun (x : ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ) in s, |f' x| * g (f x))
theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul (f : ≃ᵐ ) {s : Set } (hs : MeasurableSet s) {g : } (hg : ∀ᵐ (x : ), x f '' s0 g x) (hg_int : MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume) {f' : } (hf' : xs, HasDerivWithinAt (⇑f) (f' x) s x) :
(MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun (x : ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ) in s, |f' x| * g (f x))
theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' {f : } (hf : MeasurableEmbedding f) {s : Set } (hs : MeasurableSet s) {f' : } (hf' : ∀ (x : ), HasDerivAt f (f' x) x) {g : } (hg : 0 ≤ᵐ[MeasureTheory.volume] g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) :
(MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun (x : ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ) in s, |f' x| * g (f x))
theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' (f : ≃ᵐ ) {s : Set } (hs : MeasurableSet s) {f' : } (hf' : ∀ (x : ), HasDerivAt (⇑f) (f' x) x) {g : } (hg : 0 ≤ᵐ[MeasureTheory.volume] g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) :
(MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun (x : ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ) in s, |f' x| * g (f x))