changing indices

Stream: new members

[Alex Kontorovich]

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!

[Alex J. Best]

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.

[Alex J. Best]

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)