10.3 機率空間#

本節目標#

• 理解樣本空間、事件與機率公理（Kolmogorov 公理）。
• 學會用 Mathlib 的 PMF（probability mass function）建構離散機率空間。
• 定義條件機率，敘述 Bayes 定理並做簡單的形式化。
• 例題：生日悖論的敘述與部分形式化。
• 用 Finset.sum 計算機率。

機率空間的公理#

定義：一個（離散）機率空間由三部分組成：

• 樣本空間 \(\Omega\) ：所有可能結果的集合；
• 事件： \(\Omega\) 的子集；

• 機率函數 \(P\) ：把事件映到 \([0, 1]\) 的實數，滿足：

• \(P(\Omega) = 1\) ；

• \(P(A) \ge 0\) ；
• 可數可加性：若 \(A_1, A_2, \dots\) 兩兩互斥，則 \(P(\bigcup_i A_i) = \sum_i P(A_i)\) 。

由公理可推出 \(P(\emptyset) = 0\) 、單調性（ \(A \subseteq B \Rightarrow P(A) \le P(B)\) ）、 以及容斥式 \(P(A \cup B) = P(A) + P(B) - P(A \cap B)\) 。

在離散（有限或可數）世界裡，一切都由「每個點的權重」決定—— 這正是 PMF 的世界。

Mathlib 的 PMF#

定義：PMF α 是函數 \(f : \alpha \to \mathbb{R}_{\ge 0}\) ，且滿足 \(\sum_{a} f(a) = 1\) （可數求和收斂）。

