# 樣本空間：擲兩次硬幣的兩種觀察尺度與不等可能的結果

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-sample-space/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-sample-space-01 · production-20261019-adopted-96



## 目標與範圍

隨機試驗：把一枚硬幣擲兩次。(1) 若依次記錄結果，寫出樣本空間 S，證明它包含所有可能基本結果且恰有 4 個元素；(2) 若只記錄正面次數，寫出樣本空間 S′={0,1,2}；(3) 在另外給定的機率模型 P（S 的每個有序結果機率 1/4）下，算出 S′ 各結果的機率 1/4、1/2、1/4，說明同一樣本空間中的結果不必等可能；(4) 以 S 上另一個合法的非均勻模型 Q 說明樣本空間本身不決定機率；(5) 分辨結果 (H,T) 與事件 {(H,T),(T,H)}。

在 MKO 的範圍內工作：試驗與觀察尺度明示（假設 a1），樣本空間包含指定描述下的所有可能基本結果（假設 a2）。機率值只在明示給定的模型（G4、G5）中計算，作為後續機率模型的額外資料，不從樣本空間推出。不處理連續或無限樣本空間與測度論；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- finite_counting_basics
- prob_axioms
- image_preimage_def
- finite_prob_weights


- G1 — 試驗：把同一枚硬幣擲兩次。每次擲的結果是 H（正面）或 T（反面），沒有其他結果（不考慮硬幣立起等情況）（假設 a1）。
- G2 — 觀察尺度一：依次記錄兩次結果，成為有序對（第一次，第二次）。
- G3 — 觀察尺度二：只記錄兩次中出現 H 的次數。
- G4 — 機率模型 P（額外資料，不由樣本空間推出）：S 的每個有序結果機率都是 1/4，例如硬幣公正且兩次獨立時採用。
- G5 — 另一個機率模型 Q（額外資料）：Q((H,H))=9/25，Q((H,T))=6/25，Q((T,H))=6/25，Q((T,T))=4/25，例如 H 的機率為 3/5 且兩次獨立時採用。


- H,\ T — 正面、反面
- S — 依次記錄兩次結果時的樣本空間
- S' — 只記錄正面次數時的樣本空間
- h — 把有序結果對應到正面次數的函數
- P,\ Q — S 上兩個不同的機率模型
- P' — 由 P 經 h 得到的 S′ 上的機率





## 規則與來源


- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_sample_space · cited — 若隨機試驗的樣本空間為 S，則每個可能基本結果 x 都滿足 x∈S；空間本身不附帶各結果等可能的假設。 · mko-sample-space
- finite_prob_weights · prerequisite — 有限樣本空間上的點權重：若對每個結果 ω 給定 p(ω)≥0，且所有 p(ω) 的總和為 1，則對 S 的每個子集合 E 令 P(E)=Σ_{ω∈E} p(ω)，所得 P 滿足機率公理。
- L_S_complete · lemma — 在 G1、G2 之下，每個可能基本結果都屬於 S={(H,H),(H,T),(T,H),(T,T)}。





## 逐步主鏈

S01 · definition操作前

\text{experiment: two tosses, recorded in order}

操作後

\text{outcome}=(a,b),\ a,b\in\{H,T\}

條件：無

規則：mko_sample_space · 依賴：G1, G2

葉節點依據：mko_sample_space + def_intro

依 MKO，樣本空間取決於試驗與觀察方式，所以先固定兩者：擲兩次，依次記錄。於是一個基本結果是有序對 (a,b)，a 是第一次結果，b 是第二次結果，各自是 H 或 T（G1）。



S02 · equivalent操作前

\{(a,b)\mid a\in\{H,T\},\ b\in\{H,T\}\}

操作後

\{H,T\}\times\{H,T\}

條件：無

規則：cartesian_product_def · 依賴：S01

葉節點依據：cartesian_product_def + set_builder

