Radon-Nikodym derivatives and conditional expectations

We express the Radon-Nikodym derivative of the pushforward of measures in terms of the conditional expectation of the Radon-Nikodym derivative of the original measures.

Main statements

In all statements, μ and ν are measures with μ ≪ ν.

• rnDeriv_map: the Radon-Nikodym derivative ∂(μ.map g)/∂(ν.map g) of the pushforward of measures by a function g : 𝓧 → 𝓨 evaluated at g x is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the comap by g of the sigma-algebra on 𝓨.
• rnDeriv_trim: the Radon-Nikodym derivative ∂(μ.trim hm)/∂(ν.trim hm) of the trimmed measures (for hm : m ≤ m0 stating that m is a sub-sigma-algebra of m0) is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the sigma-algebra m.

We have two versions of the above statements, one with a.e. equality to the conditional expectation condLExp built from the Lebesgue integral, and one with a.e. equality to the conditional expectation condExp built from the Bochner integral.

theorem MeasureTheory.toReal_rnDeriv_map {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] (hμν : μ.AbsolutelyContinuous ν) {g : 𝓧 → 𝓨} (hg : Measurable g) [hσ : SigmaFinite (Measure.map g ν)] : (fun (a : 𝓧) => ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᶠ[ae ν] ν[fun (a : 𝓧) => (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

The Radon-Nikodym derivative ∂(μ.map g)/∂(ν.map g) of the pushforward of measures by a function g : 𝓧 → 𝓨 evaluated at g x is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the comap by g of the sigma-algebra on 𝓨.

See toReal_rnDeriv_map_ae_eq_trim for the same statement, but with a.e. equality with respect to the trimmed measure ν.trim hg.comap_le.

theorem MeasureTheory.rnDeriv_map {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] (hμν : μ.AbsolutelyContinuous ν) {g : 𝓧 → 𝓨} (hg : Measurable g) [hσ : SigmaFinite (Measure.map g ν)] : (fun (a : 𝓧) => (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᶠ[ae ν] ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]

The Radon-Nikodym derivative ∂(μ.map g)/∂(ν.map g) of the pushforward of measures by a function g : 𝓧 → 𝓨 evaluated at g x is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the comap by g of the sigma-algebra on 𝓨.

See rnDeriv_map_ae_eq_trim for the same statement, but with a.e. equality with respect to the trimmed measure ν.trim hg.comap_le.

theorem MeasureTheory.rnDeriv_map_ae_eq_trim {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] (hμν : μ.AbsolutelyContinuous ν) {g : 𝓧 → 𝓨} (hg : Measurable g) [SigmaFinite (Measure.map g ν)] : (fun (a : 𝓧) => (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᶠ[ae (ν.trim ⋯)] ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]

The Radon-Nikodym derivative ∂(μ.map g)/∂(ν.map g) of the pushforward of measures by a function g : 𝓧 → 𝓨 evaluated at g x is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the comap by g of the sigma-algebra on 𝓨.

See rnDeriv_map for the same statement, but with a.e. equality with respect to the measure ν.

theorem MeasureTheory.toReal_rnDeriv_map_ae_eq_trim {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : Measure 𝓧} [IsFiniteMeasure μ] (hμν : μ.AbsolutelyContinuous ν) {g : 𝓧 → 𝓨} (hg : Measurable g) [SigmaFinite (Measure.map g ν)] : (fun (a : 𝓧) => ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᶠ[ae (ν.trim ⋯)] ν[fun (a : 𝓧) => (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

The Radon-Nikodym derivative ∂(μ.map g)/∂(ν.map g) of the pushforward of measures by a function g : 𝓧 → 𝓨 evaluated at g x is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the comap by g of the sigma-algebra on 𝓨.

See toReal_rnDeriv_map for the same statement, but with a.e. equality with respect to the measure ν.

theorem MeasureTheory.toReal_rnDeriv_trim {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (hm : m ≤ m𝓧) [IsFiniteMeasure μ] [hsf : SigmaFinite (ν.trim hm)] (hμν : μ.AbsolutelyContinuous ν) : (fun (x : 𝓧) => ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) =ᶠ[ae (ν.trim hm)] ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | m]

The Radon-Nikodym derivative ∂(μ.trim hm)/∂(ν.trim hm) of the trimmed measures (for hm : m ≤ m0 stating that m is a sub-sigma-algebra of m0) is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the sigma-algebra m.

theorem MeasureTheory.rnDeriv_trim {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : Measure 𝓧} (hm : m ≤ m𝓧) [IsFiniteMeasure μ] [SigmaFinite (ν.trim hm)] (hμν : μ.AbsolutelyContinuous ν) : (μ.trim hm).rnDeriv (ν.trim hm) =ᶠ[ae (ν.trim hm)] fun (x : 𝓧) => ENNReal.ofReal (ν[fun (x : 𝓧) => (μ.rnDeriv ν x).toReal | m] x)

The Radon-Nikodym derivative ∂(μ.trim hm)/∂(ν.trim hm) of the trimmed measures (for hm : m ≤ m0 stating that m is a sub-sigma-algebra of m0) is a.e.-equal to the conditional expectation of ∂μ/∂ν with respect to the sigma-algebra m.