## 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,

--unfold fsum,
transitivity  f (k+1) + fsum f k,
{unfold fsum,},
rw hk,
clear hk,
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

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,