Lag-Constancy Infrastructure for ViaKoopman Proof

This file contains lag-constancy lemmas for the Koopman-based de Finetti proof:

• condexp_pullback_factor - CE pullback along factor maps
• LagConstancyProof section with permutation lemmas
• setIntegral_eq_of_reindex_eq - Set integral equality via reindexing
• condExp_ae_eq_of_setIntegral_diff_eq_zero - CE equality from set integral equality
• condexp_lag_constant_from_exchangeability - Main lag-constancy result

All lemmas in this file are proved (no sorries).

Extracted from: Infrastructure.lean (Part 2/3) Status: Complete (no sorries in proofs)

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_pullback_factor {Ω : Type u_2} {Ω' : Type u_3} [inst : MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure μ'] (g : Ω' → Ω) (hg : Measurable g) (hpush : MeasureTheory.Measure.map g μ' = μ) {H : Ω → ℝ} (hH : MeasureTheory.Integrable H μ) (m : MeasurableSpace Ω) (hm : m ≤ inst) : (fun (ω' : Ω') => μ[H|m] (g ω')) =ᵐ[μ'] μ'[H ∘ g|MeasurableSpace.comap g m]

Factor-map pullback for conditional expectation.

If g : Ω' → Ω is a factor map (i.e., map g μ' = μ), then conditional expectation pulls back correctly: CE[H | 𝒢] ∘ g = CE[H ∘ g | comap g 𝒢] a.e.

This is the key lemma for transporting conditional expectations between spaces.

Lag-Constancy from Exchangeability: The Transposition Argument

This section proves that exchangeability implies lag-constancy for conditional expectations. The proof uses Kallenberg's transposition argument:

1. For k ≥ 1, the transposition τ = swap(k, k+1) fixes index 0
2. Exchangeability gives measure invariance under reindex τ
3. Shift-invariant sets are preserved by reindex τ (they depend only on tails)
4. Therefore CE[f(ω₀)·g(ω_{k+1}) | ℐ] = CE[f(ω₀)·g(ω_k) | ℐ]

Key lemmas:

• shift_reindex_swap_eq: For m > k+1, shift^m ∘ reindex τ = shift^m
• reindex_swap_preimage_shiftInvariant: Shift-invariant sets are τ-invariant
• condexp_lag_constant_from_exchangeability: The main result

theorem Exchangeability.DeFinetti.ViaKoopman.reindex_swap_preimage_shiftInvariant {α : Type u_2} [MeasurableSpace α] (k : ℕ) (s : Set (ℕ → α)) (hs : isShiftInvariant s) : reindex (Equiv.swap k (k + 1)) ⁻¹' s = s

Preimages of shift-invariant sets under reindex (swap k (k+1)) are the same set.

Proof strategy: A set s is shift-invariant iff membership depends only on tails. Since swap k (k+1) only affects coordinates k and k+1, for any n > k+1, the n-tail of ω equals the n-tail of (reindex τ ω). By shift-invariance, membership in s is determined by any tail, hence ω ∈ s ↔ (reindex τ ω) ∈ s.

theorem Exchangeability.DeFinetti.ViaKoopman.reindex_perm_preimage_shiftInvariant {α : Type u_2} [MeasurableSpace α] (π : Equiv.Perm ℕ) (M : ℕ) (h_id_beyond : ∀ (n : ℕ), M ≤ n → π n = n) (s : Set (ℕ → α)) (hs : isShiftInvariant s) : reindex π ⁻¹' s = s

Generalized reindex preimage invariance: For any permutation π that is identity beyond some bound M, shift-invariant sets are reindex-invariant.

This generalizes reindex_swap_preimage_shiftInvariant from transpositions to arbitrary finite-support permutations. The proof uses the same key insight: shift^[M] commutes with reindex π when π is identity beyond M, so membership in shift-invariant sets is preserved.

Cycle permutation for lag constancy

def Exchangeability.DeFinetti.ViaKoopman.cycleShiftDown (L R : ℕ) (hLR : L ≤ R) : Equiv.Perm ℕ

A cycle on [L, R] that maps n → n-1 (for L < n ≤ R) and L → R. This is useful for proving lag constancy of cylinder sets: it shifts coordinates down by 1 within the range, wrapping L to R.

Equations

• One or more equations did not get rendered due to their size.

theorem Exchangeability.DeFinetti.ViaKoopman.cycleShiftDown_lt (L R n : ℕ) (hLR : L ≤ R) (hn : n < L) : (cycleShiftDown L R hLR) n = n

theorem Exchangeability.DeFinetti.ViaKoopman.cycleShiftDown_gt (L R n : ℕ) (hLR : L ≤ R) (hn : R < n) : (cycleShiftDown L R hLR) n = n

theorem Exchangeability.DeFinetti.ViaKoopman.cycleShiftDown_sub (L R n : ℕ) (hLR : L ≤ R) (hLn : L < n) (hnR : n ≤ R) : (cycleShiftDown L R hLR) n = n - 1

theorem Exchangeability.DeFinetti.ViaKoopman.cycleShiftDown_L (L R : ℕ) (hLR : L ≤ R) : (cycleShiftDown L R hLR) L = R

theorem Exchangeability.DeFinetti.ViaKoopman.cycleShiftDown_id_beyond (L R : ℕ) (hLR : L ≤ R) (n : ℕ) (hn : R < n) : (cycleShiftDown L R hLR) n = n

The cycle is identity beyond R.

Disjoint offset swap permutation

For shifting cylinders from coords {i : i ∈ S} to {offset + i : i ∈ S} while fixing coords outside. This is used in h_shift_to_N₀ to show CE[φ(ω_k) · 1_B | mSI] = CE[φ(ω_k) · 1_{B_at N₀} | mSI].

