Theorems · Theorem · dynamical systems

Function.IsFixedPt.tendsto_birkhoffAverage

∀ {α : Type u_1} {E : Type u_2} (R : Type u_3) [inst : DivisionSemiring R] [CharZero R] [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : Module R E] {f : α → α} {x : α},
  Function.IsFixedPt f x →
    ∀ (g : α → E), Filter.Tendsto (fun x_1 => birkhoffAverage R f g x_1 x) Filter.atTop (nhds (g x))

The Birkhoff averages of a function g over the orbit of a fixed point x of f tend to g x as N → ∞. In fact, they are equal to g x for all N ≠ 0, see Function.IsFixedPt.birkhoffAverage_eq. TODO: add a version for a periodic orbit.

Defined in

Mathlib.Dynamics.BirkhoffSum.NormedSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionSemiringCharZeroAddCommMonoidTopologicalSpaceModule