tendsto_atTop_zero_of_tsum_ne_top

English

If the sum ∑' x f(x) is finite, then f(n) → 0 as n → ∞ (i.e., along the atTop filter on the natural numbers).

Русский

Если сумма ∑' n f(n) конечна, то f(n) → 0 при n → ∞ (по фильтру atTop).

LaTeX

$$$\left(\sum\' x \ f(x) \neq \infty\right) \Rightarrow \mathrm{Tendsto}(f,\, \mathrm{atTop},\, \mathcal{N}(0)).$$$

Lean4

theorem tendsto_atTop_zero_of_tsum_ne_top {f : ℕ → ℝ≥0∞} (hf : ∑' x, f x ≠ ∞) : Tendsto f atTop (𝓝 0) :=
  by
  rw [← Nat.cofinite_eq_atTop]
  exact tendsto_cofinite_zero_of_tsum_ne_top hf

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