sum manipulation

Stream: new members

[Anatole Dedecker]

I'm a little bit struggling with sum manipulation : I want to use the fact that (finset.range n).sum f - (finset.range k).sum f = (finset.range (n-k)).sum (lambda i, f (k+i)) but I can't find anything in the library that would help me to prove it. How would you do this ?

[Anatole Dedecker]

(deleted)

[Patrick Massot]

You should try really hard to avoid anything that involves natural number subtraction. This operation has no good property, it only promises pain.

[Jalex Stark]

this file has lots of stuff
https://leanprover-community.github.io/mathlib_docs/algebra/big_operators.html

[Kevin Buzzard]

It's probably not true if n<k

[Kevin Buzzard]

If n>=k you might be better off writing n=k+t and removing all mention of subtraction

[Jalex Stark]

import tactic

open_locale big_operators
open finset

variables {R : Type*} [comm_ring R]
example (f : ℕ → R) (n m : ℕ) (h : m ≤ n) :
∑ k in range n, f k - ∑ k in range m, f k = ∑ k in range (n - m), f (k - m) :=
begin
sorry
end

[Jalex Stark]

finset.sum_range_add_sum_Ico is pretty close (indeed, it's written without subtraction)

[Anatole Dedecker]

So I should write (finset.range k+t).sum f - (finset.range k).sum f = (finset.range t).sum (lambda i, f (k+i)) ?

[Jalex Stark]

docs#finset.sum_range_add_sum_Ico

[Anatole Dedecker]

Jalex Stark said:

finset.sum_range_add_sum_Ico is pretty close (indeed, it's written without subtraction)

Oh yes, thanks !

[Anatole Dedecker]

It might even be simpler to use with this formulation in my specific case

[Jalex Stark]

for completeness,

import tactic

open_locale big_operators
open finset

variables {R : Type*} [comm_ring R]
example (f : ℕ → R) (n m : ℕ) (h : m ≤ n) :
∑ k in range n, f k - ∑ k in range m, f k = ∑ k in range (n - m), f (m + k) :=
begin
  rw ← sum_range_add_sum_Ico f h,
  simp only [add_sub_cancel'],
  rw sum_Ico_eq_sum_range,
end

[Anatole Dedecker]

Thank you very much !

[Anatole Dedecker]

Thank you very much !

[Jalex Stark]

this exchange would have been easier if you had started with a #mwe, like a statement of a lemma whose proof is sorry

[Anatole Dedecker]

Oh yes, I'll keep that in mind