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.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.