tendsto_pow_atTop_nhds_zero_iff — Mathlib

English

For r ∈ NNReal, Tendsto (n ↦ r^n) atTop (𝓝 0) iff r < 1.

Русский

Для r ∈ NNReal верно: Tendsto (n^n) → 0 тогда и только тогда, когда r < 1.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{NNReal}, \\\\ operatorname{Tendsto}(n \\\\mapsto r^n) \\\\ atTop \\\\ (\\\\mathcal{N} 0) \\\\Leftrightarrow \\\\ r < 1.$$$

Lean4

@[simp]
protected theorem tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 :=
  by
  refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩
  lift r to NNReal
  · refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))
    exact eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩
  rw [← coe_zero] at h
  norm_cast at h ⊢
  exact NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h

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