如何在精益中使用求和符号？

Question

在 lean 中，存在求和符号（Σ，大西格玛）的符号，用于编写包含许多项的求和。遗憾的是，mathlib documentation nor the reference manual 似乎都没有提供太多关于如何使用它的信息。

使用它需要什么导入，如何用它写求和？

比如第一个n个自然数加起来等于n * (n + 1) / 2的定理，用求和符号怎么写？

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

Answer 1

此符号在 algebra.big_operators.basic 中定义。这是一个最小的工作示例：

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

注意这里的∑是“sum”，不是“sigma”(Σ)。

在algebra.big_operators.finprod中定义了另一个API:

import algebra.big_operators.finprod

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

两个 API 之间的主要区别在于前一个采用 finset 并计算此有限集的总和，而后一个定义适用于任何函数，但 returns 只要函数有无限支持就为零。这意味着您必须证明 {k | k ≤ n ∧ k ≠ 0} 的有限性才能对 ∑ᶠ k ≤ n, k.

做任何有用的事情

Answer 2

Yury 的回答很好，但请注意，他们使用病态的（对数学家而言）函数 nat.div 进行自然除法；例如，此函数具有属性即 9 / 2 = 4，因为它输出自然。计算机科学家可能对此习以为常，但我倾向于鼓励数学家不惜一切代价避免使用此函数，因为他们已经习惯了诸如 a / b * b = a 之类的事情，而 nat.div 则不是这样。如果您首先强制进入有理数，那么您将使用 rat.div 以非病态（对数学家）方式表现。要证明上面 Yury 的结果，您需要绕道去证明，例如，n*(n+1) 总是偶数。将方法与有理数进行比较，在有理数的情况下，它很容易消失：

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

换句话说，证明是“明显的归纳法”，而精益证明的简短表明没有其他事情发生。

如何在精益中使用求和符号？

How to use the summation sign in lean?

syntax

libraries

lean