Theorems · Theorem · measure theory

MeasureTheory.rnDeriv_map

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

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.SigmaFinite