所有可能的有序記錄，恰好是 a、b 各自走遍 {H,T} 的有序對；依笛卡兒積定義，這就是 {H,T}×{H,T}。



S03 · equivalent操作前

\{H,T\}\times\{H,T\}

操作後

S=\{(H,H),(H,T),(T,H),(T,T)\}

條件：無

規則：case_analysis · 依賴：S02

葉節點依據：case_analysis + cartesian_product_def + set_extensionality

對 a 分兩種情況（H 或 T），每種情況再對 b 分兩種，共得四個有序對。把它們列出，並把這個集合命名為 S。



S04 · implies操作前

x\ \text{a possible elementary outcome}

操作後

x\in S

條件：無

規則：L_S_complete · 依賴：S01, S03

葉節點依據：forall_intro + case_analysis + cartesian_product_def

依引理 L_S_complete（在 S04.1、S04.2 證明），每個可能基本結果都屬於 S。這正是 MKO 對樣本空間的要求 x∈S，也滿足假設 a2：S 包含所有可能基本結果。



S05 · implies操作前

|\{H,T\}\times\{H,T\}|

操作後

|S|=2\cdot 2=4

條件：H\neq T

規則：finite_counting_basics · 依賴：S02, S03

葉節點依據：finite_counting_basics + cartesian_product_def + numeric_evaluation

依有限計數 |A×B|=|A|·|B|，|S|=2·2=4。列舉中的四個對兩兩不同：例如 (H,T) 與 (T,H) 的第一坐標不同，所以是不同的結果；次序是記錄的一部分。



S06 · definition操作前

\text{ordered outcome }(a,b)\in S

操作後

h:S\to S',\ h(a,b)=\text{number of }H\text{ among }a,b,\ S'=\{0,1,2\}

條件：無

規則：def_intro · 依賴：G3, S03

葉節點依據：def_intro + function_def

換成觀察尺度二（G3）：只記錄 H 的次數。兩次擲出的 H 次數只能是 0、1 或 2，所以第二個樣本空間是 S′={0,1,2}。兩個尺度由函數 h:S→S′ 聯繫，h 把有序結果送到它含有的 H 個數。



S07 · implies操作前

h(H,H),\ h(H,T),\ h(T,H),\ h(T,T)

操作後

2,\ 1,\ 1,\ 0;\quad h(S)=\{0,1,2\}=S'

條件：無

規則：image_preimage_def · 依賴：S03, S04, S06

葉節點依據：image_preimage_def + numeric_evaluation

逐一計算：h(H,H)=2、h(H,T)=1、h(T,H)=1、h(T,T)=0。所以 h 的像 h(S)={0,1,2}=S′：每個可能的 H 次數都在 S′ 中（完整），S′ 的每個值也都可能出現。



S08 · implies操作前

|S|=4,\ |S'|=3

操作後

S\neq S'

條件：無

規則：set_extensionality · 依賴：S05, S07

葉節點依據：set_extensionality + finite_counting_basics

S 的元素是有序對，S′ 的元素是數；兩者的個數也不同（4 與 3）。所以同一試驗在不同觀察尺度下有不同的樣本空間，正如 MKO 所說。



S09 · implies操作前

p(\omega)=\tfrac14\ \ (\omega\in S)

操作後

P\ \text{is a probability on }S

條件：p(\omega)\ge 0; \sum_{\omega\in S}p(\omega)=1

規則：finite_prob_weights · 依賴：G4, S03

葉節點依據：finite_prob_weights + numeric_evaluation

G4 是另外給定的模型資料，不是從 S 推出的。四個權重都 ≥0，總和 4·(1/4)=1，依 finite_prob_weights，P(E)=Σ_{ω∈E} p(ω) 是 S 上的機率。



S10 · equivalent操作前

h^{-1}(\{0\}),\ h^{-1}(\{1\}),\ h^{-1}(\{2\})

操作後

