Zulip Chat Archive

Stream: new members

Topic: changing indices


view this post on Zulip Alex Kontorovich (Apr 15 2020 at 17:44):

Hi, I'm trying to change indices in summation:

lemma diff_sums (F:ℕ→\R) :  j,  i, (j i)   (
  ((range j).sum F) - ((range i).sum F)) =
  (range (j-i)).sum (λ k , F(k+i))
  := sorry

I see that this kind of thing has been done already, e.g., "sum_range_def" in:
https://github.com/leanprover/lean2/blob/master/library/data/nat/bigops.lean

But I'm not able to call sum_range_def (though I am able to call "sum_range_succ" which I think is defined in the same file?)

Help please? Thanks!

view this post on Zulip Alex J. Best (Apr 15 2020 at 17:51):

That repo is from lean2 (the old version of lean) so possibly that particular lemma is not in lean 3 (with the same name).
I think the lemma sum_Ico_eq_sub in algebra/big_operators.lean does half of what you want.

view this post on Zulip Alex J. Best (Apr 15 2020 at 17:57):

So with some minor modifications to your statement this works

lemma diff_sums (F:  ) :  j,  i, (i  j)   (
  ((range j).sum F) - ((range i).sum F)) =
  (range (j-i)).sum (λ k , F(i+k))
  := begin
  intros,
  rw  sum_Ico_eq_sub,
  exact (sum_Ico_eq_sum_range _ _ _),
  assumption,
  end

I changed j \ge ito be i \le j as all lemmas in mathlib are stated with a less than rather than a greater than where possible (so it is best to basically never use greater than, and swap the sides in all statements). And I changed k + i to i + k to match the library version (not necessary but makes the proof one line shorter)


Last updated: May 13 2021 at 20:13 UTC