tendsto_nat_tsum — Mathlib

English

For any f : ℕ → ENNReal, the sequence of partial sums tends to the total sum: Tendsto (n ↦ ∑ i ∈ [0,n), f i) atTop (nhds (∑' n, f n)).

Русский

Для любой функции f : ℕ → ENNReal частичные суммы сходятся к полной сумме:

LaTeX

$$$\text{Tendsto}\,(\lambda n. \sum_{i< n} f(i))\;\mathrm{atTop}\; (\mathcal{N} (\sum' n, f n))$$$

Lean4

theorem tendsto_nat_tsum (f : ℕ → ℝ≥0∞) : Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' n, f n)) :=
  by
  rw [← hasSum_iff_tendsto_nat]
  exact ENNReal.summable.hasSum

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