list.sum (range (succ n)) =

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

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

[Jalex Stark]

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]

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]

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

[Kevin Buzzard]

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]

Thanks!

[Jeremy Avigad]

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]

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