\{(T,T)\},\ \{(H,T),(T,H)\},\ \{(H,H)\}

條件：無

規則：image_preimage_def · 依賴：S07

葉節點依據：image_preimage_def + set_extensionality + numeric_evaluation

依原像定義，h⁻¹({k}) 是 S 中 H 個數為 k 的結果。讀 S07 的值：0 次只有 (T,T)；1 次有 (H,T) 與 (T,H)；2 次只有 (H,H)。三個原像兩兩不相交，聯集是 S。「觀察到 k 次正面」恰好是 S 中的事件 h⁻¹({k}) 發生。



S11 · implies操作前

P'(k)=P(h^{-1}(\{k\}))

操作後

P'(0)=\tfrac14,\ P'(1)=\tfrac12,\ P'(2)=\tfrac14

條件：\{(H,T)\}\cap\{(T,H)\}=\varnothing

規則：prob_axioms · 依賴：S09, S10

葉節點依據：prob_axioms + finite_prob_weights + def_intro + numeric_evaluation

定義 S′ 上的權重 P′(k)=P(h⁻¹({k}))。依 S09 的 P 與有限可加性：P′(0)=P({(T,T)})=1/4；P′(1)=P({(H,T)})+P({(T,H)})=1/4+1/4=1/2；P′(2)=P({(H,H)})=1/4。三者都 ≥0，總和 1/4+1/2+1/4=1，依 finite_prob_weights，P′ 是 S′ 上的機率。



S12 · implies操作前

P'(1)=\tfrac12,\ P'(0)=\tfrac14

操作後

P'(1)\neq P'(0)

條件：無

規則：numeric_evaluation · 依賴：S11

葉節點依據：numeric_evaluation

1/2≠1/4，所以在這個模型中 S′ 的三個結果不是等可能的，儘管它們都是 S′ 的元素。屬於同一樣本空間並不推出等可能。若誤把 S′ 當作等可能，每個結果會得到 1/3，與 P′(1)=1/2 不符。



S13 · implies操作前

Q:\ \tfrac{9}{25},\ \tfrac{6}{25},\ \tfrac{6}{25},\ \tfrac{4}{25}

操作後

Q\ \text{is a probability on }S,\ Q\neq P

條件：\text{weights}\ge 0; \text{total}=1

規則：finite_prob_weights · 依賴：G5, S03, S09

葉節點依據：finite_prob_weights + numeric_evaluation

G5 的四個權重都 ≥0，總和 (9+6+6+4)/25=1，依 finite_prob_weights，Q 也是 S 上的機率。但 Q((H,H))=9/25≠4/25=Q((T,T))，所以 Q 不均勻，也不同於 P。同一個樣本空間 S 承載兩個不同的機率模型，所以 S 本身不附帶等可能的假設。這些權重對應 H 機率 3/5、兩次獨立的情形：(3/5)²=9/25，(3/5)(2/5)=6/25，(2/5)²=4/25。



S14 · implies操作前

(H,T)\in S,\ E=\{(H,T),(T,H)\}

操作後

(H,T)\in E\subseteq S,\ (H,T)\neq E

條件：無

規則：subset_def · 依賴：S03, S10

葉節點依據：subset_def + set_extensionality

(H,T) 是 S 的一個元素，即一個基本結果。「恰好一次正面」對應 E=h⁻¹({1})={(H,T),(T,H)}，它是 S 的子集合，也就是一個事件。(H,T)∈E，但 (H,T)≠E：一個是有序對，一個是含兩個有序對的集合。試驗結果為 (H,T) 時，事件 E 發生。



S15 · implies操作前

\text{two observation scales and two models}

操作後

S=\{H,T\}^2,\ |S|=4;\ S'=\{0,1,2\};\ P'=(\tfrac14,\tfrac12,\tfrac14);\ Q\neq P

條件：無

規則：and_intro_elim · 依賴：S04, S05, S07, S08, S11, S12, S13, S14

