Kallenberg Lemma 1.3: Drop-Info Property via Contraction

This file implements Kallenberg (2005), Lemma 1.3, the "contraction-independence" lemma.

Main Results

• condExp_indicator_eq_of_law_eq_of_comap_le: If (X,W) =^d (X,W') and σ(W) ⊆ σ(W'), then E[1_{X∈A}|σ(W')] = E[1_{X∈A}|σ(W)] a.e.

Mathematical Background

Kallenberg's Lemma 1.3 (Contraction-Independence):

Given random elements ξ, η, ζ where:

1. (ξ, η) =^d (ξ, ζ) (pair laws match)
2. σ(η) ⊆ σ(ζ) (η is a contraction of ζ — i.e., η = f ∘ ζ for some measurable f)

Conclusion: P[ξ ∈ B | ζ] = P[ξ ∈ B | η] a.s.

The intuition: conditioning on the finer σ-algebra σ(ζ) gives the same result as conditioning on the coarser σ-algebra σ(η), because the "extra" information in ζ beyond η doesn't change the relationship with ξ (due to the pair law equality).

References

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

theorem condExp_indicator_eq_of_law_eq_of_comap_le {Ω : Type u_1} {α : Type u_2} {γ : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → α) (W W' : Ω → γ) (hX : Measurable X) (hW : Measurable W) (hW' : Measurable W') (h_law : MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, W' ω)) μ) (h_le : MeasurableSpace.comap W inferInstance ≤ MeasurableSpace.comap W' inferInstance) {A : Set α} (hA : MeasurableSet A) : μ[(X ⁻¹' A).indicator fun (x : Ω) => 1 | MeasurableSpace.comap W' inferInstance] =ᵐ[μ] μ[(X ⁻¹' A).indicator fun (x : Ω) => 1 | MeasurableSpace.comap W inferInstance]

Kallenberg Lemma 1.3 (Contraction-Independence).

If (X,W) =^d (X,W') (pair laws equal) and σ(W) ⊆ σ(W') (W is a contraction of W'), then conditioning an indicator of X on σ(W') equals conditioning on σ(W).

This is the "drop information from finer to coarser σ-algebra" property.

Proof: L²/martingale argument.

1. Let μ₁ := E[φ|σ(W)] and μ₂ := E[φ|σ(W')] where φ = 1_{X∈A}
2. Tower: μ₁ = E[μ₂|σ(W)] (since σ(W) ≤ σ(W'))
3. Law equality: E[μ₁²] = E[μ₂²] (from pair law)
4. Compute: E[(μ₂-μ₁)²] = E[μ₂²] - 2E[μ₂μ₁] + E[μ₁²] = E[μ₂²] - 2E[E[μ₂|σ(W)]·μ₁] + E[μ₁²] (tower) = E[μ₂²] - 2E[μ₁²] + E[μ₁²] = E[μ₂²] - E[μ₁²] = 0
5. So μ₂ = μ₁ a.e.