# Documentation

Mathlib.Analysis.InnerProductSpace.MeanErgodic

# Von Neumann Mean Ergodic Theorem in a Hilbert Space #

In this file we prove the von Neumann Mean Ergodic Theorem for an operator in a Hilbert space. It says that for a contracting linear self-map f : E →ₗ[𝕜] E of a Hilbert space, the Birkhoff averages

birkhoffAverage 𝕜 f id N x = (N : 𝕜)⁻¹ • ∑ n in Finset.range N, f^[n] x


converge to the orthogonal projection of x to the subspace of fixed points of f, see ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection.

theorem LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure {𝕜 : Type u_2} {E : Type u_1} [] [] (f : E →ₗ[𝕜] E) (hf : ) (g : E →L[𝕜] { x // x }) (hg_proj : ∀ (x : { x // x }), g x = x) (hg_ker : ↑() closure ↑(LinearMap.range (f - 1))) (x : E) :
Filter.Tendsto (fun x => birkhoffAverage 𝕜 (f) id x x) Filter.atTop (nhds ↑(g x))

Von Neumann Mean Ergodic Theorem, a version for a normed space.

Let f : E → E be a contracting linear self-map of a normed space. Let S be the subspace of fixed points of f. Let g : E → S be a continuous linear projection, g|_S=id. If the range of f - id is dense in the kernel of g, then for each x, the Birkhoff averages

birkhoffAverage 𝕜 f id N x = (N : 𝕜)⁻¹ • ∑ n in Finset.range N, f^[n] x


converge to g x as N → ∞.

Usually, this fact is not formulated as a separate lemma. I chose to do it in order to isolate parts of the proof that do not rely on the inner product space structure.

theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection {𝕜 : Type u_2} {E : Type u_1} [] [] [] (f : E →L[𝕜] E) (hf : f 1) (x : E) :
Filter.Tendsto (fun x => birkhoffAverage 𝕜 (f) id x x) Filter.atTop (nhds ↑(↑() x))

Von Neumann Mean Ergodic Theorem for an operator in a Hilbert space. For a contracting continuous linear self-map f : E →L[𝕜] E of a Hilbert space, ‖f‖ ≤ 1, the Birkhoff averages

birkhoffAverage 𝕜 f id N x = (N : 𝕜)⁻¹ • ∑ n in Finset.range N, f^[n] x


converge to the orthogonal projection of x to the subspace of fixed points of f.