葉節點依據：and_intro_elim

彙整：依次記錄時 S 有 4 個元素並包含所有可能結果（S04、S05）；只記錄正面次數時 S′={0,1,2}（S07、S08）；在 G4 之下 S′ 的機率是 1/4、1/2、1/4，不等可能（S11、S12）；S 可承載不同模型（S13）；(H,T) 是結果，{(H,T),(T,H)} 是事件（S14）。







## 局部子步與引理

S04.1 · implies操作前

x\ \text{possible}

操作後

x=(a,b),\ a\in\{H,T\},\ b\in\{H,T\}

條件：無

規則：def_unfold · 依賴：S01, G1

葉節點依據：def_unfold + forall_elim

設 x 是任意一個可能基本結果。依 S01 的觀察尺度，x 是一個有序對 (a,b)；依 G1，每次擲的結果只能是 H 或 T，所以 a、b∈{H,T}。



S04.2 · implies操作前

x=(a,b),\ a,b\in\{H,T\}

操作後

x\in S

條件：無

規則：forall_intro · 依賴：S04.1, S02, S03

葉節點依據：cartesian_product_def + eq_replace + forall_intro

由 S02，(a,b)∈{H,T}×{H,T}；由 S03，這個積等於 S，所以 x∈S。x 是任意的，依 ∀引入，每個可能基本結果都屬於 S。S04.1 與 S04.2 合起來證得引理 L_S_complete。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S04, S05, S07, S08, S11, S12, S13, S14, and_intro_elim — 目標 G 是題目五項結論的合取；每一項都由所列步驟從已知正向證成，此步只做合取，沒有把 G 當作前提。
- S14 · premise_audit · S03, S10, subset_def — E⊆S 由 E 的兩個元素都在 S 中得到（完整檢查）。不宣稱結果與事件可以互換。
- S13 · premise_audit · G5, finite_prob_weights, numeric_evaluation — Q 的合法性只需非負與總和為 1（N6）；與獨立性的對應只是說明權重的來源，論證不依賴它（N7 到 N9 只核對算術）。
- S12 · premise_audit · S11, numeric_evaluation — 只需比較兩個明確的有理數（N5）。結論只針對 G4 的模型；不宣稱 S′ 在任何模型下都不等可能。
- S11 · premise_audit · S09, S10, prob_axioms, finite_prob_weights — 可加性只用在不相交的單點事件 {(H,T)} 與 {(T,H)}；P′ 的值完全依賴 G4 的模型，不依賴 S′ 本身。
- S10 · inverse_equivalence · image_preimage_def, set_extensionality — 每個原像都由 S 的四個元素逐一判定，兩邊元素相同，雙向成立。
- S09 · premise_audit · G4, finite_prob_weights, prob_axioms — 需要非負與總和為 1 兩個條件，N2 核對後者。此步不宣稱 G4 是唯一可能的模型（S13 給出另一個）。
- S08 · premise_audit · S05, S07, set_extensionality — 個數不同就足以說明兩集合不等。兩者都是合法的樣本空間，各自相對於自己的觀察尺度。
- S07 · premise_audit · S03, S04, image_preimage_def, L_S_complete — 因 S 已含所有可能結果（S04），h(S) 就是所有可能的 H 次數；這是對 S 四個元素的完整計算，不是抽樣。
- S06 · premise_audit · G3, def_intro — 此步只定義；S′ 的完整性在 S07 以 h 的值核對。
- S05 · premise_audit · finite_counting_basics, cartesian_product_def — 需要 {H,T} 有兩個不同元素（H≠T）；結論只是個數，不涉及機率。
- S04.2 · premise_audit · S02, S03, forall_intro — 需要 S03 的集合相等；不宣稱 S 的元素出現機率相同。
- S04.1 · premise_audit · G1, S01 — 只用到 G1、G2 對試驗與記錄方式的描述；x 是任意的。
- S04 · premise_audit · L_S_complete, G1 — 完整性依賴 G1 的「每次只有 H 或 T」；若試驗允許硬幣立起，S 就不完整。
- S03 · inverse_equivalence · case_analysis, cartesian_product_def, set_extensionality — 分情況窮盡 {H,T} 的兩個值，所以列舉的集合與笛卡兒積元素相同：每個列出的對都在積中，積的每個元素也都被列出。
- S02 · inverse_equivalence · cartesian_product_def — 這是笛卡兒積定義的直接改寫，兩個方向都由定義保證。
- S01 · premise_audit · G1, G2, mko_sample_space — 此步只明示試驗與觀察尺度（假設 a1），不推出新事實；換一種記錄方式會得到不同的樣本空間（見 S06）。





