English
Under appropriate normed conditions, the distance between Birkhoff averages is bounded by the average of pointwise orbit distances: dist(birkhoffAverage 𝕜 f g n x, birkhoffAverage 𝕜 f g n y) ≤ (∑_{k=0}^{n-1} dist(g(f^[k] x), g(f^[k] y)))/n.
Русский
При подходящих условиях нормы расстояние между средними Биркхоффа ограничено средним значением попарных расстояний на орбитах: dist(birkhoffAverage ...) ≤ (∑ dist(...))/n.
LaTeX
$$$\\operatorname{dist}(\\mathrm{birkhoffAverage} 𝕜 f g n x, \\mathrm{birkhoffAverage} 𝕜 f g n y) \\le \\frac{\\sum_{k=0}^{n-1} \\operatorname{dist}(g(f^{[k]}x), g(f^{[k]}y))}{n}$$$
Lean4
theorem dist_birkhoffAverage_birkhoffAverage_le (f : α → α) (g : α → E) (n : ℕ) (x y : α) :
dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) ≤
(∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
(dist_birkhoffAverage_birkhoffAverage _ _ _ _ _ _).trans_le <| by gcongr; apply dist_birkhoffSum_birkhoffSum_le
