Zulip Chat Archive

Stream: new members

Topic: Summation over finite integer ranges


Duncan Skahan (Oct 30 2024 at 18:01):

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

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

?

Michael Stoll (Oct 30 2024 at 18:25):

@loogle Finset.sum, Nat, Finset.Ico

loogle (Oct 30 2024 at 18:25):

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

Bjørn Kjos-Hanssen (Oct 30 2024 at 21:16):

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 (Oct 30 2024 at 21:32):

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

Bjørn Kjos-Hanssen (Oct 30 2024 at 22:45):

Still need to take care of the assumption

k1k \ge 1

Arend Mellendijk (Oct 31 2024 at 00:16):

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]

Last updated: May 02 2025 at 03:31 UTC