Theorems · Theorem · measure theory

MeasureTheory.rnDeriv_trim

∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} (hm : m ≤ m𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite (ν.trim hm)],
  μ.AbsolutelyContinuous ν →
    (μ.trim hm).rnDeriv (ν.trim hm) =ᵐ[ν.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.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.SigmaFinite