跳轉到

10.1 組合數學#

本節目標#

  • 理解階乘 \(n!\) 與二項式係數 \(\binom{n}{k}\) 的定義，並熟悉 Mathlib 的 Nat.factorial 與 Nat.choose。
  • 掌握 Pascal 遞迴及其在 Lean 中的形式（Nat.choose_succ_succ）。
  • 認識二項式定理，並學會在 Mathlib 中找到、敘述與使用對應引理。
  • 學習「算兩次」（double counting）的證明技巧。
  • 練習：Vandermonde 恆等式。

階乘#

定義： \(n! = 1 \cdot 2 \cdots n\) ，並約定 \(0! = 1\) 。遞迴寫法是 \(n! = n \cdot (n-1)!\) ， \(0! = 1\) 。

Mathlib 中的 Nat.factorial 正是這個遞迴定義：

#check @Nat.factorial
-- Nat.factorial : ℕ → ℕ
-- Mathlib 定義（示意）：
-- def Nat.factorial : ℕ → ℕ
--   | 0 => 1
--   | n + 1 => (n + 1) * n.factorial

example : Nat.factorial 0 = 1 := rfl
example : Nat.factorial 5 = 120 := by decide
example (n : ℕ) : Nat.factorial (n + 1) = (n + 1) * Nat.factorial n := rfl

階乘的成長速度極快。一個常被用到的基本性質是「 \(n!\) 是正的」：

example (n : ℕ) : 0 < Nat.factorial n := Nat.factorial_pos n

二項式係數的定義#

定義：從 \(n\) 個相異物品中選出 \(k\) 個的方法數記作 \(\binom{n}{k}\) ， 公式為

\[ \binom{n}{k} = \frac{n!}{k! \, (n-k)!} \quad (0 \le k \le n)。 \]

在自然數上，除法不封閉，所以 Mathlib 用一個等價但「整數安全」的定義： Nat.choose n k 定義為滿足遞迴（即 Pascal 三角形）的函數。我們先看 它與階乘公式的關係：

#check @Nat.choose
-- Mathlib 定義（示意）：以 Pascal 遞迴為定義
-- def Nat.choose : ℕ → ℕ → ℕ
--   | _ , 0 => 1
--   | 0, _ + 1 => 0
--   | n + 1, k + 1 => Nat.choose n k + Nat.choose n (k + 1)

example : Nat.choose 5 2 = 10 := by decide
example : Nat.choose 10 3 = 120 := by decide
example (n : ℕ) : Nat.choose n 0 = 1 := Nat.choose_zero_right n
example (n k : ℕ) : Nat.choose n (n + 1) = 0 := Nat.choose_succ_self_right n

若 \(k > n\) ，則 \(\binom{n}{k} = 0\) ：沒得選。

Pascal 遞迴#

定理（Pascal）：對 \(n, k \ge 0\) ，

\[ \binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}。 \]

直覺：考慮第 \(n+1\) 個物品。選它，剩下要從前 \(n\) 個選 \(k\) 個（ \(\binom{n}{k}\) 種）； 不選它，則從前 \(n\) 個選 \(k+1\) 個（ \(\binom{n}{k+1}\) 種）。兩類互斥且窮盡。

Mathlib 中的形式：

#check @Nat.choose_succ_succ
-- Nat.choose_succ_succ (n k : ℕ) :
--   Nat.choose (n + 1) (k + 1) = Nat.choose n k + Nat.choose n (k + 1)

用這條引理可以「算出」任意具體的二項式係數：

example : Nat.choose 6 3 = 20 := by
  rw [Nat.choose_succ_succ]
  rw [Nat.choose_succ_succ]
  rw [Nat.choose_succ_succ]
  decide

二項式定理#

定理（二項式定理）：對任意 \(x, y\) 與 \(n\) ，

\[ (x + y)^n = \sum_{k=0}^{n} \binom{n}{k} x^k y^{n-k}。 \]

在 Mathlib 中，這條定理對交換環成立，稱為 add_pow（把 \(x + y\) 看成 「加法的 \(n\) 次方」）：

#check @add_pow
-- add_pow {R : Type*} [CommSemiring R] (x y : R) (n : ℕ) :
--   (x + y) ^ n = ∑ k ∈ Finset.range (n + 1), n.choose k * x ^ k * y ^ (n - k)

