Zulip Chat Archive

Stream: Is there code for X?

Topic: telescoping sums


view this post on Zulip Scott Morrison (Jun 26 2020 at 11:10):

lemma telescope {M : Type*} [add_comm_group M] (f :   M) (n : ) :
   i in range n, (f (i+1) - f i) = f n - f 0 :=
sorry

I didn't look too hard for this one: I gave up after searching for telescop and only finding something silly involving nat subtraction. :-)

view this post on Zulip Johan Commelin (Jun 26 2020 at 11:17):

I think @Sebastien Gouezel had something similar a little while ago

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:24):

import tactic
open_locale big_operators
open finset

lemma telescope {M : Type*} [add_comm_group M] (f :   M) (n : ) :
 i in range n, (f (i+1) - f i) = f n - f 0 :=
  by { apply sum_range_induction; abel, simp }

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:34):

git grep -n "(f (i+1) - f i) = f n - f 0"
src/algebra/big_operators.lean:560:  ∑ i in range n, (f (i+1) - f i) = f n - f 0 :=

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:35):

It's called sum_range_sub_of_monotone...

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:35):

that's the one scott found. it's about nats.

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:36):

Aaah, I see.

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:36):

i'm working to PR the version for groups right now

view this post on Zulip Patrick Massot (Jun 26 2020 at 12:36):

As you can see from the word monotone which seems completely useless

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:36):

@Jalex Stark Don't forget to tag it with @[to_multiplicative] :stuck_out_tongue_wink:

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 12:36):

Patrick Massot said:

As you can see from the word monotone which seems completely useless

... but of course isn't.

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:38):

i don't understand how to_additive works. is there also a thing called to_multiplicative?

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:38):

No, hence the :stuck_out_tongue_wink:

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:39):

My point is, there is a multiplicative version of this lemma. Prove that, and @[to_additive] will give you the version we are discussing here.

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:39):

Except that the additive version would then and up with f n + - f 0...

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:39):

Because the multiplicative version will have f n * (f 0)^-1

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:40):

I'll do what's done for range_induction, and write both explicitly but have the proof of the additive case be a call to the multiplicative one

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:40):

why don't we have has_div for groups?

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:40):

I still don't really know

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:44):

does it make sense to import tactic.group in algebra.big_operators?

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:44):

My initial reaction would be, yes please

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:45):

Maybe the big_ops file should be split?

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:45):

it is pretty large

view this post on Zulip Johan Commelin (Jun 26 2020 at 12:45):

I can imagine that tactics like abel and ring want to know about finset.{prod,sum}

view this post on Zulip Reid Barton (Jun 26 2020 at 12:58):

Does it make sense for to_additive to learn to turn x * y^-1 into x - y?

view this post on Zulip Jalex Stark (Jun 26 2020 at 12:59):

we should have has_div for group and to_additive should learn to turn x/y into x-y

view this post on Zulip Jalex Stark (Jun 26 2020 at 13:06):

#3184

view this post on Zulip Reid Barton (Jun 26 2020 at 13:07):

I feel like this is a bad solution.

view this post on Zulip Reid Barton (Jun 26 2020 at 13:07):

Type classes are hard enough already.

view this post on Zulip Jalex Stark (Jun 26 2020 at 13:11):

I believe you, but I don't understand

view this post on Zulip Reid Barton (Jun 26 2020 at 13:13):

It's just solving the problem in the wrong way. For instance now you will also have to add a bunch of lemmas to deal with this strange new / for groups.

view this post on Zulip Reid Barton (Jun 26 2020 at 13:14):

Plus, no one really wants / for groups in the first place, I think.

view this post on Zulip Reid Barton (Jun 26 2020 at 13:16):

You're gaining notation that you don't want, and then incurring all the headaches of type classes as a cost.

view this post on Zulip Scott Morrison (Jun 26 2020 at 13:16):

Awesome, thanks! I left some comments on the comments in #3184.

view this post on Zulip Jalex Stark (Jun 26 2020 at 13:37):

Scott Morrison said:

Awesome, thanks! I left some comments on the comments in #3184.

resolved


Last updated: May 07 2021 at 22:14 UTC