Theorems · Theorem · measure theory

MeasureTheory.condLExp_ofReal

∀ {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ᵐ[μ] f → μ⁻[fun x => ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x => ENNReal.ofReal (μ[f | m] x)

The two definitions of the conditional expectation condExp and condLExp (for Bochner and Lebesgue integrals respectively) agree almost everywhere.

Defined in

Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Cited by

1 results in Mathlib

Foundations

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