#check @PMF
-- Mathlib 定義（示意）：
-- def PMF (α : Type*) := { f : α → ℝ≥0 // HasSum f 1 }

在有限型別 \(\alpha\) 上，HasSum f 1 就是 Finset.sum 等於 \(1\) 。

最常用的兩個建構子：

-- 均勻分佈：每個點權重 1/n
#check @PMF.uniformOfFintype
-- PMF.uniformOfFintype {α : Type*} [Fintype α] [Nonempty α] : PMF α

-- 常數分佈：全部質量集中在一點
#check @PMF.pure
-- PMF.pure {α : Type*} (a : α) : PMF α

取值：

-- 「某事件發生的機率」：對 PMF p，事件 A 的機率是 ∑_{a ∈ A} p a
#check @PMF.toReal

例：丟一個公平骰子。樣本空間 \(\Omega = \{1, \dots, 6\}\) ，即 Fin 6。

open scoped NNReal

noncomputable example : PMF (Fin 6) := PMF.uniformOfFintype

-- 擲出偶數的機率 = 3/6 = 1/2
noncomputable example :
    (∑ i ∈ {i : Fin 6 | i.val % 2 = 0}, PMF.uniformOfFintype i) = 1/2 := by
  sorry -- 練習：用 Finset.sum 與 uniformOfFintype 的定理化簡

關鍵工具是 Finset.sum：離散機率的計算本質上就是加總權重。 事實上，Mathlib 中「事件的機率」就是把指標函數（indicator）與 PMF 相乘後求和：

#check @PMF.toMeasure -- PMF 可轉成測度（測度論的入口，本書點到為止）

條件機率#

定義：在事件 \(B\) 發生的條件下，事件 \(A\) 的條件機率為

直覺：把全部質量「限制」在 \(B\) 上，再重新正規化使總和為 \(1\) 。

Mathlib 的 PMF.cond 正是這個直覺的形式化：

#check @PMF.cond
-- PMF.cond (p : PMF α) {s : Set α} [h : Nonempty s] : PMF s
-- 把 p 限制在集合 s 上並重新正規化

條件機率的計算性質：對 \(a \in s\) ，

Bayes 定理：

它的證明只是把條件機率定義展開：\(P(A \mid B) P(B) = P(A \cap B) = P(B \mid A) P(A)\)。

在 PMF 語言中，可以敘述如下（骨架）：

-- Bayes 的 PMF 版骨架：對 a, b 屬於相應事件，
-- PMF.cond (p ∘ ... ) 的關係可由 cond 的定義展開驗證。
-- 核心恆等式（有限情形）：
example (p : PMF (Fin 2)) (i j : Fin 2) :
    p i * PMF.cond p {j} i / (∑ k ∈ {j}, p k) = ... := by
  sorry -- 見練習：由 cond 的權重公式直接展開

更務實的做法是把 Bayes 寫成「權重恆等式」：在有限空間上，

（當 \(a \in B\) 時），兩邊都是 Finset.sum 的比值，用場論簡化 （field_simp）即可互推。Bayes 定理不外乎把 \(P(B \mid A)\) 也展開成 比值後相消。

例題：生日悖論#

問題：一個房間裡有 \(n\) 個人，至少兩人生日相同的機率為何？ （假設 365 天、每天等可能，忽略閏年。）

樣本空間： \(\Omega = \{1,\dots,365\}^n\) ，均勻分佈。 事件「全不相同」的機率：

當 \(n = 23\) 時 \(P(\text{至少兩人相同}) > 1/2\) ——這就是「悖論」： 直覺低估了碰撞的機率。

部分形式化（樣本空間與事件）：取 \(d = 365\) （示意可用符號 \(d\) ）：

-- 樣本空間：n 人的生日組合 = Fin d 的 n 次方
-- 在 Mathlib 中，函數型別的 Fintype 實例已齊備：
example (d n : ℕ) [Fintype (Fin d)] : Fintype (Fin d → Fin d) := inferInstance

-- 「全不相同」的事件：
def AllDistinct (d n : ℕ) (f : Fin n → Fin d) : Prop :=
  Function.Injective f

而「全不相同」的機率與乘積公式的關係，本質上是計數：注入函數的 個數 \(= d(d-1)\cdots(d-n+1)\) 。這正是 10.1 節排列數的計數—— 組合數學與機率在此匯流。Mathlib 中相關計數可搜尋 Fintype.card 搭配 Function.Injective 的引理。

用 Finset.sum 計算機率#

小結本節的計算模式：

-- 機率 = 權重的加總：
--   P(A) = ∑ a ∈ A, p a
-- 條件機率 = 縮小樣本空間後重新正規化：
--   cond p s a = p a / (∑ b ∈ s, p b)

所有離散機率計算都可以化約為 Finset.sum 的操作，而 Finset.sum 的性質（線性、重排、分割）我們在前面章節已經練習過。

小結與練習#

本節重點：

• 機率公理： \(P(\Omega) = 1\) 、非負、（可數）可加。
• PMF α：權重非負且總和為 \(1\) 的函數；均勻分佈是 PMF.uniformOfFintype。
• 條件機率 = 限制在事件上重新正規化，對應 PMF.cond。
• Bayes 定理是條件機率定義的代數推論。
• 生日悖論：注入函數的計數給出「全異」機率的乘積公式。

練習：

1. 用 PMF.pure 建構「必然發生」的分佈，並證明取值為 \(1\) 。
2. 證明：對有限 \(\alpha\) 與 PMF \(p\) ， \(\sum_a p\, a = 1\) （這是 PMF 定義在有限情形的展開）。
3. 用 PMF.cond 的權重公式證明：若 \(a \notin s\) 則 \(\mathrm{cond}(p, s)\) 在 \(a\) 上無定義／機率結構為 0 （提示：s 作為子型別， \(a\) 不在型別中）。
4. Bayes 定理：在 PMF 或直接在實數層面，假設 \(P(A), P(B) > 0\) ， 由條件機率定義推出 \(P(A \mid B) = P(B \mid A) P(A) / P(B)\) 。 建議先把兩個條件機率都寫成 Finset.sum 的比值，再 field_simp。
5. 生日悖論：計算 \(n = 23, d = 365\) 時「全異」機率小於 \(1/2\) ——用浮點或 decide 不可行，請寫一個小程式（Python/Lean #eval 搭配 Float）數值驗證，並思考為何 Lean 中精確證明這類不等式 需要不同的技巧（如界估與對數）。
6. Monty Hall（挑戰）：樣本空間取 Fin 3 × Fin 3（獎品位置 × 你最初選的門），均勻分佈。 定義「換門後中獎」的事件為「兩門不同」，證明其機率為 \(2/3\) 。 提示：事件即補集，機率為 \(1 - 1/3\) 。