Pair-Law Equality from Contractability

This file proves the key pair-law equality: for a contractable sequence X, the pair (U, W) has the same distribution as (U, W') where:

• U = first r coordinates
• W = future tail from m+1
• W' = X_r consed onto W

This is fundamental to the martingale approach proof of de Finetti's theorem.

Main definitions

• phi0, phi1 - Strictly increasing injections for contractability argument

Main results

• pair_law_eq_of_contractable - The key pair-law equality (U, W) =^d (U, W')
• condExp_indicator_eq_of_contractable - CE drop-info via contraction
• comap_consRV_eq_sup - σ(consRV x t) = σ(x) ⊔ σ(t)
• condExp_Xr_indicator_eq_of_contractable - CE drop-info for X_r indicator

These are extracted from ViaMartingale.lean to enable modular imports.

Pair-Law Equality from Contractability

The key step: use two strictly increasing injections to show that (U, W) =^d (U, W') where W' = consRV (X r) W.

Setup for r ≤ m:

• U := first r coordinates = (X 0, ..., X (r-1))
• W := future tail from m+1 = shiftRV X (m+1) = (X (m+1), X (m+2), ...)
• W' := cons of X_r onto W = consRV (X r) W = (X r, X (m+1), X (m+2), ...)

Two increasing injections (both of length r + ∞):

• φ₀: 0, 1, ..., r-1, m+1, m+2, ... (skips indices r through m)
• φ₁: 0, 1, ..., r-1, r, m+1, m+2, ... (skips indices r+1 through m)

By contractability, both give the same joint distribution. Projecting:

• φ₀ gives (U, W)
• φ₁ gives (U, W')

Hence (U, W) =^d (U, W'). Combined with σ(W) ≤ σ(W') from comap_le_comap_consRV, Kallenberg 1.3 gives U ⊥⊥ X_r | W.

def Exchangeability.DeFinetti.ViaMartingale.phi0 (r m : ℕ) : ℕ → ℕ

Injection φ₀ for contractability: indices 0,...,r-1, m+1, m+2, ... Skips indices r through m.

Equations

• Exchangeability.DeFinetti.ViaMartingale.phi0 r m n = if n < r then n else n + (m - r + 1)

def Exchangeability.DeFinetti.ViaMartingale.phi1 (r m : ℕ) : ℕ → ℕ

Injection φ₁ for contractability: indices 0,...,r, m+1, m+2, ... Skips indices r+1 through m.

Equations

• Exchangeability.DeFinetti.ViaMartingale.phi1 r m n = if n ≤ r then n else n + (m - r)

theorem Exchangeability.DeFinetti.ViaMartingale.phi0_strictMono (r m : ℕ) (_hr : r ≤ m) : StrictMono (phi0 r m)

theorem Exchangeability.DeFinetti.ViaMartingale.phi1_strictMono (r m : ℕ) (_hr : r ≤ m) : StrictMono (phi1 r m)

theorem Exchangeability.DeFinetti.ViaMartingale.phi0_phi1_agree_on_first_r (r m i : ℕ) (hi : i < r) : phi0 r m i = phi1 r m i

φ₀ and φ₁ agree on indices 0,...,r-1 (the first r coordinates).

theorem Exchangeability.DeFinetti.ViaMartingale.phi0_at_r (r m : ℕ) (hr : r ≤ m) : phi0 r m r = m + 1

φ₀ at index r gives m+1 (start of future tail).

theorem Exchangeability.DeFinetti.ViaMartingale.phi1_at_r (r m : ℕ) : phi1 r m r = r

φ₁ at index r gives r (the extra coordinate in W').

theorem Exchangeability.DeFinetti.ViaMartingale.phi1_after_r (r m k : ℕ) (hr : r ≤ m) : phi1 r m (r + 1 + k) = m + 1 + k

φ₁ at index r+1+k gives m+1+k (same as φ₀ at index r+k).

theorem Exchangeability.DeFinetti.ViaMartingale.pair_law_eq_of_contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX : ∀ (n : ℕ), Measurable (X n)) (r m : ℕ) (hr : r ≤ m) : have U := fun (ω : Ω) (i : Fin r) => X (↑i) ω; have W := shiftRV X (m + 1); have W' := consRV (fun (ω : Ω) => X r ω) W; MeasureTheory.Measure.map (fun (ω : Ω) => (U ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (U ω, W' ω)) μ

Key lemma: Contractability gives pair-law equality (U, W) =^d (U, W').

Given a contractable sequence X:

• U is the first r coordinates: (X 0, ..., X (r-1))
• W is the future tail from m+1: shiftRV X (m+1)
• W' is X_r consed onto W: consRV (X r) (shiftRV X (m+1))

Then (U, W) =^d (U, W') because both arise from strictly increasing subsequences of the same length (via φ₀ and φ₁).

This is the pair-law hypothesis needed for Kallenberg 1.3.

Proof strategy:

1. Embed (Fin r → α) × (ℕ → α) into (ℕ → α) via concatenation
2. Show (U, W) and (U, W') map to reindexings of X via φ₀ and φ₁
3. By contractability, these reindexings have equal finite marginals
4. By π-system uniqueness, the embedded measures are equal
5. Pull back to show (U, W) =^d (U, W')

theorem Exchangeability.DeFinetti.ViaMartingale.condExp_indicator_eq_of_contractable {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m : ℕ} (hrm : r ≤ m) {A : Set (Fin r → α)} (hA : MeasurableSet A) : have U := fun (ω : Ω) (i : Fin r) => X (↑i) ω; have W := shiftRV X (m + 1); have W' := consRV (fun (ω : Ω) => X r ω) W; μ[(U ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W' inferInstance] =ᵐ[μ] μ[(U ⁻¹' A).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance]

Conditional expectation drop-info via true contraction (Kallenberg 1.3).

This is the CORRECT version that uses the contraction structure σ(W) ⊆ σ(W') rather than the broken triple-law approach.

Given contractability of X, for r < m:

• U = (X_0, ..., X_{r-1}) (first r coordinates)
• W = shiftRV X (m+1) (far future)
• W' = consRV (X r) W (X_r consed onto far future)

We have:

1. σ(W) ⊆ σ(W') via comap_le_comap_consRV
2. (U, W) =^d (U, W') via pair_law_eq_of_contractable

By Kallenberg Lemma 1.3 (condExp_indicator_eq_of_law_eq_of_comap_le): E[1_{U∈A} | σ(W')] = E[1_{U∈A} | σ(W)]

Since σ(W') = σ(X_r, W), this gives: E[1_{U∈A} | σ(X_r, W)] = E[1_{U∈A} | σ(W)]

which is exactly U ⊥⊥ X_r | W in indicator form.

theorem Exchangeability.DeFinetti.ViaMartingale.comap_consRV_eq_sup {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (x : Ω → α) (t : Ω → ℕ → α) : MeasurableSpace.comap (consRV x t) inferInstance = MeasurableSpace.comap x inferInstance ⊔ MeasurableSpace.comap t inferInstance

The σ-algebra of W' = consRV (X r) W equals the join of σ(X_r) and σ(W).

This is key for translating the Kallenberg 1.3 result to conditional independence.

Proof idea:

• (≤): Any set in σ(consRV x t) is the preimage of a measurable set in ℕ → α. Coordinate 0 gives σ(x), coordinates 1,2,... give σ(t), so it's in the join.
• (≥): x = (consRV x t) ∘ π₀ and t = tailRV (consRV x t), so both σ(x) and σ(t) are contained in σ(consRV x t).

theorem Exchangeability.DeFinetti.ViaMartingale.condExp_Xr_indicator_eq_of_contractable {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m : ℕ} (hrm : r ≤ m) {B : Set α} (hB : MeasurableSet B) : have Y := X r; have U := fun (ω : Ω) (i : Fin r) => X (↑i) ω; have W := shiftRV X (m + 1); μ[(Y ⁻¹' B).indicator fun (x : Ω) => 1|MeasurableSpace.comap U inferInstance ⊔ MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[(Y ⁻¹' B).indicator fun (x : Ω) => 1|MeasurableSpace.comap W inferInstance]

Conditional expectation drop-info for X_r-indicator via true contraction.

This is the key lemma for restructuring block_coord_condIndep. Given contractability of X, for r < m and B ∈ σ(X_r):

E[1_{X_r ∈ B} | σ(U, W)] = E[1_{X_r ∈ B} | σ(W)]

where U = firstRMap X r and W = shiftRV X (m+1).

Proof strategy: The direct Kallenberg 1.3 approach has type issues (W and W' need the same type). Two correct approaches:

1. Use pair_law_eq_of_contractable with (U, W) =^d (U, W') where W' = consRV(X_r, W), then translate via σ(W') = σ(X_r) ⊔ σ(W) (from comap_consRV_eq_sup). This gives E[f(U) | σ(X_r, W)] = E[f(U) | σ(W)], i.e., U ⊥⊥ X_r | W. By symmetry of CI, this gives X_r ⊥⊥ U | W which is the goal.
2. Embed into a common type space by viewing W as a tuple (default, W) to match W' = (U, W).