Zulip Chat Archive

Stream: Is there code for X?

Topic: break off last term of summation


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 08:00):

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

view this post on Zulip Kevin Buzzard (Mar 10 2021 at 08:01):

One pulls off the first term, one the last term

view this post on Zulip Benjamin Davidson (Mar 10 2021 at 08:11):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Benjamin Davidson (Mar 11 2021 at 05:06):

Sure, I'll give that a go.

view this post on Zulip 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]

@[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)

view this post on Zulip Eric Wieser (Mar 11 2021 at 09:02):

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

view this post on Zulip Benjamin Davidson (Mar 11 2021 at 09:09):

May I ask what the point of that is?

view this post on Zulip 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

view this post on Zulip Benjamin Davidson (Mar 12 2021 at 06:27):

Ah I see. Thanks!

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Benjamin Davidson (Mar 14 2021 at 16:42):

See #6676


Last updated: May 17 2021 at 15:13 UTC