Theorems · Theorem · measure theory

MeasureTheory.toReal_condLExp

∀ {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : 𝓧), f x ∂μ ≠ ⊤ → (fun x => (μ⁻[f | m] x).toReal) =ᵐ[μ] μ[fun x => (f x).toReal | m]

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

2 results in Mathlib

Foundations

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