Conditional Independence - Extension from Indicators to Simple Functions

This file extends conditional independence from indicator functions to simple functions, which is the first step toward the full monotone class extension to bounded measurables.

Main results

• condIndep_of_indep_pair: Independence Y ⊥ Z plus (Y,Z) ⊥ W implies Y ⊥⊥_W Z
• condIndep_simpleFunc: Factorization extends to simple functions

References

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

Conditional independence from unconditional independence

theorem condIndep_of_indep_pair {Ω : 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) (hYZ_indep : ProbabilityTheory.IndepFun Y Z μ) (hPairW_indep : ProbabilityTheory.IndepFun (fun (ω : Ω) => (Y ω, Z ω)) W μ) : CondIndep μ Y Z W

Extension to simple functions and bounded measurables (§C2)

theorem condIndep_indicator {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hCI : CondIndep μ Y Z W) (c : ℝ) (A : Set α) (hA : MeasurableSet A) (d : ℝ) (B : Set β) (hB : MeasurableSet B) : μ[(A.indicator fun (x : α) => c) ∘ Y * (B.indicator fun (x : β) => d) ∘ Z|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[(A.indicator fun (x : α) => c) ∘ Y|MeasurableSpace.comap W inferInstance] * μ[(B.indicator fun (x : β) => d) ∘ Z|MeasurableSpace.comap W inferInstance]

Base case: Factorization for scaled indicators.

For φ = c • 1_A and ψ = d • 1_B, the factorization follows by extracting scalars and applying the CondIndep definition.

theorem condIndep_indicator_simpleFunc {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hCI : CondIndep μ Y Z W) (c : ℝ) (A : Set α) (hA : MeasurableSet A) (ψ : MeasureTheory.SimpleFunc β ℝ) (hY : Measurable Y) (hZ : Measurable Z) : μ[(A.indicator fun (x : α) => c) ∘ Y * ⇑ψ ∘ Z|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[(A.indicator fun (x : α) => c) ∘ Y|MeasurableSpace.comap W inferInstance] * μ[⇑ψ ∘ Z|MeasurableSpace.comap W inferInstance]

Factorization for simple functions (both arguments).

If Y ⊥⊥_W Z for indicators, extend to simple functions via linearity. Uses single induction avoiding nested complexity.

theorem condIndep_simpleFunc {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hCI : CondIndep μ Y Z W) (φ : MeasureTheory.SimpleFunc α ℝ) (ψ : MeasureTheory.SimpleFunc β ℝ) (hY : Measurable Y) (hZ : Measurable Z) : μ[⇑φ ∘ Y * ⇑ψ ∘ Z|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[⇑φ ∘ Y|MeasurableSpace.comap W inferInstance] * μ[⇑ψ ∘ Z|MeasurableSpace.comap W inferInstance]