Conditional Independence - Projection Theorems

This file proves that conditional independence allows projecting conditional expectations from σ(Z,W) to σ(W).

Main results

• condExp_project_of_condIndep: When Y ⊥⊥_W Z, conditioning on (Z,W) gives the same result as conditioning on W alone for indicator functions of Y.

Key insight

Conditional independence means that knowing Z provides no additional information about Y beyond what W already provides. Therefore E[f(Y)|σ(Z,W)] = E[f(Y)|σ(W)].

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Section 6.1

theorem condExp_project_of_condIndep {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) (h_indep : CondIndep μ Y Z W) {A : Set α} (hA : MeasurableSet A) : μ[(Y ⁻¹' A).indicator fun (x : Ω) => 1 | MeasurableSpace.comap (fun (ω : Ω) => (Z ω, W ω)) inferInstance] =ᵐ[μ] μ[(Y ⁻¹' A).indicator fun (x : Ω) => 1 | MeasurableSpace.comap W inferInstance]

Conditional expectation projection from conditional independence (helper).

When Y ⊥⊥_W Z, conditioning on (Z,W) gives the same result as conditioning on W alone for indicator functions of Y.

This is a key technical lemma used to prove the main projection theorem.

Kallenberg 1.3: Indicator Conditional Independence from Drop-Info

Infrastructure for deriving conditional independence from distributional equality via the "drop information" property for Y.

Note: Helper lemmas integrable_mul_of_bound_one and condExp_indicator_ae_bound_one are available from CondExpHelpers.lean.