Theorems · Theorem · dynamical systems

ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (f : E →L[𝕜] E),
  ‖f‖ ≤ 1 →
    ∀ (x : E),
      Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) id x_1 x) Filter.atTop
        (nhds ↑(((↑f).eqLocus ↑1).orthogonalProjectionOnto 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`.

Defined in

Mathlib.Analysis.InnerProductSpace.MeanErgodic

Cited by

0 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace