Telescoping infinite sums

Stream: Is there code for X?

[Eric Wieser]

Do we have anything like the following?

theorem hasSum_telescope
    {R} [TopologicalSpace R] [AddCommGroup R] [TopologicalAddGroup R] (x : ℕ → R)
    (hx : Tendsto x atTop (𝓝 0)) :
    HasSum (fun i : ℕ => x i - x (i + 1)) (x 0) :=

[Sébastien Gouëzel]

It's not true: take x i = (-1)^i / i, it tends to zero but x i - x (i + 1) is not summable.

[Eric Wieser]

I guess wikipedia is just wrong then? Are there any reasonable extra conditions that make this salvageable?

[Damiano Testa]

I thought that alternating sign series did have this property.

In particular, @Sébastien Gouëzel, isn't the general term of your example approx $1/i^2$?

Of course, not all convergent-but-not-absolutely-convergent series have, though.

[Damiano Testa]

Oh, Eric is only asking for the sequence to converge to zero, not for the series to be summable (though not necessarily absolutely)!

Still, I am a little skeptical about Sébastien's example.

[Sébastien Gouëzel]

I put the sign (-1)^i to make sure that x i - x (i + 1) is of the order of magnitude of 1/i.

[Damiano Testa]

:man_facepalming: I was so sure that the sign had been extracted out of x, that I simply assumed that you were subtracting two numbers with the same sign!

Sébastien, I completely agree with you!

[Antoine Chambert-Loir]

Eric Wieser said:

I guess wikipedia is just wrong then? Are there any reasonable extra conditions that make this salvageable?

Wikipedia says it holds when $a_n$ tends to $0$, and the arguments there are correct, if summability is taken on the sense of series (partial sums converge), but as Sébastien's example shows, this is weaker than the definition of summability for families.