# Zulip Chat Archive

## Stream: new members

### Topic: A simple series lemma

#### Stepan Nesterov (Apr 22 2021 at 20:52):

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 (Apr 22 2021 at 20:56):

#### Yakov Pechersky (Apr 22 2021 at 20:56):

You're asking about `has_sum`

, while that one is about `summable`

#### Stepan Nesterov (Apr 22 2021 at 20:59):

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 (Apr 22 2021 at 21:24):

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 (Apr 22 2021 at 21:26):

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 (Apr 22 2021 at 21:27):

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

Last updated: Dec 20 2023 at 11:08 UTC