break off last term of summation

Stream: Is there code for X?

[Benjamin Davidson]

Does the following exist in mathlib?

import algebra.big_operators.intervals
open finset
open_locale big_operators

example {n : ℕ} {f : ℕ → ℕ} : ∑ i in range n.succ, f i = ∑ i in range n, f i + f n :=
by rw [← sum_range_add_sum_Ico f n.le_succ, Ico.succ_singleton, sum_singleton]

I know it follows easily from docs#finset.sum_range_add_sum_Ico, but I was surprised to not find it explicitly.

[Kevin Buzzard]

Isn't it docs#finset.sum_range_succ or docs#finset.sum_range_succ' ?

[Kevin Buzzard]

One pulls off the first term, one the last term

[Benjamin Davidson]

Thank you! I don't know why I couldn't find this.

[Benjamin Davidson]

docs#finset.sum_range_succ has f n + (∑ x in range n, f x) as its RHS. Would it be worthwhile to add a version with an RHS of (∑ x in range n, f x) + f n? I think that would make it easier to find.

[Scott Morrison]

That is strange. Maybe even experiment with just switching the order on the RHS in that lemma?

[Benjamin Davidson]

Sure, I'll give that a go.

[Benjamin Davidson]

Upon taking a closer look, why do both of the following lemmas exist? Is the additive version of the latter not the same as the former?

lemma sum_range_succ {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) :
  (∑ x in range (n + 1), f x) = f n + (∑ x in range n, f x) :=
by rw [range_succ, sum_insert not_mem_range_self]

@[to_additive]
lemma prod_range_succ (f : ℕ → β) (n : ℕ) :
  (∏ x in range (n + 1), f x) = f n * (∏ x in range n, f x) :=
by rw [range_succ, prod_insert not_mem_range_self]

(from lines 651-658 of algebra.big_operators.basic)

[Eric Wieser]

to_additive is not generating a lemma there, it's just linking together the lemmas

[Benjamin Davidson]

May I ask what the point of that is?

[Eric Wieser]

So that to_additive can still be used to generate copies of lemmas that use that lemma

[Benjamin Davidson]

Ah I see. Thanks!

[Benjamin Davidson]

@Scott Morrison Should I then also try to make the same commutative change to the prod lemma?

[Kevin Buzzard]

I don't get it. Why is to_additive not being used to prove the second lemma? Is it one of those weird cases where it doesn't work for some reason?

[Benjamin Davidson]

@Kevin Buzzard Exactly, that's why I did a double-take! Strangely, though, if you remove the first (sum) lemma, the second (prod) lemma breaks, and I'm not sure why.

[Benjamin Davidson]

See #6676