English
A sequence of nonnegative terms has HasSum to r if and only if the sequence of its finite partial sums converges to r.
Русский
Посылка из неотрицательных значений f имеет HasSum к r тогда и только тогда, когда частичные суммы сходятся к r.
LaTeX
$$$\\\\mathrm{HasSum}(f,r) \\\\iff \\\\mathrm{Tendsto}\\left(n \\mapsto \\sum_{i=0}^{n-1} f(i)\\right)_{atTop} (\\\\mathcal{N}(r))$$$
Lean4
/-- A series of non-negative real numbers converges to `r` in the sense of `HasSum` if and only if
the sequence of partial sum converges to `r`. -/
theorem hasSum_iff_tendsto_nat {f : ℕ → ℝ≥0} {r : ℝ≥0} :
HasSum f r ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r) :=
by
rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]
simp only [← ENNReal.coe_finset_sum]
exact ENNReal.tendsto_coe
