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 i<nf(i)\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