finite sum

Stream: new members

[Junjie Bai]

How can I write the finite sum from 0 to some integer i?

[Johan Commelin]

docs#Finset.sum and docs#Finset.range

[Kevin Buzzard]

and docs#Nat.succ :-) (because range i is $0\leq x<i$)

[Junjie Bai]

That helps! but I get a new question: I want to sum some function from \Z to \N, but Finset.range return the type of Finset \N, how can I solve this?

[Xiyu Zhai]

docs#Finset.Ioo ?

[Kyle Miller]

There's no problem with Finset \N, since Lean inserts coercions.

open BigOperators
example (f : ℤ → ℕ) (i : ℕ) := ∑ x in Finset.range (i + 1), f x

-- Equivalent:
example (f : ℤ → ℕ) (i : ℕ) := (Finset.range (i + 1)).sum (fun x => f x)

[Kyle Miller]

This is nice too:

example (f : ℤ → ℕ) (i : ℕ) := ∑ x in Finset.Icc 0 i, f x

(Icc is "interval closed to closed")

[Kyle Miller]

Or you can use an "Iverson bracket" (indicator function) approach using an infinite sum:

∑' x, (if 0 ≤ x ∧ x ≤ i then 1 else 0) * f x

[White Chen]

Maybe this helps: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/how.20to.20spell.20tsum.20in.20a.20set.3F

[Junjie Bai]

That helps a lot! Thank you!