Conditional Independence - Bounded Measurable Extension

This file extends conditional independence from simple functions to bounded measurable functions using L¹ approximation and convergence arguments.

Main results

• condIndep_simpleFunc_left: Simple function → bounded measurable extension (left)
• condIndep_bddMeas_extend_left: Full bounded measurable extension (left)
• condIndep_boundedMeasurable: Conditional independence for bounded measurable functions
• condIndep_of_rect_factorization: Rectangle factorization implies conditional independence

References

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

theorem condIndep_simpleFunc_left {Ω : Type u_5} {α : Type u_6} {β : Type u_7} {γ : Type u_8} {m₀ : MeasurableSpace Ω} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hCI : CondIndep μ Y Z W) (φ : MeasureTheory.SimpleFunc α ℝ) {ψ : β → ℝ} (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) (hψ_meas : Measurable ψ) (Mψ : ℝ) (hψ_bdd : ∀ᵐ (ω : Ω) ∂μ, |ψ (Z ω)| ≤ Mψ) : μ[⇑φ ∘ Y * ψ ∘ Z|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[⇑φ ∘ Y|MeasurableSpace.comap W inferInstance] * μ[ψ ∘ Z|MeasurableSpace.comap W inferInstance]

theorem condIndep_bddMeas_extend_left {Ω : Type u_5} {α : Type u_6} {β : Type u_7} {γ : Type u_8} {m₀ : MeasurableSpace Ω} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hCI : CondIndep μ Y Z W) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) {φ : α → ℝ} {ψ : β → ℝ} (hφ_meas : Measurable φ) (hψ_meas : Measurable ψ) (Mφ Mψ : ℝ) (hφ_bdd : ∀ᵐ (ω : Ω) ∂μ, |φ (Y ω)| ≤ Mφ) (hψ_bdd : ∀ᵐ (ω : Ω) ∂μ, |ψ (Z ω)| ≤ Mψ) : μ[φ ∘ Y * ψ ∘ Z|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[φ ∘ Y|MeasurableSpace.comap W inferInstance] * μ[ψ ∘ Z|MeasurableSpace.comap W inferInstance]

Extend factorization from simple φ to bounded measurable φ, keeping ψ fixed. Refactored to avoid instance pollution: works with σ(W) directly.

theorem condIndep_boundedMeasurable {Ω : 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) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) {φ : α → ℝ} {ψ : β → ℝ} (hφ_meas : Measurable φ) (hψ_meas : Measurable ψ) (Mφ Mψ : ℝ) (hφ_bdd : ∀ᵐ (ω : Ω) ∂μ, |φ (Y ω)| ≤ Mφ) (hψ_bdd : ∀ᵐ (ω : Ω) ∂μ, |ψ (Z ω)| ≤ Mψ) : μ[φ ∘ Y * ψ ∘ Z|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[φ ∘ Y|MeasurableSpace.comap W inferInstance] * μ[ψ ∘ Z|MeasurableSpace.comap W inferInstance]

Conditional independence extends to bounded measurable functions (monotone class).

If Y ⊥⊥_W Z for indicators, then by approximation the factorization extends to all bounded measurable functions.

Mathematical content: For bounded measurable f(Y) and g(Z): E[f(Y)·g(Z)|σ(W)] = E[f(Y)|σ(W)]·E[g(Z)|σ(W)]

Proof strategy: Use monotone class theorem:

1. Simple functions are dense in bounded measurables
2. Conditional expectation is continuous w.r.t. bounded convergence
3. Approximate f, g by simple functions fₙ, gₙ
4. Pass to limit using dominated convergence

This is the key extension that enables proving measurability properties.

Wrapper: Rectangle factorization implies conditional independence

theorem condIndep_of_rect_factorization {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) (hRect : ∀ ⦃A : Set α⦄ ⦃B : Set β⦄, MeasurableSet A → MeasurableSet B → μ[((Y ⁻¹' A).indicator fun (x : Ω) => 1) * (Z ⁻¹' B).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[(Y ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance] * μ[(Z ⁻¹' B).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance]) : CondIndep μ Y Z W

Rectangle factorization implies conditional independence.

This is essentially the identity, since CondIndep is defined as rectangle factorization. This wrapper allows replacing axioms in ViaMartingale.lean with concrete proofs.