Theorems · Theorem · measure theory

NNReal.hasSum_iff_tendsto_nat

∀ {f : ℕ → NNReal} {r : NNReal}, HasSum f r ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds r)

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.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Cited by

2 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound