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} [IsROrC ๐] [NormedSpace ๐ E] (f : E โโ[๐] E) (hf : LipschitzWith 1 โf) (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} [IsROrC ๐] [InnerProductSpace ๐ E] [] (f : E โL[๐] E) (hf : ) (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.