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 โˆˆ 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 โˆˆ 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 โˆˆ Finset.range N, f^[n] x

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