## 錯誤控制與反例

同一樣本空間不代表等可能MKO 指出常見誤解是認為同一樣本空間中的結果必定等可能。S′={0,1,2} 是合法的樣本空間，但在模型 P 下三個結果的機率是 1/4、1/2、1/4（S11），不是各 1/3。就連 S 上的均勻權重也是 G4 另外給的資料；G5 的 Q 在同一個 S 上並不均勻（S13）。

結果不是事件MKO 提醒不要把單一結果與事件集合混為一談。(H,T) 是 S 的元素；「恰好一次正面」在 S 中是事件 {(H,T),(T,H)}，含兩個結果（S14）。同一句描述在 S′ 中對應結果 1，在 S 中對應一個事件；判斷時要先說清楚用的是哪個樣本空間。

漏掉可能結果依次記錄時，(H,T) 與 (T,H) 是不同的結果（S05）。若把 S 寫成 {(H,H),(H,T),(T,T)}，就漏掉了可能結果 (T,H)，違反假設 a2；之後事件與機率計算都會失去正確的論域。L_S_complete 的證明（S04.1、S04.2）正是用來排除這種遺漏。


- S′={0,1,2} 是樣本空間，所以每個結果的機率都是 1/3 → reject — 在模型 P 下 P′(1)=1/2≠1/3（S11）；樣本空間不附帶等可能假設。
- S 有 4 個元素，所以 (H,H) 的機率必為 1/4 → reject — 在同一個 S 上，模型 Q 給 (H,H) 機率 9/25（S13）。
- 依次記錄時，{(H,H),(H,T),(T,T)} 是樣本空間 → reject — (T,H) 是可能結果卻不在其中，違反假設 a2。
- (H,T) 與 {(H,T),(T,H)} 是同一個對象 → reject — 前者是有序對（結果），後者是含兩個元素的集合（事件）。
- S 與 S′ 不同，所以其中至少一個不是這個試驗的樣本空間 → reject — 兩者各自相對於不同的觀察尺度（G2、G3），都是合法的樣本空間（S04、S07）。





## 結論與限制

依次記錄兩次擲硬幣時，樣本空間 S={(H,H),(H,T),(T,H),(T,T)} 包含所有可能基本結果，恰有 4 個元素；只記錄正面次數時樣本空間是 S′={0,1,2}。在另外給定的模型 P 下，S′ 的結果機率為 1/4、1/2、1/4，並不等可能；S 上也可以有非均勻的模型 Q。所以樣本空間只說明哪些結果可能，不決定機率。(H,T) 是結果，{(H,T),(T,H)} 是事件。


- G4、G5 是模型假設；本稿不討論它們是否符合某枚實際硬幣，那是統計問題。
- finite_prob_weights 作為前置知識使用，未在本稿中由機率公理推出。





## 驗證及來源綁定

11 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: c0d1f9b0e3d3e27afde0183074318b955b8122887189e0f0232556ac536804a1
- original source SHA-256: c0d1f9b0e3d3e27afde0183074318b955b8122887189e0f0232556ac536804a1
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-sample-space-01.json)