# Zulip Chat Archive

## Stream: new members

### Topic: list.sum (range (succ n)) =

#### ROCKY KAMEN-RUBIO (May 11 2020 at 17:11):

**Minimal working example:** I want to prove that I can remove the last element from a list sum and add it outside the sum. I get stuck here. I can't find anything in the list documentation that would do this.

```
import tactic
import data.nat.basic
import data.list.basic
example (n : ℕ) : list.sum (list.range (nat.succ n)) = list.sum (list.range n) + (nat.succ n)
:=
begin
unfold list.range list.sum list.range_core,
sorry,
end
```

More context: I want to prove that this `fsum`

is equivalent to the wordier way of summing an expression using `range`

and `sum`

.

```
import tactic
import data.nat.basic
import data.list.basic
def fsum : (ℕ → ℕ) → ℕ → ℕ :=
λ f n, nat.rec_on n (f 0) (λ n' ihn', f (nat.succ n') + ihn')
lemma l0 (f : ℕ → ℕ) (n : ℕ): fsum f n = (list.map f (list.range (n+1))).sum :=
begin
induction n with k hk,
unfold list.range fsum list.sum list.range_core,
simp only [zero_add, list.foldl, list.map],
--unfold fsum,
transitivity f (k+1) + fsum f k,
{unfold fsum,},
rw hk,
clear hk,
--rw nat.succ_eq_add_one,
unfold list.range fsum list.sum list.range_core,
end
```

#### Kevin Buzzard (May 11 2020 at 17:13):

If you were to use `finset.sum`

then this lemma would already be available to you -- it's in the library (IIRC).

#### Jalex Stark (May 11 2020 at 17:14):

if you want to sum a function `f`

from 0 to n-1, would you write this?

`finset.sum (coe (list.range n)) f`

#### Kevin Buzzard (May 11 2020 at 17:19):

The example is incorrect by the way: you should be adding `n`

not `n+1`

at the end. Here's a proof, plus the hint as to how I found it:

```
import tactic
import data.nat.basic
import data.list.basic
example (n : ℕ) : list.range (nat.succ n) = list.range n ++ [n] := by library_search -- list.range_concat n
example (n : ℕ) : list.sum (list.range (nat.succ n)) = list.sum (list.range n) + n
:=
begin
rw list.range_concat,
rw list.sum_append,
rw list.sum_singleton,
end
```

#### Kevin Buzzard (May 11 2020 at 17:19):

`range_concat`

I searched for, and the other two functions I guessed the names and they were there.

#### Kevin Buzzard (May 11 2020 at 17:22):

If I wanted to sum `f`

from `0`

to `n-1`

I'd write

```
import tactic
import data.nat.basic
import data.list.basic
import data.finset
open finset
example (n : ℕ) (f : ℕ → ℤ) : ℤ := (range n).sum f
```

because it feels to me like $\sum_{i<n}f(i)$

#### Jalex Stark (May 11 2020 at 17:22):

Thanks!

#### Jeremy Avigad (May 11 2020 at 17:24):

We are still working on a draft of another chapter for Mathematics in Lean. I am hoping to proofread tonight and post it tomorrow. But coincidentally, there is a section essentially dedicated to `(range n).sum f`

. The draft is here: https://avigad.github.io/mathematics_in_lean/the_natural_numbers.html#sums-and-products. It also explains how to use the summation notation.

#### Kevin Buzzard (May 11 2020 at 17:25):

```
import tactic
import data.nat.basic
import data.list.basic
import data.finset
open finset
example (n : ℕ) : (range(n+1)).sum id = (range(n)).sum id + n
:=
begin
rw finset.sum_range_succ,
apply add_comm,
end
```

Last updated: Dec 20 2023 at 11:08 UTC