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

• MeasureTheory.condExp_indep_eq: If m₁, m₂ are independent σ-algebras and f is an m₁-measurable function, then 𝔼[f | m₂] = 𝔼[f] almost everywhere.

theorem MeasureTheory.condExp_indep_eq {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m₁ m₂ m : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → E} (hle₁ : m₁ ≤ m) (hle₂ : m₂ ≤ m) [SigmaFinite (μ.trim hle₂)] (hf : StronglyMeasurable f) (hindp : ProbabilityTheory.Indep m₁ m₂ μ) : μ[f|m₂] =ᶠ[ae μ] fun (x : Ω) => ∫ (x : Ω), f x ∂μ

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