Summation over finite integer ranges

Stream: new members

[Duncan Skahan]

Is there a way to do sums over finite integer ranges where it isn't too hard to prove things like

$$\sum_{k=0}^{n-1} a_{n+1} = \sum_{k=1}^n a_n$$

?

[Michael Stoll]

@loogle Finset.sum, Nat, Finset.Ico

[loogle]

:search: Finset.sum_Ico_eq_sum_range, Finset.sum_range_add_sum_Ico, and 55 more

[Bjørn Kjos-Hanssen]

Here's a kind of long solution, using Finset.sum_bijective .

import Mathlib
open Finset
lemma not_too_hard {n : ℕ} (a : ℕ → ℕ) :
    ∑ i : { x // x ∈ filter (fun k => 1 ≤ k) (range n.succ.succ) }, a i.1 =
    ∑ i : { x // x ∈ range n.succ }, a i.1.succ :=
  @sum_bijective (filter (fun k => 1 ≤ k) (range n.succ.succ)) (range n.succ)
    ℕ _ univ univ (fun x => a x) (fun x => a <| Nat.succ x)
    (fun x => ⟨x-1, by
      have : x.1 < n.succ.succ := by aesop
      simp; omega⟩) (by
      constructor
      · intro x y h
        simp at h
        exact Subtype.eq <|Nat.sub_one_cancel (by aesop) (by aesop) h
      · intro x
        use ⟨x.1+1,by simp;exact List.mem_range.mp x.2⟩
        simp
    ) (by simp) (by aesop)

[Yaël Dillies]

Following Michael's hint above, you should be using docs#Finset.sum_range_succ

[Bjørn Kjos-Hanssen]

Still need to take care of the assumption

$$k \ge 1$$

[Arend Mellendijk]

Here's how you can use docs#Finset.sum_map to prove this.

import Mathlib

example (a : ℕ → ℝ) (n : ℕ) :
    ∑ k ∈ Finset.Ico 0 n, a (k+1) = ∑ k ∈ Finset.Ico 1 (n+1), a k := by
  convert Finset.sum_map (Finset.Ico 0 n) (addRightEmbedding 1) a |>.symm using 1
  simp only [Finset.map_add_right_Ico, zero_add]

Or more verbosely

example (a : ℕ → ℝ) (n : ℕ) :
    ∑ k ∈ Finset.Ico 0 n, a (k+1) = ∑ k ∈ Finset.Ico 1 (n+1), a k := calc
  ∑ k ∈ Finset.Ico 0 n, a (k+1) = ∑ k ∈ Finset.Ico 0 n, a (addRightEmbedding 1 k) := by
    simp only [addRightEmbedding_apply]
  _ = ∑ k ∈ Finset.map (addRightEmbedding 1) (Finset.Ico 0 n), a k := by
    simp only [Finset.sum_map]
  _ = ∑ k ∈ Finset.Ico 1 (n+1), a k := by
    simp only [Finset.map_add_right_Ico]