tendsto_translation_number₀' — Mathlib

English

For each f, Tendsto (f^(n+1) 0)/(n+1) to τ f as n → ∞.

Русский

Для каждого f Tendsto (f^(n+1) 0)/(n+1) к τ f при n → ∞.

LaTeX

$$$ \forall f \in CircleDeg1Lift, \ Tendsto (n \mapsto (f^(n+1)) 0 / (n+1))_{atTop} (\mathcal{N}(τ f)). $$$

Lean4

theorem tendsto_translation_number₀' :
    Tendsto (fun n : ℕ => (f ^ (n + 1) : CircleDeg1Lift) 0 / ((n : ℝ) + 1)) atTop (𝓝 <| τ f) :=
  by
  refine
    tendsto_iff_dist_tendsto_zero.2 <|
      squeeze_zero (fun _ => dist_nonneg) (fun n => ?_)
        ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_atTop_nat 1))
  dsimp
  have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
  rw [Real.dist_eq, div_sub' (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this, Nat.cast_add_one,
    div_le_div_iff_of_pos_right this, ← Nat.cast_add_one]
  apply dist_pow_map_zero_mul_translationNumber_le

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