Theorems · Theorem · sequences and series

tendsto_sum_nat_add

∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  (f : ℕ → G), Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

For f : ℕ → G, the sum ∑' k, f (k + i) tends to zero. This does not require a summability assumption on f, as otherwise all such sums are zero.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.NatInt

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupTopologicalSpaceIsTopologicalAddGroupT2Space