English
For all f: α→α and g: α→E, the distance between birkhoffSum f g n x and birkhoffSum f g n y is bounded by the sum of pointwise distances along the orbits: dist(birkhoffSum f g n x, birkhoffSum f g n y) ≤ sum_{k=0}^{n-1} dist(g(f^[k] x), g(f^[k] y)).
Русский
Для любых f: α→α и g: α→E расстояние между birkhoffSum f g n x и birkhoffSum f g n y не превышает суммы попарных расстояний вдоль орбит: dist(…, …) ≤ ∑ dist(g(f^k x), g(f^k y)).
LaTeX
$$$\\operatorname{dist}(\\mathrm{birkhoffSum}(f,g,n,x), \\mathrm{birkhoffSum}(f,g,n,y)) \\le \\sum_{k=0}^{n-1} \\operatorname{dist}(g(f^{[k]}x), g(f^{[k]}y))$$$
Lean4
theorem dist_birkhoffSum_birkhoffSum_le (f : α → α) (g : α → E) (n : ℕ) (x y : α) :
dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y)) :=
dist_sum_sum_le _ _ _
