Theorems · Theorem · measure theory

MeasureTheory.ae_eq_condLExp

∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {Y : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal),
  Measurable Y →
    (∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P) → Y =ᵐ[P] P⁻[X | mΩ]

The conditional (Lebesgue) expectation P⁻[X|mΩ] is defined uniquely as an mΩ-measurable function up to P-ae equality by its (Lebesgue) integral over all mΩ-measurable sets.

Defined in

Mathlib.MeasureTheory.Function.ConditionalLExpectation

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite