QiuQiu

Elementary Math

2026-09-06 · 随笔 · 43a908c205b5

读 Lean / Mathlib 证明时会冒出一堆名字,它们不属于正在证的那个领域,而是更底层的常识。课本一句话带过,Lean 要求每一步点名。这里收集这类“底层工具”,每条给出它在 Mathlib 里的名字、它到底说了什么、以及一个在具体证明里怎么用的例子。

等号的三种身份

说了什么

同一个 == 在课本里表达三种不同的东西:

身份 含义 例子 能干什么
定义 左边是新记号,右边是它的意思 φ(t):=f(θ+td)\varphi(t):=f(\theta+td) 随时展开或折叠,不能“解”
恒等式 对范围内所有取值都成立,是定理 (x+1)2=x2+2x+1(x+1)^2=x^2+2x+1,tr⁡(AB)=tr⁡(BA)\operatorname{tr}(AB)=\operatorname{tr}(BA) 改写,把一种形式换成另一种
方程 只对某些取值成立,未知数待求 x2=4x^2=4 解出未知数

分辨方法:问“这个等号里有没有待求的量”。有,是方程;没有且引入了新记号,是定义;没有且两边都是已知的东西,是恒等式。课本偶尔用 ≡\equiv 标恒等式、用 :=:= 或 ≜\triangleq 标定义,多数时候三种都写 ==。

它不是什么

恒等式不是方程。对一个恒等式做“两边求导、代值、解出某个量”的操作,只会得到它自己:一阶 Taylor 行 φ(t)=φ(0)+φ′(0) t+o(t)\varphi(t)=\varphi(0)+\varphi'(0)\,t+o(t) 对所有 tt 成立,里面没有未知数,φ′(0)\varphi'(0) 是由极限定义已经确定的数;想从这一行“解出” φ′(0)\varphi'(0),结果是 φ′(0)=φ′(0)\varphi'(0)=\varphi'(0)。要算 φ′(0)\varphi'(0) 得回到定义或求导法则。

约等 ≈\approx 连等式都不是。f(θ+td)≈f(θ)+t g⊤df(\theta+td)\approx f(\theta)+t\,g^{\top}d 是丢掉余项后的说法,严格版本是恒等式加一条关于余项的断言 r=o(t)r=o(t)。

例子:Lean 把三者分开写

身份 Lean 语法 例子
定义 def … := def φ (t : ℝ) : ℝ := f (θ + t • d)
恒等式 带全称量词的 theorem theorem trace_mul_comm (A B) : trace (A * B) = trace (B * A)
方程 假设或存在量词里的等式 (h : x ^ 2 = 4),或 ∃ x, x ^ 2 = 4

rfl 只能证第一种展开后两边字面相同的等式;rw 用第二种改写目标;第三种需要给出解或从假设推。在 Lean 里用错身份会直接报错,这就是为什么读 Lean 证明时会第一次注意到等号有三种。

为什么小学到高中没人提:练习题几乎全是解方程,等号在直觉里就等于“待解”。到微积分和线性代数,恒等式和定义变成主角,但没人回头说一句“等号换身份了”。

有限求和换序:Finset.sum_comm

说了什么

两层有限求和可以交换内外顺序:

∑i∈s∑j∈tf(i,j)=∑j∈t∑i∈sf(i,j)\sum_{i\in s}\sum_{j\in t} f(i,j)=\sum_{j\in t}\sum_{i\in s} f(i,j)

Mathlib 里的形式:

theorem Finset.sum_comm {s : Finset γ} {t : Finset α} {f : γ → α → β} :
    (∑ x ∈ s, ∑ y ∈ t, f x y) = ∑ y ∈ t, ∑ x ∈ s, f x y

本质只是加法的交换律和结合律用了很多次:把所有 f(i,j)f(i,j) 摆成一张 ∣s∣×∣t∣|s|\times|t| 的表,先按行加再按列加,和先按列加再按行加,得到的是同一堆数的总和。证明对 Finset 做归纳。

分析里叫有限版 Fubini,离散数学里叫双重求和换序。它对任何交换幺半群成立,和线性代数无关。

它不是什么

三个容易混的定理:

