English
For f : ℕ → ENNReal and r ∈ ENNReal, HasSum f r holds if and only if the sequence of partial sums tends to r: HasSum f r ↔ Tendsto (n ↦ ∑ i ∈ [0,n), f(i)) atTop (nhds r).
Русский
Для f : ℕ → ENNReal и r ∈ ENNReal условие HasSum f r эквивалентно тому, что частичные суммы сходятся к r: HasSum f r ⇔ Tendsto (n ↦ ∑_{i< n} f(i)) atTop (nhds r).
LaTeX
$$$\mathrm{HasSum}\, f\, r \;\;\Longleftrightarrow\;\; \mathrm{Tendsto}\,(\lambda n. \sum_{i=0}^{n-1} f(i))\;\mathrm{atTop}\; (\mathcal{N} r)$$$
Lean4
theorem hasSum_iff_tendsto_nat {f : ℕ → ℝ≥0∞} (r : ℝ≥0∞) :
HasSum f r ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r) :=
by
refine ⟨HasSum.tendsto_sum_nat, fun h => ?_⟩
rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]
· exact ENNReal.summable.hasSum
· exact fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset_range.2 hst)
