Koopman Operator and Mean Ergodic Theorem

This file contains the core results connecting the Koopman operator to conditional expectation:

• condexpL2_fixes_fixedSubspace - CE fixes the fixed subspace
• birkhoffAverage_tendsto_condexp - Birkhoff averages converge to CE in L²
• condexpL2_koopman_comm - CE commutes with Koopman operator

These results are fundamental for the de Finetti proof via ergodic theory.

theorem Exchangeability.DeFinetti.ViaKoopman.condexpL2_fixes_fixedSubspace {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) {g : ↥(MeasureTheory.Lp ℝ 2 μ)} (hg : g ∈ fixedSubspace hσ) : condexpL2 g = g

Conditional expectation onto shift-invariant σ-algebra fixes elements of fixedSubspace.

This is the tower property of conditional expectation: E[f|σ] = f when f is σ-measurable.

theorem Exchangeability.DeFinetti.ViaKoopman.birkhoffAverage_tendsto_condexp {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (f : ↥(MeasureTheory.Lp ℝ 2 μ)) : Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ (⇑(Ergodic.koopman PathSpace.shift hσ)) (fun (f : ↥(MeasureTheory.Lp ℝ 2 μ)) => f) n f) Filter.atTop (nhds (condexpL2 f))

Main theorem: Birkhoff averages converge in L² to conditional expectation.

This combines:

1. The Mean Ergodic Theorem (MET) giving convergence to orthogonal projection
2. The identification proj = condexp via range_condexp_eq_fixedSubspace

Part B (Shift Equivariance): Conditional expectation commutes with Koopman operator

The conditional expectation onto the shift-invariant σ-algebra commutes with composition by shift. This is the key fact for showing CE[f(ω₀)·g(ωₖ) | 𝓘] is constant in k.

Proof Strategy: Both condexpL2 and koopman shift are continuous linear operators, with condexpL2 being the orthogonal projection onto fixedSubspace hσ. For any f ∈ Lp, we show P(Uf) = Pf where P = condexpL2 and U = koopman shift:

1. Decompose f = Pf + (f - Pf) with Pf ∈ S and (f - Pf) ⊥ S where S = fixedSubspace
2. U(Pf) = Pf since Pf ∈ fixedSubspace (definition of fixed subspace)
3. U(f - Pf) ⊥ S since U is an isometry preserving orthogonality
4. Therefore P(Uf) = P(Pf) = Pf since projection onto invariant subspace commutes.

theorem Exchangeability.DeFinetti.ViaKoopman.condexpL2_koopman_comm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (f : ↥(MeasureTheory.Lp ℝ 2 μ)) : condexpL2 ((Ergodic.koopman PathSpace.shift hσ) f) = condexpL2 f

Part B (Shift Equivariance): Conditional expectation commutes with Koopman operator.

theorem Exchangeability.DeFinetti.ViaKoopman.birkhoffCylinder_tendsto_condexp {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) {m : ℕ} (fs : Fin m → α → ℝ) (hmeas : ∀ (k : Fin m), Measurable (fs k)) (hbd : ∀ (k : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs k x| ≤ C) : have F := productCylinder fs; ∃ (fL2 : ↥(MeasureTheory.Lp ℝ 2 μ)), (∀ᵐ (ω : Ω[α]) ∂μ, ↑↑fL2 ω = F ω) ∧ Filter.Tendsto (fun (n : ℕ) => birkhoffAverage ℝ (⇑(Ergodic.koopman PathSpace.shift hσ)) (fun (f : ↥(MeasureTheory.Lp ℝ 2 μ)) => f) n fL2) Filter.atTop (nhds (condexpL2 fL2))

Specialization to cylinder functions: the core case for de Finetti.