English
Equality Tendsto (r^n) atTop (nhds 0) is equivalent to |r|<1.
Русский
Сходимость r^n к 0 равносильна |r|<1.
LaTeX
$$$$\\operatorname{Tendsto}(r^n)\\text{ atTop} (\\nhds 0) \\iff |r| < 1.$$$$
Lean4
@[simp]
theorem tendsto_pow_atTop_nhds_zero_iff {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜]
[TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1 :=
by
rw [tendsto_zero_iff_abs_tendsto_zero]
refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩
· by_cases hr : 1 = |r|
· replace h : Tendsto (fun n : ℕ ↦ |r| ^ n) atTop (𝓝 0) := by simpa only [← abs_pow, h]
simp only [hr.symm, one_pow] at h
exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds
· apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
· refine
(pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le) hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))
exact ⟨n, le_of_lt hn⟩
· simpa only [← abs_pow]
· simpa only [← abs_pow] using (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h
