Generalized Lag-Constancy and Two-Sided Infrastructure

This file contains advanced infrastructure for the Koopman-based de Finetti proof:

• Two-sided extension lemmas for bi-infinite path spaces
• condexp_precomp_iterate_eq_twosided - CE invariance under two-sided shifts
• condexp_lag_constant_product - Generalized lag constancy for products
• condexp_lag_constant_product_general - Full generalization at arbitrary coordinates
• Conditional expectation helper lemmas (L¹-Lipschitz, pullout)

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

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

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_precomp_iterate_eq_twosided {α : Type u_1} [MeasurableSpace α] {μhat : MeasureTheory.Measure Ωℤ[α]} [MeasureTheory.IsProbabilityMeasure μhat] (hσ : MeasureTheory.MeasurePreserving shiftℤ μhat μhat) {k : ℕ} {f : Ωℤ[α] → ℝ} (hf : MeasureTheory.Integrable f μhat) : μhat[fun (ω : Ωℤ[α]) => f (shiftℤ^[k] ω) | shiftInvariantSigmaℤ] =ᵐ[μhat] μhat[f | shiftInvariantSigmaℤ]

theorem Exchangeability.DeFinetti.ViaKoopman.Integrable.of_abs_bounded {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ} (hg : MeasureTheory.Integrable g μ) (C : ℝ) (h_bound : ∀ (ω : Ω), |f ω| ≤ C) (hfg_meas : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω * g ω) μ) : MeasureTheory.Integrable (fun (ω : Ω) => f ω * g ω) μ

Integrability of f * g when g is integrable and |f| ≤ C.

This shows that multiplying an integrable function by a bounded function preserves integrability. The bound |f * g| ≤ C * |g| follows from |f| ≤ C.

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_lag_constant_product {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] (hExch : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) μ = μ) (n : ℕ) (fs : Fin n → α → ℝ) (hfs_meas : ∀ (i : Fin n), Measurable (fs i)) (hfs_bd : ∀ (i : Fin n), ∃ (C : ℝ), ∀ (x : α), |fs i x| ≤ C) (g : α → ℝ) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) (k : ℕ) (hk : n ≤ k) : μ[fun (ω : ℕ → α) => (∏ i : Fin n, fs i (ω ↑i)) * g (ω (k + 1)) | shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : ℕ → α) => (∏ i : Fin n, fs i (ω ↑i)) * g (ω k) | shiftInvariantSigma]

Generalized lag-constancy for products (extends condexp_lag_constant_from_exchangeability).

For EXCHANGEABLE measures μ on path space, if P = ∏{i<n} f_i(ω_i) is a product of the first n coordinates and g : α → ℝ is bounded measurable, then for k ≥ n: CE[P · g(ω{k+1}) | mSI] = CE[P · g(ω_k) | mSI]

Proof: Uses transposition τ = swap(k, k+1). Since k ≥ n, τ fixes all indices < n. Therefore P is unchanged by reindex τ, while g(ω_{k+1}) becomes g(ω_k). Exchangeability then gives the result.

Key insight: This generalizes the pair case where P = f(ω_0) and n = 1.

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_lag_constant_product_general {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] (hExch : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) μ = μ) (n : ℕ) (fs : Fin n → α → ℝ) (coords : Fin n → ℕ) (hfs_meas : ∀ (i : Fin n), Measurable (fs i)) (hfs_bd : ∀ (i : Fin n), ∃ (C : ℝ), ∀ (x : α), |fs i x| ≤ C) (g : α → ℝ) (hg_meas : Measurable g) (hg_bd : ∃ (Cg : ℝ), ∀ (x : α), |g x| ≤ Cg) (j : ℕ) (hj : ∀ (i : Fin n), coords i < j) : μ[fun (ω : ℕ → α) => (∏ i : Fin n, fs i (ω (coords i))) * g (ω (j + 1)) | shiftInvariantSigma] =ᵐ[μ] μ[fun (ω : ℕ → α) => (∏ i : Fin n, fs i (ω (coords i))) * g (ω j) | shiftInvariantSigma]

Generalized lag constancy for products at arbitrary coordinates.

This extends condexp_lag_constant_product to products at general coordinates k_0, ..., k_{n-1}. For j, j+1 both larger than all k_i, the transposition τ = swap(j, j+1) fixes all coordinates in the product, so the conditional expectation is unchanged.

Key observation: If M = max(k_i) + 1, then for all j ≥ M:

• τ = swap(j, j+1) fixes all indices 0, 1, ..., j-1
• In particular, τ fixes all k_i (since k_i < M ≤ j)
• Therefore P ∘ reindex τ = P
• And the lag constancy argument applies

Conditional Expectation Helper Lemmas

These lemmas support the L¹ Cesàro convergence framework.

theorem Exchangeability.DeFinetti.ViaKoopman.integrable_mul_of_ae_bdd_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsFiniteMeasure μ] {Z Y : Ω[α] → ℝ} (hZ : Measurable Z) (hZ_bd : ∃ (C : ℝ), ∀ᵐ (ω : Ω[α]) ∂μ, |Z ω| ≤ C) (hY : MeasureTheory.Integrable Y μ) : MeasureTheory.Integrable (Z * Y) μ

If Z is a.e.-bounded and measurable and Y is integrable, then Z*Y is integrable (finite measure suffices).

theorem Exchangeability.DeFinetti.ViaKoopman.condExp_mul_pullout {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] {Z Y : Ω[α] → ℝ} (hZ_meas : Measurable Z) (hZ_bd : ∃ (C : ℝ), ∀ᵐ (ω : Ω[α]) ∂μ, |Z ω| ≤ C) (hY : MeasureTheory.Integrable Y μ) : μ[Z * Y | shiftInvariantSigma] =ᵐ[μ] Z * μ[Y | shiftInvariantSigma]

Pull-out property: if Z is measurable w.r.t. the conditioning σ-algebra and a.e.-bounded, then CE[Z·Y | mSI] = Z·CE[Y | mSI] a.e. This is the standard "taking out what is known".