English
In a normed setting, the distance between the n-th Birkhoff averages of g at x and y satisfies dist(birkhoffAverage 𝕜 f g n x, birkhoffAverage 𝕜 f g n y) = dist(birkhoffSum f g n x, birkhoffSum f g n y)/n.
Русский
В нормированном пространстве расстояние между n-й средней Биркхоффа по x и y равняется расстоянию между n-й суммой Биркхоффа по x и y делённому на n.
LaTeX
$$$\\mathrm{dist}(\\mathrm{birkhoffAverage}(f,g,n,x),\\mathrm{birkhoffAverage}(f,g,n,y))=\\dfrac{\\mathrm{dist}(\\mathrm{birkhoffSum}(f,g,n,x),\\mathrm{birkhoffSum}(f,g,n,y))}{n}$$$
Lean4
theorem dist_birkhoffAverage_birkhoffAverage (f : α → α) (g : α → E) (n : ℕ) (x y : α) :
dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) =
dist (birkhoffSum f g n x) (birkhoffSum f g n y) / n :=
by simp [birkhoffAverage, dist_smul₀, div_eq_inv_mul]
