translationNumber_eq_of_dist_bounded

English

If for all n the orbit distance dist((f^n)0, (g^n)0) is bounded by some C, then τ f = τ g.

Русский

Если расстояние между орбитами f^n(0) и g^n(0) ограничено константой C, то τ f = τ g.

LaTeX

$$$ \forall f,g \in CircleDeg1Lift, \forall C \in \mathbb{R}, \left( \forall n \in \mathbb{N}, \operatorname{dist}((f^n)0, (g^n)0) \le C \right) \Rightarrow τ(f) = τ(g). $$$

Lean4

theorem translationNumber_eq_of_dist_bounded {f g : CircleDeg1Lift} (C : ℝ)
    (H : ∀ n : ℕ, dist ((f ^ n) 0) ((g ^ n) 0) ≤ C) : τ f = τ g :=
  Eq.symm <|
    g.translationNumber_eq_of_tendsto_aux <| f.tendsto_translationNumber_of_dist_bounded_aux (fun n ↦ (g ^ n) 0) C H

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