English
Let x be a fixed point of f. Then the Birkhoff averages along the orbit of x converge to g(x); in fact, bAvg_n(x) = g(x) for all n, hence Tendsto birkhoffAverage to g(x).
Русский
Пусть x — фиксированная точка f. Тогда усреднения Биркхоффа по орбите x сходятся к g(x); фактически для всех n имеем bAvg_n(x) = g(x), следовательно, предел равен g(x).
LaTeX
$$$\\mathrm{Tendsto}(\\mathrm{birkhoffAverage} \\, 𝕜 \\, f \\, g \\, \\cdot \\, x) \\ a tTop \\ (\\mathcal{N}(g(x)))$$$
Lean4
/-- 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. -/
theorem tendsto_birkhoffAverage (R : Type*) [DivisionSemiring R] [CharZero R] [AddCommMonoid E] [TopologicalSpace E]
[Module R E] {f : α → α} {x : α} (h : f.IsFixedPt x) (g : α → E) :
Tendsto (birkhoffAverage R f g · x) atTop (𝓝 (g x)) :=
tendsto_const_nhds.congr' <| (eventually_ne_atTop 0).mono fun _n hn ↦ (h.birkhoffAverage_eq R g hn).symm
