dist_birkhoffAverage_apply_birkhoffAverage

English

The distance between the n-th Birkhoff averages after applying f to x and x itself is equal to the distance between g(f^[n] x) and g(x), divided by n: dist(birkhoffAverage 𝕜 f g n (f x), birkhoffAverage 𝕜 f g n x) = dist(g(f^[n] x), g x)/n.

Русский

Расстояние между n-ой средней Биркхоффа после применения f к x и самого x равно расстоянию между g(f^[n] x) и g(x), делённому на n.

LaTeX

$$$\\operatorname{dist}(\\mathrm{birkhoffAverage} 𝕜 f g n (f x), \\mathrm{birkhoffAverage} 𝕜 f g n x) = \\dfrac{\\operatorname{dist}(g(f^{[n]}x), g(x))}{n}$$$

Lean4

theorem dist_birkhoffAverage_apply_birkhoffAverage (f : α → α) (g : α → E) (n : ℕ) (x : α) :
    dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / n := by
  simp [dist_birkhoffAverage_birkhoffAverage, dist_birkhoffSum_apply_birkhoffSum]

Похожие утверждения