tendsto_translation_number' — Mathlib

English

For any x ∈ ℝ, Tendsto ( (f^(n+1) x - x)/(n+1) ) to τ f.

Русский

Для любого x ∈ ℝ предел (f^(n+1) x − x)/(n+1) равен τ f.

LaTeX

$$$ \forall x \in \mathbb{R}, \ Tendsto (n \mapsto ((f^{n+1}) x - x)/(n+1))_{atTop} (\mathcal{N}(τ f)). $$$

Lean4

theorem tendsto_translation_number' (x : ℝ) :
    Tendsto (fun n : ℕ => ((f ^ (n + 1) : CircleDeg1Lift) x - x) / (n + 1)) atTop (𝓝 <| τ f) :=
  mod_cast (tendsto_add_atTop_iff_nat 1).2 (f.tendsto_translationNumber x)

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