Densities of pushforwards under an injective change of variables

Let ρ be a measure on X, S a measurable set, T : X → X a measurable map and J : X → ℝ≥0∞ a measurable Jacobian for T on S, in the sense of the change of variables identity

ρ.withDensity g (T '' s) = ∫⁻ x in s, J x * g (T x) ∂ρ

for every measurable s ⊆ S and every g. Nothing else about T is assumed: the identity is the abstract output of a change of variables formula such as Mathlib's MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, and this file derives the consequences for pushforwards of measures μ ≪ ρ restricted to S.

• If J vanishes nowhere on S, then T pushes μ restricted to S to a measure absolutely continuous with respect to ρ.
• If moreover T is injective on S, maps measurable subsets of S to measurable sets, and J is finite on S, then the densities satisfy the Jacobian equation dμ/dρ (x) = J x * d(T₊ (μ|S))/dρ (T x) on S, and integrals of a function Φ with Φ 0 = 0 of the density of the pushforward are integrals over S: ∫ Φ (d(T₊ (μ|S))/dρ) dρ = ∫_S J x * Φ (dμ/dρ (x) / J x) dρ.

Main statements

• TauCeti.map_restrict_absolutelyContinuous_of_withDensity_image_eq: the pushforward of an absolutely continuous measure is absolutely continuous;
• TauCeti.restrict_eq_withDensity_indicator_rnDeriv_map_restrict: the Jacobian equation, as an identity of measures;
• TauCeti.lintegral_comp_rnDeriv_map_restrict: integrals of functions of the density of the pushforward, as integrals over the source.

theorem TauCeti.map_restrict_absolutelyContinuous_of_withDensity_image_eq {X : Type u_1} [MeasurableSpace X] (ρ : MeasureTheory.Measure X) {T : X → X} (hT : Measurable T) {S : Set X} (hSm : MeasurableSet S) {J : X → ENNReal} (hJm : Measurable J) (hJ : ∀ x ∈ S, J x ≠ 0) (hcov : ∀ (s : Set X), MeasurableSet s → s ⊆ S → ∀ (g : X → ENNReal), (ρ.withDensity g) (T '' s) = ∫⁻ (x : X) in s, J x * g (T x) ∂ρ) {μ : MeasureTheory.Measure X} (hμ : μ.AbsolutelyContinuous ρ) : (MeasureTheory.Measure.map T (μ.restrict S)).AbsolutelyContinuous ρ

Let T be a measurable map and J a measurable function vanishing nowhere on a measurable set S, such that ρ.withDensity g (T '' s) = ∫⁻ x in s, J x * g (T x) ∂ρ for every measurable s ⊆ S and every g. Then T pushes μ ≪ ρ restricted to S to a measure absolutely continuous with respect to ρ.

theorem TauCeti.restrict_eq_withDensity_indicator_rnDeriv_map_restrict {X : Type u_1} [MeasurableSpace X] (ρ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite ρ] {T : X → X} (hT : Measurable T) {S : Set X} (hSm : MeasurableSet S) (hinj : Set.InjOn T S) (himage : ∀ (s : Set X), MeasurableSet s → s ⊆ S → MeasurableSet (T '' s)) {J : X → ENNReal} (hcov : ∀ (s : Set X), MeasurableSet s → s ⊆ S → ∀ (g : X → ENNReal), (ρ.withDensity g) (T '' s) = ∫⁻ (x : X) in s, J x * g (T x) ∂ρ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hac : (MeasureTheory.Measure.map T (μ.restrict S)).AbsolutelyContinuous ρ) : μ.restrict S = ρ.withDensity (S.indicator fun (x : X) => J x * (MeasureTheory.Measure.map T (μ.restrict S)).rnDeriv ρ (T x))

Under the change of variables of map_restrict_absolutelyContinuous_of_withDensity_image_eq, with T injective on S and sending measurable subsets of S to measurable sets, μ restricted to S has density J x * d((T)₊ (μ|S))/dρ (T x) on S.

theorem TauCeti.lintegral_comp_rnDeriv_map_restrict {X : Type u_1} [MeasurableSpace X] (ρ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite ρ] {T : X → X} (hT : Measurable T) {S : Set X} (hSm : MeasurableSet S) (hinj : Set.InjOn T S) (himage : ∀ (s : Set X), MeasurableSet s → s ⊆ S → MeasurableSet (T '' s)) {J : X → ENNReal} (hJm : Measurable J) (hJ : ∀ x ∈ S, J x ≠ 0 ∧ J x ≠ ⊤) (hcov : ∀ (s : Set X), MeasurableSet s → s ⊆ S → ∀ (g : X → ENNReal), (ρ.withDensity g) (T '' s) = ∫⁻ (x : X) in s, J x * g (T x) ∂ρ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hac : (MeasureTheory.Measure.map T (μ.restrict S)).AbsolutelyContinuous ρ) {Φ : ENNReal → ENNReal} (hΦ : Φ 0 = 0) : ∫⁻ (y : X), Φ ((MeasureTheory.Measure.map T (μ.restrict S)).rnDeriv ρ y) ∂ρ = ∫⁻ (x : X) in S, J x * Φ (μ.rnDeriv ρ x / J x) ∂ρ

Under the hypotheses of restrict_eq_withDensity_indicator_rnDeriv_map_restrict, with J positive and finite on S, integrals of a function Φ with Φ 0 = 0 of the density of (T)₊ (μ|S) are integrals over S: ∫ Φ (d((T)₊ (μ|S))/dρ) dρ = ∫_S J x * Φ (dμ/dρ (x) / J x) dρ.