A simple series lemma

Stream: new members

[Stepan Nesterov]

Does mathlib has the following statement: If \sum_{n=0}^{\infty} a_n converges, then so does \sum_{n=k}^{\infty} a_n?

[Yakov Pechersky]

docs#sum_add_tsum_nat_add

[Yakov Pechersky]

You're asking about has_sum, while that one is about summable

[Stepan Nesterov]

Yes, I found has_sum.add_compl and was trying to use it to get an obvious equality, but struggled to find a statement that the tail is summable.
That looks like what I needed, thanks!

[Kevin Buzzard]

There is a subtlety here. Lean only has this result under a well-hidden extra assumption that the series is absolutely convergent. For example I don't think that mathlib has a proof that if the alternating sum of 1/n from 1 converges then the alternating sum from k converges.

[Kevin Buzzard]

This is because Lean's hugely general infinite sum API has as definition of convergence that all finite sums converge with the cofinite topology

[Kevin Buzzard]

So in particular any permutation of the source type won't change summability, or the sum