How to use the summation sign in lean?

user_16563251 0
Viewed 302

In lean, there exists a notation for the summation sign (Σ, large Sigma) to write sums with many terms. Sadly, neither the mathlib documentation nor the reference manual seem to provide much information about how it can be used.

What imports are required in order to use it, and how do you write sums with it?

For example, how would you write the theorem that the first n natural numbers add up to n * (n + 1) / 2, using the summation sign?

theorem exmpl (n : ℕ) : --(sum from k=1 to k=n over term n) = n * (n + 1) / 2
lean libraries syntax
2 Answers

Yury's answer is fine, but note that they're using the pathological (to a mathematician) function nat.div for division on naturals; this function has the property that 9 / 2 = 4 for example, because it outputs a natural. Computer scientists may be used to this, but I tend to encourage mathematicians to avoid this function at all costs, because they are used to things like a / b * b = a being true, and this is not true for nat.div. If you coerce into the rationals first, then you'll be using rat.div which behaves in the non-pathological (to a mathematician) way. To prove Yury's results above you'll need to go on a detour to prove that, for example, n*(n+1) is always even. Compare the approach with rationals, where it all drops out easily:

import tactic

open_locale big_operators

open finset

-- sum from i = 0 to n-1 of i^3 is (n(n-1)/2)^2
example (n : ℕ) : (∑ i in range n, i^3 : ℚ) = (n*(n-1)/2)^2 :=
begin
  induction n with d hd,
  { simp, ring },
  { rw [sum_range_succ, hd],
    simp, ring }
end

In other words the proof is "the obvious induction works", and the shortness of the Lean proof indicates that nothing else is going on.

user_68930270

This notation is defined in algebra.big_operators.basic. Here is a minimal working example:

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

open_locale big_operators -- enable notation
open finset

example (n : ℕ) : ∑ k in Icc 1 n, k = n * (n + 1) / 2 := sorry
example (n : ℕ) : ∑ k in range n, k = n * (n - 1) / 2 := sorry
example (n : ℕ) : ∑ k in range (n + 1), k = n * (n + 1) / 2 := sorry

Note that ∑ here is "sum", not "sigma" (Σ).

There is another API defined in algebra.big_operators.finprod:

import algebra.big_operators.finprod

example (n : ℕ) : ∑ᶠ k ≤ n, k = n * (n + 1) / 2 := sorry

The main difference between two APIs is that the former one takes a finset and computes the sum over this finite set while the latter definition takes works for any function but returns zero whenever the function has infinite support. This means that you will have to prove finiteness of {k | k ≤ n ∧ k ≠ 0} to do anything useful with ∑ᶠ k ≤ n, k.

user_122434220
Related