English
Let f be a function from an arbitrary index set to extended nonnegative reals. If the (extended) sum ∑' x f(x) is finite, then f tends to 0 along the cofinite filter (i.e., away from finitely many points).
Русский
Пусть f: A → ℝ≥0∞. Если сумма ∑' x f(x) конечна, то f(x) → 0 по фильтру cofinites (то есть при удалении конечного множества точек).
LaTeX
$$$\left(\sum\' x \ f(x) \neq \infty\right) \Rightarrow \mathrm{Tendsto}(f,\, \text{cofinite},\, \mathcal{N}(0)).$$$
Lean4
theorem tendsto_cofinite_zero_of_tsum_ne_top {α} {f : α → ℝ≥0∞} (hf : ∑' x, f x ≠ ∞) : Tendsto f cofinite (𝓝 0) :=
by
have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf
have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) := funext fun n => (coe_toNNReal (f_ne_top n)).symm
rw [h_f_coe, ← @coe_zero, tendsto_coe]
exact NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)
