Shift-invariant σ-algebra and conditional expectation #
This file establishes the fundamental connection between:
- The fixed-point subspace of the Koopman operator
- The L² space with respect to the shift-invariant σ-algebra
- The conditional expectation onto the shift-invariant σ-algebra
The core definitions (shiftInvariantSigma, isShiftInvariant, tailSigma) and
the construction of shift-invariant representatives (gRep, mkShiftInvariantRep)
are in separate modules:
ShiftInvariantSigma.lean: Core σ-algebra definitionsShiftInvariantRepresentatives.lean: Limsup construction for representatives
Main definitions #
fixedSubspace: The subspace of L² functions fixed by the Koopman operator.metProjectionShift: Orthogonal projection onto the fixed-point subspace.condexpL2: Conditional expectation on L² with respect to the shift-invariant σ-algebra.
Main results #
fixedSpace_eq_invMeasurable: Functions fixed by Koopman are exactly those measurable with respect to the shift-invariant σ-algebra.proj_eq_condexp: The orthogonal projection onto the fixed-point subspace equals the conditional expectation onto the shift-invariant σ-algebra.
References #
- Olav Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Springer, Chapter 1 (pages 26-27). The shift-invariant σ-algebra is denoted 𝓘_ξ in Kallenberg.
- FMP 10.4: Invariant sets and functions (Chapter 10, pages 180-181). Key results used in the first proof.
FMP 10.4: Invariant Sets and Functions #
For a measure-preserving transformation T on (S, 𝒮, μ):
Definitions:
- A set I ∈ 𝒮 is invariant if I = T⁻¹I
- A set I is almost invariant if μ(I Δ T⁻¹I) = 0
- 𝓘 = invariant σ-field (invariant sets in 𝒮)
- 𝓘' = almost invariant σ-field (almost invariant sets in 𝒮^μ)
- A function f is invariant if f = f ∘ T
- A function f is almost invariant if f = f ∘ T a.s. μ
Lemma 1 (invariant sets and functions): A measurable function f: S → S' (Borel space) is invariant/almost invariant iff it is 𝓘-measurable/𝓘^μ-measurable, respectively.
Lemma 2 (almost invariance): For any distribution μ and μ-preserving transformation T, the invariant and almost invariant σ-fields satisfy: 𝓘' = 𝓘^μ (almost invariant = completion of invariant).
Lemma 3 (ergodicity): Let ξ be a random element in S with distribution μ, and T a μ-preserving map on S. Then ξ is T-ergodic iff the sequence (T^n ξ) is θ-ergodic, in which case even η = (f ∘ T^n ξ) is θ-ergodic for every measurable f: S → S'.
Functions that are AEStronglyMeasurable with respect to the invariant σ-algebra are
almost everywhere fixed by the shift.
If an Lp function is measurable with respect to the invariant σ-algebra, the Koopman
operator fixes it.
A Koopman-fixed function is automatically measurable with respect to the invariant σ-algebra.
Starting from the a.e. identity f ∘ shift = f, the previous lemma replaces a
representative of f by an actual shift-invariant function, and the resulting
measurability is transported back to f.
The Mean Ergodic Theorem and conditional expectation #
This section establishes the key connection between:
- The Koopman operator
U : L²(μ) → L²(μ)given by(Uf)(ω) = f(shift ω) - The fixed-point subspace
{f : Uf = f}(shift-invariant functions) - The conditional expectation
E[·|ℐ]onto the shift-invariant σ-algebra
Main theorem (proj_eq_condexp): The orthogonal projection onto the fixed-point
subspace equals the conditional expectation onto the shift-invariant σ-algebra.
Mathematical background:
- The Mean Ergodic Theorem states that Cesàro averages
n⁻¹ ∑ᵢ₌₀ⁿ⁻¹ Uⁱfconverge in L² to the orthogonal projection onto the fixed-point subspace - Conditional expectation
E[f|ℐ]is also characterized as an orthogonal projection (onto functions measurable w.r.t. ℐ) - Both projections are idempotent and symmetric, with the same range
- By uniqueness of orthogonal projections (
orthogonalProjections_same_range_eq), they must be equal
Application to de Finetti: This identification allows us to use ergodic theory (Koopman operator, Mean Ergodic Theorem) to prove facts about conditional expectations, which are central to the probabilistic formulation of de Finetti's theorem.
The fixed-point subspace of the Koopman operator.
This is the closed subspace of L²(μ) consisting of equivalence classes of functions f such that f ∘ shift = f almost everywhere.
In the ergodic approach to de Finetti, this is the target space of the limiting projection from the Mean Ergodic Theorem.
Equations
Instances For
Functions in the fixed-point subspace are exactly those that are a.e. invariant under shift.
The orthogonal projection onto the fixed-point subspace exists (as a closed subspace).
Orthogonal projection onto the fixed-point subspace (MET projection).
This is the orthogonal projection P : L²(μ) → fixedSubspace arising from the
Mean Ergodic Theorem (MET). It is defined as the composition of:
- Orthogonal projection onto the fixed-point subspace (as an abstract subspace)
- The subtype inclusion back into L²(μ)
Properties (established in subsequent lemmas):
metProjectionShift_idem: Idempotent (P² = P)metProjectionShift_isSymmetric: Symmetric/self-adjointmetProjectionShift_range: Range equals the fixed-point subspacemetProjectionShift_tendsto: Limit of Cesàro averages (Mean Ergodic Theorem)
Key theorem: proj_eq_condexp shows this projection equals conditional expectation
onto the shift-invariant σ-algebra.
Defined as an alias for metProjection shift, the generic projection for any
measure-preserving transformation.
Equations
Instances For
The range of metProjectionShift equals the fixed subspace.
metProjectionShift fixes elements of the fixed subspace.
Conditional expectation on L² with respect to the shift-invariant σ-algebra.
This is the orthogonal projection onto the subspace of shift-invariant L² functions,
implemented using mathlib's condExpL2.
Equations
Instances For
lpMeas functions are exactly the Koopman-fixed functions.
The conditional expectation equals the orthogonal projection onto the fixed-point subspace.
This fundamental connection links:
- Probability theory: conditional expectation with respect to shift-invariant σ-algebra
- Functional analysis: orthogonal projection in Hilbert space
- Ergodic theory: fixed-point subspace of the Koopman operator