split sum

Stream: new members

[Alex Zhang]

How can I split the following sum? (I.e. how to prove hh?)

import algebra.big_operators.basic
import data.real.basic
import data.set.function

open function

open_locale big_operators

lemma test
  (n : ℕ) (x y: ℕ → ℝ) (σ : fin n → fin n) (perm: bijective σ): tt :=
begin
  induction n with n ih,
  {simp,},
  have hh:
  ∑ (i : fin n.succ), x ↑i * y (n.succ - ↑i - 1)
  =x n * y ↑(σ n) + ∑ (i : fin n), x ↑i * y (n.succ - ↑i - 1),
  {sorry},
end

[Kevin Buzzard]

The machinery we have in lean for doing this kind of maths question is all set up for finset.sum over finset.range so if I was faced with that goal I would translate into that language, but if I were faced with that mathematics then I would try and avoid summing over fin n completely

[Kevin Buzzard]

If you can express everything in this more idiomatic way then a theorem called something like docs#finset.sum_range_succ should do it

[Eric Wieser]

Your statement must be false, because you've assumed y n = y (σ n) for all σ.

[Eric Wieser]

Are you missing a second σ somewhere on either the LHS or RHS?

[Eric Wieser]

I think the lemma you're after is docs#fin.sum_univ_cast_succ, anyway

[Alex Zhang]

I removed y completely now.

[Kevin Buzzard]

aah excellent, I didn't know we had the corresponding lemma for sums over fin. Thanks Eric.

[Eric Wieser]

In future Alex, can you make a true #mwe? One easy way to do so is write extract_goal at the sorry that you're actually stuck at, and then use that instead:

example {R} [ring R] (n : ℕ) (x : ℕ → R)  :
  ∑ (i : fin n.succ), x ↑i = x n + ∑ (i : fin n), x ↑i :=
sorry

[Alex Zhang]

Thanks for your advice!

[Kevin Buzzard]

PS tt is a bool, if you want a Prop there's true

[Alex Zhang]

Suppose I want to use the theorem finset.sum_range_succ, but I don't know whether it exits and what its name is. How can I locate it?

[Eric Wieser]

library_search

[Kevin Buzzard]

Or observe that you're trying to simplify the sum over range (succ n) and so start guessing the name and use ctrl-space to help you look for possible helpful theorems