English
For a map f: α → α, a function g: α → M into a module, and n ∈ ℕ, the Birkhoff average is defined as the normalized sum: birkhoffAverage_R f g n x = (n)^{-1} · birkhoffSum f g n x, i.e., the average of g along the first n iterates of x under f.
Русский
Для отображения f: α → α и функции g: α → M, тесно связанного с модулем, среднее Биркхоффа за n шагов равно нормированному сумме: усреднение по первым n терминам вдоль орбиты x под действием f.
LaTeX
$$$\mathrm{birkhoffAverage}(R,f,g,n,x) = n^{-1} \cdot \mathrm{birkhoffSum}(f,g,n,x).$$$
Lean4
/-- The average value of `g` on the first `n` points of the orbit of `x` under `f`,
i.e. the Birkhoff sum `∑ k ∈ Finset.range n, g (f^[k] x)` divided by `n`.
This average appears in many ergodic theorems
which say that `(birkhoffAverage R f g · x)`
converges to the "space average" `⨍ x, g x ∂μ` as `n → ∞`.
We use an auxiliary `[DivisionSemiring R]` to define division by `n`.
However, the definition does not depend on the choice of `R`,
see `birkhoffAverage_congr_ring`. -/
def birkhoffAverage (f : α → α) (g : α → M) (n : ℕ) (x : α) : M :=
(n : R)⁻¹ • birkhoffSum f g n x
