Stream: Is there code for X?

Topic: break off last term of summation

Benjamin Davidson (Mar 10 2021 at 07:59):

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 (Mar 10 2021 at 08:01):

One pulls off the first term, one the last term

Benjamin Davidson (Mar 10 2021 at 08:11):

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

Benjamin Davidson (Mar 10 2021 at 08:18):

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 (Mar 10 2021 at 10:31):

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

Benjamin Davidson (Mar 11 2021 at 05:06):

Sure, I'll give that a go.

Benjamin Davidson (Mar 11 2021 at 05:31):

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]

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 (Mar 11 2021 at 09:02):

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

Benjamin Davidson (Mar 11 2021 at 09:09):

May I ask what the point of that is?

Eric Wieser (Mar 11 2021 at 09:37):

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

Benjamin Davidson (Mar 12 2021 at 06:27):

Ah I see. Thanks!

Benjamin Davidson (Mar 12 2021 at 06:28):

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

Kevin Buzzard (Mar 12 2021 at 06:46):

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 (Mar 12 2021 at 06:49):

@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 (Mar 14 2021 at 16:42):

See #6676

Last updated: May 17 2021 at 15:13 UTC