dist_birkhoffSum_apply_birkhoffSum

English

For all f: α→α, g: α→E, n ∈ ℕ and x ∈ α, the distance between the n-th Birkhoff sums at f x and at x equals the distance between the one-step difference g(f^[n] x) and g x: dist(birkhoffSum f g n (f x), birkhoffSum f g n x) = dist(g (f^[n] x), g x).

Русский

Для любых f: α→α, g: α→E, n ∈ ℕ и x ∈ α расстояние между n-й суммой Биркхоффа в f x и в x равно расстоянию между g(f^[n] x) и g(x).

LaTeX

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

Lean4

theorem dist_birkhoffSum_apply_birkhoffSum (f : α → α) (g : α → E) (n : ℕ) (x : α) :
    dist (birkhoffSum f g n (f x)) (birkhoffSum f g n x) = dist (g (f^[n] x)) (g x) := by
  simp only [dist_eq_norm, birkhoffSum_apply_sub_birkhoffSum]

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