Theorems · Theorem · measure theory

MeasureTheory.rnDeriv_map_ae_eq_trim

∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ],
  μ.AbsolutelyContinuous ν →
    ∀ {g : 𝓧 → 𝓨} (hg : Measurable g) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)],
      (fun a => (MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)) =ᵐ[ν.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 ν.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Cited by

0 results in Mathlib

Foundations

Depth 301 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.SigmaFinite