Kallenberg 1.3 Indicator Conditional Independence #

This file provides infrastructure for proving conditional independence from the "drop-info" property, which is Kallenberg Lemma 1.3.

Main results #

condIndep_indicator_of_dropInfoY: Drop-info implies indicator conditional independence

Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Lemma 1.3

theorem condIndep_indicator_of_dropInfoY {Ω : Type u_5} [inst_mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Y Z W : Ω → ℝ} {mW : MeasurableSpace Ω} (_hmW_le : mW ≤ inst_mΩ) (hmW_le_mZW : mW ≤ MeasurableSpace.comap (fun (ω : Ω) => (Z ω, W ω)) inferInstance) (dropY : ∀ (A : Set ℝ), MeasurableSet A → μ[fun (ω : Ω) => (Y ⁻¹' A).indicator (fun (x : Ω) => 1) ω|MeasurableSpace.comap (fun (ω : Ω) => (Z ω, W ω)) inferInstance] =ᵐ[μ] μ[fun (ω : Ω) => (Y ⁻¹' A).indicator (fun (x : Ω) => 1) ω|mW]) (hY : Measurable Y) (hZ : Measurable Z) (hW : Measurable W) {A B : Set ℝ} (hA : MeasurableSet A) (hB : MeasurableSet B) :

μ[fun (ω : Ω) => (Y ⁻¹' A).indicator (fun (x : Ω) => 1) ω * (Z ⁻¹' B).indicator (fun (x : Ω) => 1) ω|mW] =ᵐ[μ] μ[fun (ω : Ω) => (Y ⁻¹' A).indicator (fun (x : Ω) => 1) ω|mW] * μ[fun (ω : Ω) => (Z ⁻¹' B).indicator (fun (x : Ω) => 1) ω|mW]

From drop‑info for Y to indicator conditional independence.

Assume for all Borel A we have condExp μ (σ[Z,W]) (1_A ∘ Y) =ᵐ condExp μ (σ[W]) (1_A ∘ Y). Then for all Borel A,B:

E[ 1_A(Y) 1_B(Z) | σ(W) ] = E[ 1_A(Y) | σ(W) ] * E[ 1_B(Z) | σ(W) ] a.e.