名字 换的是什么 形式
mul_comm 两个标量的左右 ab=baab=ba
Finset.sum_comm 两个求和号的内外 ∑i∑j=∑j∑i\sum_i\sum_j=\sum_j\sum_i
Finset.mul_sum / Finset.sum_mul 常数因子进出求和号 c∑kak=∑kc akc\sum_k a_k=\sum_k c\,a_k

第三个是分配律,不是交换律,而且要求 cc 与求和变量 kk 无关。∑kakbk\sum_k a_k b_k 拆不成 (∑kak)(∑kbk)(\sum_k a_k)(\sum_k b_k)。

使用条件

Finset.sum_comm 要求外层范围 ss 和内层范围 tt 都是固定的,内层不能依赖外层变量。像 ∑i∑j≤i\sum_{i}\sum_{j\le i} 这种三角形范围,要用 Finset.sum_comm' 或 Finset.sum_sigma 并显式给出范围变换。

例子:矩阵乘法结合律

目标:(AB)C=A(BC)(AB)C=A(BC)。矩阵乘法按定义(Matrix.mul_apply)展开:

(AB)ij=∑kAik Bkj(AB)_{ij}=\sum_k A_{ik}\,B_{kj}

左边,先把 CljC_{lj} 乘进内层求和(Finset.sum_mul),再用标量结合律 mul_assoc:

((AB)C)ij=∑l(∑kAikBkl)Clj=∑l∑k(AikBkl)Clj=∑l∑kAikBklClj((AB)C)_{ij} =\sum_l\Big(\sum_k A_{ik}B_{kl}\Big)C_{lj} =\sum_l\sum_k (A_{ik}B_{kl})C_{lj} =\sum_l\sum_k A_{ik}B_{kl}C_{lj}

右边,先把 AikA_{ik} 乘进内层求和(Finset.mul_sum),再用 mul_assoc:

(A(BC))ij=∑kAik(∑lBklClj)=∑k∑lAik(BklClj)=∑k∑lAikBklClj(A(BC))_{ij} =\sum_k A_{ik}\Big(\sum_l B_{kl}C_{lj}\Big) =\sum_k\sum_l A_{ik}(B_{kl}C_{lj}) =\sum_k\sum_l A_{ik}B_{kl}C_{lj}

两边的被加项已经完全相同,只差求和号顺序:左边是 ∑l∑k\sum_l\sum_k,右边是 ∑k∑l\sum_k\sum_l。这一步就是 Finset.sum_comm。

每一步用到的定理:

步骤 定理 属于哪层
展开 (AB)ij(AB)_{ij} Matrix.mul_apply 线性代数(定义)
因子进出求和号 Finset.sum_mul、Finset.mul_sum 有限求和
标量结合 mul_assoc 环公理
换求和顺序 Finset.sum_comm 有限求和

为什么这里没有 mul_comm

结合律的证明全程不需要交换标量,所以对非交换环上的矩阵也成立。反过来,AB≠BAAB\ne BA 的原因也能从展开式看出来:

(AB)ij=∑kAikBkj,(BA)ij=∑kBikAkj(AB)_{ij}=\sum_k A_{ik}B_{kj},\qquad (BA)_{ij}=\sum_k B_{ik}A_{kj}

即便在交换环里用 mul_comm 把 AikBkjA_{ik}B_{kj} 换成 BkjAikB_{kj}A_{ik},下标仍是 (ik),(kj)(ik),(kj),和 (BA)ij(BA)_{ij} 的 (ik),(kj)(ik),(kj) 落在不同矩阵上。mul_comm 换的是求和号里面两个标量的左右,Finset.sum_comm 换的是两个求和号的内外,矩阵 ABAB 与 BABA 的差别在下标,两个定理都碰不到它。

Mathlib 层级速查

层 内容 例子
Foundations Lean 类型论、Eq、Nat 归纳、Finset 定义 Eq.trans、Finset.induction_on
抽象代数 幺半群、环的公理和推论 mul_comm、mul_assoc、add_assoc
大算符(BigOperators) 有限求和、有限乘积 Finset.sum_comm、Finset.sum_mul
线性代数 矩阵、线性映射 Matrix.mul_apply、Matrix.mul_assoc

读证明时看到不认识的名字,先按这张表定位它在哪一层,再决定要不要深究。