Theorems · Theorem · measure theory

NNReal.tendsto_sum_nat_add

∀ (f : ℕ → NNReal), Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

For f : ℕ → ℝ≥0, then ∑' k, f (k + i) tends to zero. This does not require a summability assumption on f, as otherwise all sums are zero.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Cited by

1 results in Mathlib

Foundations

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