telescoping sums

Stream: Is there code for X?

[Scott Morrison]

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. :-)

[Johan Commelin]

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

[Jalex Stark]

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 }

[Johan Commelin]

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 :=

[Johan Commelin]

It's called sum_range_sub_of_monotone...

[Jalex Stark]

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

[Johan Commelin]

Aaah, I see.

[Jalex Stark]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Sebastien Gouezel]

Patrick Massot said:

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

... but of course isn't.

[Jalex Stark]

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

[Johan Commelin]

No, hence the :stuck_out_tongue_wink:

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Jalex Stark]

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

[Jalex Stark]

why don't we have has_div for groups?

[Johan Commelin]

I still don't really know

[Jalex Stark]

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

[Johan Commelin]

My initial reaction would be, yes please

[Johan Commelin]

Maybe the big_ops file should be split?

[Jalex Stark]

it is pretty large

[Johan Commelin]

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

[Reid Barton]

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

[Jalex Stark]

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

[Jalex Stark]

#3184

[Reid Barton]

I feel like this is a bad solution.

[Reid Barton]

Type classes are hard enough already.

[Jalex Stark]

I believe you, but I don't understand

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Jalex Stark]

Scott Morrison said:

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

resolved