translationNumber_eq_of_tendsto₀

English

If the sequence n ↦ f^[n] 0 / n converges to a real τ' as n → ∞, then τ f = τ'.

Русский

Если последовательность n ↦ f^[n] 0 / n сходится к τ' при n → ∞, то τ(f) = τ'.

LaTeX

$$$ \forall f \in CircleDeg1Lift, \forall τ' \in \mathbb{R}, \operatorname{Tendsto} (n \mapsto f^[n] 0 / n)_{atTop} (\mathcal{N}(τ')) \Rightarrow τ(f) = τ'. $$$

Lean4

theorem translationNumber_eq_of_tendsto₀ {τ' : ℝ} (h : Tendsto (fun n : ℕ => f^[n] 0 / n) atTop (𝓝 τ')) : τ f = τ' :=
  f.translationNumber_eq_of_tendsto_aux <| by
    simpa [Function.comp_def, transnumAuxSeq_def, coe_pow] using
      h.comp (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two)

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