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

目標與範圍

隨機試驗：把一枚硬幣擲兩次。(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)}。

逐步主鏈

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

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

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

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

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

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

x\ \text{a possible elementary outcome}

x\in S

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

|S|=2\cdot 2=4

\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\}

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

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

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

S\neq S'

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

P\ \text{is a probability on }S

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

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

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

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

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

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

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

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

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

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

\text{two observation scales and two models}

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

局部子步與引理

x\ \text{possible}

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

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

x\in S

逐步反向審查

• 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、反控制與修訂記錄）