The mean ergodic projection is conditional expectation given the invariants

Mathlib's von Neumann mean ergodic theorem gives convergence to an orthogonal projection, and the probabilistic form of the theorem still needs that projection identified with a conditional expectation. This file carries out the identification for the L² composition (Koopman) operator of a measure-preserving map T: the mean ergodic projection metProjection T hT of TauCeti.Probability.Ergodic.MeanErgodic is Mathlib's condExpL2 for the invariant σ-algebra MeasurableSpace.invariants T. Passing from condExpL2 to the conditional expectation μ[· | MeasurableSpace.invariants T] of representatives costs exactly what Mathlib's MemLp.condExpL2_ae_eq_condExp' costs — σ-finiteness of the trimmed measure μ.trim (MeasurableSpace.invariants_le T) and integrability of the observable — so the pointwise statements below assume those while the condExpL2 ones do not. Both hold automatically on a finite measure space.

The identification is not a simp step: it rests on fixedSpace_eq_lpMeas_invariants, which replaces an almost invariant observable by an invariantly measurable representative, together with the fact that both operators are orthogonal projections onto the resulting common subspace of L².

Feeding the identification into birkhoffAverage_tendsto_metProjection turns the Hilbert-space statement into the probabilists' mean ergodic theorem: the time averages birkhoffAverage ℝ T f n of an integrable square-integrable observable converge in L² to μ[f | MeasurableSpace.invariants T]. The translation between the operator Birkhoff averages of the composition operator and the pointwise Birkhoff averages of a representative is coeFn_birkhoffAverage_compMeasurePreserving of TauCeti.Probability.Ergodic.BirkhoffLp.

Main results

• metProjection_eq_condExpL2 — the mean ergodic projection is condExpL2 for the invariant σ-algebra, for an arbitrary measure;
• metProjection_ae_eq_condExp — its representatives are the conditional expectation given the invariant σ-algebra;
• condExpL2_invariants_eq_self_iff — condExpL2 for the invariant σ-algebra fixes exactly the almost everywhere invariant observables, again for an arbitrary measure;
• birkhoffAverage_tendsto_condExpL2 — the Birkhoff averages of the composition operator converge to condExpL2, and tendsto_eLpNorm_birkhoffAverage_sub_condExp — the pointwise Birkhoff averages converge in L² to the conditional expectation;
• tendsto_integral_abs_birkhoffAverage_sub_condExp — the L¹ form of the previous item, on a finite measure: the mean absolute deviation of the Birkhoff averages from the conditional expectation tends to 0. This is the shape a consumer integrating against a bounded weight wants, and it needs no integrability hypothesis of its own.

The Exchangeability roadmap records this identification as the Layer 5 milestone proj_eq_condexp, whose migration source is the Ergodic subtree of cameronfreer/exchangeability. Nothing here is a port: the statements are for an arbitrary measure-preserving map rather than the path-space shift, and the proofs consume Mathlib's condExpL2 and von Neumann mean ergodic theorem.

The projection as a conditional expectation

theorem TauCeti.Probability.metProjection_eq_condExpL2 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp ℝ 2 μ)) : (metProjection T hT) g = ↑((MeasureTheory.condExpL2 ℝ ℝ ⋯) g)

The mean ergodic projection on real L² is Mathlib's L² conditional expectation for the invariant σ-algebra of the transformation.

Both sides are the orthogonal projection onto the same closed subspace of L²: the observables fixed by composition with T are exactly those almost everywhere strongly measurable for MeasurableSpace.invariants T, by fixedSpace_eq_lpMeas_invariants.

theorem TauCeti.Probability.metProjection_ae_eq_condExp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.SigmaFinite (μ.trim ⋯)] (g : ↥(MeasureTheory.Lp ℝ 2 μ)) (hg : MeasureTheory.Integrable (↑↑g) μ) : ↑↑((metProjection T hT) g) =ᵐ[μ] μ[↑↑g | MeasurableSpace.invariants T]

The mean ergodic projection of an integrable square-integrable observable is almost everywhere its conditional expectation given the invariant σ-algebra.

@[simp]

theorem TauCeti.Probability.condExpL2_invariants_eq_self_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp ℝ 2 μ)) : ↑((MeasureTheory.condExpL2 ℝ ℝ ⋯) g) = g ↔ ↑↑g ∘ T =ᵐ[μ] ↑↑g

Conditional expectation for the invariant σ-algebra fixes exactly the almost everywhere invariant L² observables.

The mean ergodic theorem for conditional expectations

theorem TauCeti.Probability.birkhoffAverage_tendsto_condExpL2 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp ℝ 2 μ)) : Filter.Tendsto (fun (x : ℕ) => birkhoffAverage ℝ (⇑(MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ T hT).toContinuousLinearMap) id x g) Filter.atTop (nhds ↑((MeasureTheory.condExpL2 ℝ ℝ ⋯) g))

The Birkhoff averages of the L² composition operator converge to the L² conditional expectation for the invariant σ-algebra.

theorem TauCeti.Probability.tendsto_eLpNorm_birkhoffAverage_sub_condExp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.SigmaFinite (μ.trim ⋯)] {f : Ω → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hf_int : MeasureTheory.Integrable f μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (birkhoffAverage ℝ T f n - μ[f | MeasurableSpace.invariants T]) 2 μ) Filter.atTop (nhds 0)

The mean ergodic theorem for conditional expectations. The Birkhoff time averages of an integrable square-integrable observable converge in L² to its conditional expectation given the invariant σ-algebra of the transformation.

theorem TauCeti.Probability.tendsto_integral_abs_birkhoffAverage_sub_condExp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} (hf : MeasureTheory.MemLp f 2 μ) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |birkhoffAverage ℝ T f n ω - μ[f | MeasurableSpace.invariants T] ω| ∂μ) Filter.atTop (nhds 0)

The L¹ form. On a finite measure the L² convergence above upgrades to convergence of the mean absolute deviation, which is the shape a consumer integrating against a bounded weight wants:

∫ ω, |birkhoffAverage ℝ T f n ω - μ[f | invariants T] ω| ∂μ → 0.

Integrability is not a separate hypothesis: on a finite measure it follows from MemLp f 2.