在自然數上即可直接使用：

example (x y : ℕ) (n : ℕ) :
    (x + y) ^ n
      = ∑ k ∈ Finset.range (n + 1), Nat.choose n k * x ^ k * y ^ (n - k) :=
  add_pow x y n

小技巧：Mathlib 的引理命名有規律。若一時想不起名稱，在編輯器中 把游標放在陳述處，使用 exact?（或 apply?）可以自動搜尋引理：

example (x y : ℕ) (n : ℕ) :
    (x + y) ^ n
      = ∑ k ∈ Finset.range (n + 1), Nat.choose n k * x ^ k * y ^ (n - k) := by
  exact? -- 應建議 add_pow x y n

另外，Mathlib 中還有許多與 \(\binom{n}{k}\) 相關的引理，例如「二項式係數 的上界」： \(\binom{n}{k} \le n^k\) 。搜尋關鍵字 choose 搭配 le_pow 之類的名稱即可找到。

算兩次（double counting）#

技巧：要證明 \(\left|A\right| = \left|B\right|\) ，常見做法是找到一個集合 \(S\) 與兩個映射，使得 \(A\) 與 \(B\) 都是 \(S\) 的「分割計數」，於是兩邊都等於 \(\left|S\right|\) 。

最簡單的形式化版本是集合的基數計算。例如：把一個集合拆成兩部分再合併， 總數不變（容斥的特例）：

example (s t : Finset ℕ) (h : Disjoint s t) :
    (s ∪ t).card = s.card + t.card :=
  s.card_union_of_disjoint h

「算兩次」在 Lean 中通常化約為：對同一個 Finset.sum 或 Finset.card 找到兩種不同的計算路徑。一個典型的例子： \(\sum_{k=0}^{n} \binom{n}{k} = 2^n\) ， 直覺上是「每個子集要么在裡、要么不在裡」：

-- 二項式定理取 x = 1, y = 1 即得
example (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n := by
  have h := add_pow (1 : ℕ) 1 n
  simpa using h

這正是算兩次的精神：左邊按「子集大小 \(k\) 」分類計數，右邊按 「每個元素選與不選」計數，兩者計數的是同一批物件—— \([n]\) 的所有子集。

在 Mathlib 中這條恆等式已經內建：

#check @Nat.sum_range_choose
-- Nat.sum_range_choose (n : ℕ) :
--   ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n

小結與練習#

本節重點：

  • Nat.factorial 是遞迴定義，Nat.choose 以 Pascal 遞迴為定義。
  • Pascal 恆等式對應 Nat.choose_succ_succ。
  • 二項式定理在 Mathlib 中是 add_pow，特例 \(\sum_k \binom{n}{k} = 2^n\) 對應 Nat.sum_range_choose。
  • 「算兩次」= 對同一集合找出兩種 Finset.sum / Finset.card 計算路徑。

練習：

  1. 證明 \(\binom{n}{n} = 1\) （提示：Nat.choose_self）。
  2. 證明對稱性 \(\binom{n}{k} = \binom{n}{n-k}\) （提示：Nat.choose_symm， 注意它的前提形式）。
  3. 用 add_pow 證明：對 \(x = 1, y = -1\) （在整數上）， \(\sum_k (-1)^k \binom{n}{k} = 0\) （ \(n \ge 1\) 時）。提示：Mathlib 有 Nat.choose_sum_alternating 或由 add_pow 加減搭配推出。
  4. Vandermonde 恆等式：證明
\[ \binom{m+n}{r} = \sum_{k=0}^{r} \binom{m}{k}\binom{n}{r-k}。 \]

直覺（算兩次）：從 \(m+n\) 人中選 \(r\) 人，按「從前 \(m\) 人中選幾人」分類。 Mathlib 中可搜尋 Nat.sum_choose_choose 或 choose_mul_add_eq 系列； 若直接搜不到，可嘗試用 Finset.sum 重排後套用，或以 induction 對 \(m\) 歸納並使用 Pascal 恆等式。 5. 思考題：為什麼 Mathlib 選擇用 Pascal 遞迴而非階乘公式來定義 Nat.choose？若用階乘公式，哪些性質會變得難證？