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.

theorem pair_law_of_triple_law {Ω : Type u_1} {α : Type u_2} {γ : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace γ] {β : Type u_4} [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} (X : Ω → α) (Y : Ω → β) (W W' : Ω → γ) (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) (hW' : Measurable W') (h_triple : MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω, W' ω)) μ) : MeasureTheory.Measure.map (fun (ω : Ω) => ((X ω, Y ω), W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => ((X ω, Y ω), W' ω)) μ

Helper to extract pair law from triple law.

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

Legacy wrapper: the old condExp_eq_of_triple_law_direct interface.

WARNING: This lemma's original statement was incorrect. It claimed that the triple law (Z,Y,W) =^d (Z,Y,W') alone implies E[φ|σ(Z,W)] = E[φ|σ(W)]. This is FALSE in general.

This wrapper provides backward compatibility but adds the missing contraction hypothesis. If your use case doesn't have this hypothesis, the original claim was invalid and you need to restructure your proof.

The correct statement (Kallenberg 1.3) is condExp_indicator_eq_of_law_eq_of_comap_le: you need σ(W) ≤ σ(W') (W is a contraction of W') to drop from σ(W') to σ(W).