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 shiftscondexp_lag_constant_product- Generalized lag constancy for productscondexp_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)
The comap of shiftInvariantSigma along restrictNonneg is contained in shiftInvariantSigmaℤ.
This follows from the fact that preimages of shift-invariant sets are shiftℤ-invariant,
using restrictNonneg_shiftℤ : restrictNonneg (shiftℤ ω) = shift (restrictNonneg ω).
Pulling an almost-everywhere equality back along the natural extension.
Proof: Uses ae_map_iff from mathlib: since μ = map restrictNonneg ext.μhat,
we have (∀ᵐ ω ∂μ, F ω = G ω) ↔ (∀ᵐ ωhat ∂ext.μhat, F (restrictNonneg ωhat) = G (restrictNonneg ωhat)).
The hypothesis h gives the RHS, so we conclude the LHS.
Two-sided version of condexp_precomp_iterate_eq.
Proof strategy: For any k iterations of shiftℤ, the conditional expectation is unchanged because:
- shiftℤ^[k] is measure-preserving (composition of measure-preserving maps)
- shiftℤ^[k] leaves shiftInvariantSigmaℤ-measurable sets invariant
- Set-integrals over invariant sets are preserved by measure-preserving maps
Invariance of conditional expectation under the inverse shift.
Proof strategy: Similar to condexp_precomp_iterate_eq_twosided, but using
that shiftℤInv also preserves the measure and leaves the invariant σ-algebra fixed.
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.
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.
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.
If Z is a.e.-bounded and measurable and Y is integrable,
then Z*Y is integrable (finite measure suffices).
Conditional expectation is L¹-Lipschitz: moving the integrand changes the CE by at most the L¹ distance. This is a standard property following from Jensen's inequality.
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".