English
For f: ℕ → ℝ with f(n) ≥ 0, HasSum f r is equivalent to the partial sums ∑_{i< n} f(i) tending to r.
Русский
Для последовательности неотрицательных членов f(n) имеет место эквивалентность: HasSum f r ⇔ частичные суммы сходятся к r.
LaTeX
$$$\forall f:\mathbb{N}\to\mathbb{R},\; (\forall n, f(n)\ge 0) \;\Rightarrow\; \text{HasSum}(f,r) \iff \text{Tendsto}\left(\sum_{i< n} f(i)\right)_{n\to\infty} = 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_of_nonneg {f : ℕ → ℝ} (hf : ∀ i, 0 ≤ f i) (r : ℝ) :
HasSum f r ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r) :=
by
lift f to ℕ → ℝ≥0 using hf
simp only [HasSum, ← NNReal.coe_sum, NNReal.tendsto_coe']
exact exists_congr fun hr => NNReal.hasSum_iff_tendsto_nat
