Notation for finite sums, products...

Stream: new members

[Miguel Marco]

Hi all,

Is it possible to define a notation like f 1 +...+ f n to mean "the sum of f applied to the numbers from 1 to n"?

I though it might be useful (at least it would for me, since it could allow to write proofs that look more similar to what we do with pen and paper), but couldn't figure out how to define it, since it must look inside the expression f 1 and f n to find both the function f and the indexes 1and n.

[Yaël Dillies]

The ... notation is handwavy on paper, so dropping it is probably a necessary sacrifice.

[Logan Murphy]

Assuming your indices are contiguous integers from 1 to n, inclusive,

def pos_range (n : ℕ) : list ℕ :=
 (list.range n).map (λ x, x + 1)

def sum_range {α : Type*}
  (f : ℕ → α) (n : ℕ) [has_add α] [has_zero α] : α :=
  ((pos_range n).map f).foldl (+) (0 : α)

notation `∑` f `⬝` n :=  sum_range f n

#eval ∑ (λ x, x * 4)  ⬝ 10

[Kevin Buzzard]

We already have finset.sum with notation \sum

[Kyle Miller]

To a limited extent, you can get the first notation to work:

import algebra.big_operators.basic
import data.nat.interval

def dot_sum {α : Type*} [add_comm_monoid α] {f : ℕ → α} {lo hi : ℕ}
  (x : {a : α // a = f lo}) (y : {a : α // a = f hi}) : α :=
(finset.Icc lo hi).sum f

notation a ` +...+ ` b := dot_sum ⟨a, rfl⟩ ⟨b, rfl⟩

#eval id 1 +...+ id 10
-- 55

def f (n : ℕ) : ℕ := 2 * n

#eval f 1 +...+ f 10
-- 110

#eval 1 +...+ 10
-- Random error because it's just a hack. Too much to expect