tendsto_pow_atTop_nhds_zero_iff_norm_lt_one

English

Same equivalence as above for real powers and norm.

Русский

Та же эквивалентность для нормированных степеней и нормы.

LaTeX

$$$\\\\forall x \\\\in R, (\\\\lim_{n\\\\to\\\\infty} x^n = 0) \\\\Leftrightarrow \\\\|x\\\\| < 1$$$

Lean4

theorem tendsto_pow_atTop_nhds_zero_iff_norm_lt_one {R : Type*} [SeminormedRing R] [NormMulClass R] {x : R} :
    Tendsto (fun n : ℕ ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1 := by
  -- this proof is slightly fiddly since `‖x ^ n‖ = ‖x‖ ^ n` might not hold for `n = 0`

  refine ⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩
  rw [← abs_of_nonneg (norm_nonneg _), ← tendsto_pow_atTop_nhds_zero_iff, tendsto_zero_iff_norm_tendsto_zero]
  apply Tendsto.congr'
  filter_upwards [eventually_ge_atTop 1] with n hn
  induction n, hn using Nat.le_induction with
  | base => simp
  | succ n hn IH => simp [pow_succ, IH]

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