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
?
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
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