def Exchangeability.DeFinetti.ViaKoopman.disjointOffsetSwap (S : Finset ℕ) (offset : ℕ) (hS : ∀ i ∈ S, i < offset) : Equiv.Perm ℕ

Permutation that swaps i ↔ offset+i for all i in a finite set S, where all elements of S are less than offset. This is an involution.

Equations

• One or more equations did not get rendered due to their size.

theorem Exchangeability.DeFinetti.ViaKoopman.disjointOffsetSwap_mem (S : Finset ℕ) (offset : ℕ) (hS : ∀ i ∈ S, i < offset) (i : ℕ) (hi : i ∈ S) : (disjointOffsetSwap S offset hS) i = offset + i

disjointOffsetSwap maps i to offset + i for i ∈ S.

theorem Exchangeability.DeFinetti.ViaKoopman.disjointOffsetSwap_offset_mem (S : Finset ℕ) (offset : ℕ) (hS : ∀ i ∈ S, i < offset) (i : ℕ) (hi : i ∈ S) : (disjointOffsetSwap S offset hS) (offset + i) = i

disjointOffsetSwap maps offset + i to i for i ∈ S.

theorem Exchangeability.DeFinetti.ViaKoopman.disjointOffsetSwap_lt (S : Finset ℕ) (offset : ℕ) (hS : ∀ i ∈ S, i < offset) (n : ℕ) (hn_notin : n ∉ S) (hn_lt : n < offset) : (disjointOffsetSwap S offset hS) n = n

disjointOffsetSwap fixes n when n ∉ S and n < offset.

theorem Exchangeability.DeFinetti.ViaKoopman.disjointOffsetSwap_id_beyond (S : Finset ℕ) (offset : ℕ) (hS : ∀ i ∈ S, i < offset) (n : ℕ) (hn : S.sup id + offset < n) : (disjointOffsetSwap S offset hS) n = n

disjointOffsetSwap is identity beyond offset + max(S).

theorem Exchangeability.DeFinetti.ViaKoopman.setIntegral_eq_of_reindex_eq {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] (τ : Equiv.Perm ℕ) (hμ_inv : MeasureTheory.Measure.map (reindex τ) μ = μ) (F G : (ℕ → α) → ℝ) (hFG : F ∘ reindex τ = G) (hF_meas : Measurable F) (s : Set (ℕ → α)) (hs_meas : MeasurableSet s) (h_preimage : reindex τ ⁻¹' s = s) : ∫ (ω : ℕ → α) in s, F ω ∂μ = ∫ (ω : ℕ → α) in s, G ω ∂μ

For exchangeable measures, set integrals are equal for functions that agree on reindexing. This is a key step in proving lag-constancy: ∫_s F = ∫_s G when F ∘ reindex τ = G and the set s is shift-invariant (hence also reindex-invariant).

theorem Exchangeability.DeFinetti.ViaKoopman.condExp_ae_eq_of_setIntegral_diff_eq_zero {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] {F G : (ℕ → α) → ℝ} (hF_int : MeasureTheory.Integrable F μ) (hG_int : MeasureTheory.Integrable G μ) (h_diff_zero : ∀ (s : Set Ω[α]), MeasurableSet s → μ s < ⊤ → ∫ (ω : ℕ → α) in s, (F - G) ω ∂μ = 0) : μ[F|shiftInvariantSigma] =ᵐ[μ] μ[G|shiftInvariantSigma]

If ∫_s (F - G) = 0 for all s in sub-σ-algebra, then CE[F|m] = CE[G|m] a.e.

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_lag_constant_from_exchangeability {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] (hExch : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) μ = μ) (f g : α → ℝ) (hf_meas : Measurable f) (hf_bd : ∃ (C : ℝ), ∀ (x : α), |f x| ≤ C) (hg_meas : Measurable g) (hg_bd : ∃ (C : ℝ), ∀ (x : α), |g x| ≤ C) (k : ℕ) (hk : 0 < k) : μ[fun (ω : ℕ → α) => f (ω 0) * g (ω (k + 1))|shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : ℕ → α) => f (ω 0) * g (ω k)|shiftInvariantSigma]

Lag-constancy from exchangeability via transpositions (Kallenberg's approach).

For EXCHANGEABLE measures μ on path space, the conditional expectation CE[f(ω₀)·g(ω_{k+1}) | ℐ] equals CE[f(ω₀)·g(ω_k) | ℐ] for k ≥ 1.

Key insight: This uses EXCHANGEABILITY (not just stationarity). The proof is:

1. Let τ be the transposition swapping indices k and k+1
2. Exchangeability gives: Measure.map (reindex τ) μ = μ
3. Since k ≥ 1, τ fixes 0: τ(0) = 0
4. Therefore: CE[f(ω₀)·g(ω_{k+1}) | ℐ] = CE[(f∘τ)(ω₀)·(g∘τ)(ω_{k+1}) | ℐ] = CE[f(ω₀)·g(ω_k) | ℐ]

Why k ≥ 1 is required (CRITICAL):

• When k=0, τ = swap(0, 1) does NOT fix 0 (τ sends 0 ↦ 1)
• So (f∘τ)(ω₀) = f(ω₁) ≠ f(ω₀), breaking the argument
• Counterexample for k=0: i.i.d. Bernoulli(1/2):
  • CE[ω₀·ω₁ | ℐ] = E[ω₀]·E[ω₁] = 1/4
  • CE[ω₀² | ℐ] = E[ω₀²] = 1/2 (since ω₀ ∈ {0,1})
  • These are NOT equal!

Why stationarity alone is NOT enough: Stationary non-exchangeable processes (Markov chains, AR processes) can have lag-dependent conditional correlations. The transposition trick requires the FULL permutation invariance of exchangeability.