Theorems · Theorem · dynamical systems

LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (f : E →ₗ[𝕜] E),
  LipschitzWith 1 ⇑f →
    ∀ (g : E →L[𝕜] ↥(f.eqLocus 1)),
      (∀ (x : ↥(f.eqLocus 1)), g ↑x = x) →
        ↑(↑g).ker ⊆ closure ↑(f - 1).range →
          ∀ (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.

Defined in

Mathlib.Analysis.InnerProductSpace.MeanErgodic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpace