Results about both conditional expectations #
For non-negative real functions, we have two versions of the conditional expectation:
condExp and condLExp, built from the Bochner and Lebesgue integrals respectively.
In this file, we gather results that involve both versions.
Main statements #
MeasureTheory.toReal_condLExp: the two definitions of the conditional expectation agree almost everywhere. That is,(fun x ↦ (μ⁻[f | m] x).toReal) =ᵐ[μ] μ[fun x ↦ (f x).toReal | m].
theorem
MeasureTheory.toReal_condLExp
{𝓧 : Type u_1}
(m : MeasurableSpace 𝓧)
{m𝓧 : MeasurableSpace 𝓧}
{μ : Measure 𝓧}
{f : 𝓧 → ENNReal}
(hf_meas : AEMeasurable f μ)
(hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ⊤)
:
The two definitions of the conditional expectation condExp and condLExp (for Bochner and
Lebesgue integrals respectively) agree almost everywhere.