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 ∂μ ≠ ⊤) : (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.

theorem MeasureTheory.condLExp_ofReal {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} {f : 𝓧 → ℝ} (hf : Integrable f μ) (h'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.

theorem MeasureTheory.condLExp_enorm {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} {f : 𝓧 → ℝ} (hf : Integrable f μ) (h'f : 0 ≤ᵐ[μ] f) : μ⁻[fun (x : 𝓧) => ‖f x‖ₑ | m] =ᵐ[μ] fun (x : 𝓧) => ‖μ[f | m] x‖ₑ

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

theorem MeasureTheory.lintegral_enorm_condExp_indicator {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} (hm : m ≤ m𝓧) {μ : Measure 𝓧} [SigmaFinite (μ.trim hm)] {s : Set 𝓧} (hs : MeasurableSet s) (h's : μ s ≠ ⊤ := by finiteness) : ∫⁻ (a : 𝓧), ‖μ[s.indicator 1 | m] a‖ₑ ∂μ = μ s