Probabilistic properties of the conditional expectation #

This file contains some properties about the conditional expectation which does not belong in the main conditional expectation file.

Main result #

theorem MeasureTheory.condexp_indep_eq {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {m₁ : MeasurableSpace Ω} {m₂ : MeasurableSpace Ω} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ΩE} (hle₁ : m₁ m) (hle₂ : m₂ m) [MeasureTheory.SigmaFinite (μ.trim hle₂)] (hf : MeasureTheory.StronglyMeasurable f) (hindp : ProbabilityTheory.Indep m₁ m₂ μ) :
MeasureTheory.condexp m₂ μ f =ᵐ[μ] fun (x : Ω) => ∫ (x : Ω), f xμ

If m₁, m₂ are independent σ-algebras and f is m₁-measurable, then 𝔼[f | m₂] = 𝔼[f] almost everywhere.