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_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : E →ₗ[𝕜] E) (hf : LipschitzWith 1 ⇑f) (g : E →L[𝕜] ↥(LinearMap.eqLocus f 1)) (hg_proj : ∀ (x : ↥(LinearMap.eqLocus f 1)), g ↑x = x) (hg_ker : ↑(LinearMap.ker g) ⊆ closure ↑(LinearMap.range (f - 1))) (x : E) : Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage 𝕜 (⇑f) id x_1 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_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (f : E →L[𝕜] E) (hf : ‖f‖ ≤ 1) (x : E) : Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage 𝕜 (⇑f) id x_1 x) Filter.atTop (nhds ↑((orthogonalProjection (LinearMap.eqLocus f 1)) 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.