# 有限樣本空間的隨機變數：值域、原像事件與點機率 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-random-variable/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-random-variable-01 · production-20261019-adopted-96 ## 目標與範圍 S={1,2,3,4}，事件族 F=𝒫(S)，權重 w₁=1/2、w₂=1/4、w₃=1/8、w₄=1/8。隨機變數 X:S→ℝ 由表給出：X(1)=1、X(2)=0、X(3)=1、X(4)=4（即 X(s)=(s−2)²）。求 X 的值域、原像事件 {X=1}、{X≥1} 與 {X∈{2,3}}，以及每個值的點機率 P(X=t)，並證明這些點機率之和為 1。 只在 MKO 的有限切片內：S 非空有限、F 為全冪集、X 為總函數，權重是明示的有理數。值域與原像事件只讀函數資料，不使用權重；點機率另用給定權重（MKO 假設 a2）。由權重建立機率律的引理在本稿證明；不處理一般可測空間、連續密度或機率分布的一般表示；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - function_def - image_preimage_def - set_builder - prob_axioms - finite_sum_rules - numeric_evaluation - G1 — S={1,2,3,4} 非空有限，事件族為全冪集 F=𝒫(S)（MKO 假設 a1）。 - G2 — 函數資料：X(1)=1、X(2)=0、X(3)=1、X(4)=4。 - G3 — 點機率題另給權重：w₁=1/2、w₂=1/4、w₃=1/8、w₄=1/8，並令 P(E)=Σ_{s∈E} w_s（E⊆S）。 - S=\{1,2,3,4\} — 樣本空間（基本結果） - w_s — 結果 s 的權重 P(\{s\}) - X:S\to\mathbb{R} — 隨機變數，即整張函數表 - X(S) — X 的值域（去除重複值） - \{X\in T\} — 原像事件 {s∈S ∣ X(s)∈T} ## 規則與來源 - function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。 - image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。 - set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。 - prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。 - finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。 - set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。 - eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_rv_def · cited — 在非空有限樣本空間 S、事件族 F=𝒫(S) 和合法機率律 P 下，實值隨機變數為總函數 X:S→R。對任何實數子集合 T，其原像 {s∈S:X(s)∈T} 是事件；點機率 P(X=t) 是所有 X(s)=t 的結果權重之和。 · mko-random-variable - L_weight_law · lemma — 設 S 有限、F=𝒫(S)，且對所有 s 有 w_s≥0、Σ_{s∈S} w_s=1。則 P(E)=Σ_{s∈E} w_s 滿足：P(E)≥0；P(S)=1；E₁∩E₂=∅ 時 P(E₁∪E₂)=P(E₁)+P(E₂)。 - L_level_partition · lemma — 對總函數 X:S→ℝ 與其值域 R=X(S)，水平集 {X=t}（t∈R）兩兩不交，且其聯集為 S。 ## 逐步主鏈 S01 · implies操作前 w_1=\tfrac12,\ w_2=\tfrac14,\ w_3=\tfrac18,\ w_4=\tfrac18 操作後 w_s\ge 0,\ \sum_{s\in S}w_s=1 條件：無 規則：numeric_evaluation · 依賴：G3 葉節點依據：numeric_evaluation + frac_rules 先驗權重：四個權重都是正有理數，因而非負；總和 1/2+1/4+1/8+1/8=4/8+2/8+1/8+1/8=8/8=1。這是後面使用機率律的前提。 S02 · implies操作前 w_s\ge0,\ \sum_{s}w_s=1 操作後 P(E)=\sum_{s\in E}w_s\ \text{is a valid probability law on}\ \mathcal{P}(S) 條件：S\ \text{finite} 規則：L_weight_law · 依賴：S01, G1 葉節點依據：prob_axioms + finite_sum_rules + order_basics 依引理 L_weight_law，由合法權重定義的 P 滿足機率公理（非負、全空間機率為 1、互斥可加）。因 F=𝒫(S)，每個子集合 E 都是事件，P(E) 都有定義。引理在 S02.1 至 S02.3 證明。 S03 · definition操作前 X(1)=1,\ X(2)=0,\ X(3)=1,\ X(4)=4 操作後 X:S\to\mathbb{R}\ \text{total function} 條件：無 規則：mko_rv_def · 依賴：G1, G2 葉節點依據：function_def + mko_rv_def 四個基本結果各有恰好一個實數值，所以 X 是總函數 S→ℝ，符合 MKO 對隨機變數的定義。X 指的是整張表 s↦X(s)，不是某一次試驗得到的數。 S04 · equivalent操作前 X(S)=\{X(1),X(2),X(3),X(4)\} 操作後 X(S)=\{0,1,4\} 條件：無 規則：image_preimage_def · 依賴：S03 葉節點依據：image_preimage_def + set_extensionality 值域是所有值的集合：{1,0,1,4}。集合不重複計算元素，所以 X(S)={0,1,4}，只有 3 個值，而 S 有 4 個結果；這是因為 X(1)=X(3)=1。 S05 · equivalent操作前 \{X=1\}=\{s\in S\mid X(s)=1\} 操作後 \{1,3\}\in\mathcal{P}(S) 條件：無 規則：image_preimage_def · 依賴：S03, G1 葉節點依據：image_preimage_def + set_builder + set_extensionality 逐一檢查四個結果：X(1)=1 是、X(2)=0 否、X(3)=1 是、X(4)=4 否，所以原像 {X=1}={1,3}。它是 S 的子集合，F=𝒫(S)，因此是事件。這一步只讀函數資料。 S06 · equivalent操作前 P(X=1)=P(\{1,3\}) 操作後 w_1+w_3=\tfrac12+\tfrac18=\tfrac58 條件：無 規則：mko_rv_def · 依賴：S02, S05 葉節點依據：mko_rv_def + def_unfold + numeric_evaluation 點機率是所有 X(s)=1 的結果權重之和：P({1,3})=w₁+w₃=1/2+1/8=5/8。兩個結果都要加上；只算 w₁ 會得到錯誤的 1/2。 S07 · equivalent操作前 \{X=0\},\ \{X=4\} 操作後 \{2\},\ \{4\};\ P(X=0)=\tfrac14,\ P(X=4)=\tfrac18 條件：無 規則：image_preimage_def · 依賴：S02, S03 葉節點依據：image_preimage_def + set_extensionality + def_unfold 同樣掃描：只有 X(2)=0，只有 X(4)=4，所以 {X=0}={2}、{X=4}={4}，點機率分別為 w₂=1/4、w₄=1/8。 S08 · implies操作前 \{X=0\},\ \{X=1\},\ \{X=4\} 操作後 \text{pairwise disjoint},\ \{2\}\cup\{1,3\}\cup\{4\}=S 條件：無 規則：L_level_partition · 依賴：S03, S04 葉節點依據：function_def + set_operations_def 依引理 L_level_partition，值域中各值的水平集構成 S 的分割：兩兩不交、聯集為 S。證明在 S08.1、S08.2；在本例中可直接看到 {2}、{1,3}、{4} 不交且合起來是 {1,2,3,4}。 S09 · implies操作前 P(X=0)+P(X=1)+P(X=4) 操作後 P(S)=1 條件：無 規則：L_weight_law · 依賴：S02, S06, S07, S08 葉節點依據：prob_axioms + set_operations_def + numeric_evaluation 三個水平集兩兩不交（S08），對兩集合可加性用兩次：P({2}∪{1,3}∪{4})=P({2}∪{1,3})+P({4})=P({2})+P({1,3})+P({4})，左邊是 P(S)=1。數值核對：1/4+5/8+1/8=1。所以點機率合起來恰為 1。 S10 · equivalent操作前 \{X\ge 1\}=X^{-1}([1,\infty)) 操作後 \{1,3,4\},\ P=\tfrac12+\tfrac18+\tfrac18=\tfrac34 條件：無 規則：image_preimage_def · 依賴：S02, S03 葉節點依據：image_preimage_def + set_builder + numeric_evaluation 取 T=[1,∞)。以條件 X(s)≥1 篩選結果：X(1)=1、X(3)=1、X(4)=4 符合，X(2)=0 不符合，所以 {X≥1}={1,3,4}，機率為 w₁+w₃+w₄=3/4。 S11 · equivalent操作前 \{X\ge1\}=S\setminus\{X=0\} 操作後 P(X\ge1)=1-\tfrac14=\tfrac34 條件：無 規則：prob_axioms · 依賴：S07, S10, S02 葉節點依據：prob_axioms + set_operations_def + numeric_evaluation 交叉核對：值域中只有 0 小於 1，所以 {X≥1} 是 {X=0}={2} 的補集。依補集規則 P(Eᶜ)=1−P(E)，得 1−1/4=3/4，與 S10 的直接加總相同。 S12 · equivalent操作前 X^{-1}(\{2,3\}) 操作後 \varnothing\in\mathcal{P}(S),\ P(\varnothing)=0 條件：無 規則：image_preimage_def · 依賴：S03, G1 葉節點依據：image_preimage_def + set_builder + prob_axioms 取 T={2,3}：沒有任何結果的值是 2 或 3，所以原像是空集合。空集合也是 S 的子集合，屬於 F=𝒫(S)，是事件，機率為空和 0。這說明 MKO 所說「任何實數子集合的原像都是事件」包含空的情形。 S13 · implies操作前 \text{S04 to S12} 操作後 X(S)=\{0,1,4\};\ P(X=0)=\tfrac14,\ P(X=1)=\tfrac58,\ P(X=4)=\tfrac18;\ \textstyle\sum=1 條件：無 規則：and_intro_elim · 依賴：S04, S05, S06, S07, S09, S10, S12 葉節點依據：and_intro_elim 整理：值域 {0,1,4}；原像事件 {X=1}={1,3}、{X≥1}={1,3,4}、{X∈{2,3}}=∅；點機率 1/4、5/8、1/8，總和為 1。值域與事件只用函數資料，點機率才用權重。 ## 局部子步與引理 S02.1 · implies操作前 w_s\ge 0\ \ (s\in E) 操作後 P(E)=\sum_{s\in E}w_s\ge 0 條件：無 規則：order_basics · 依賴：S01, order_basics 葉節點依據：order_basics + finite_sum_rules 非負數相加仍非負（由 u≥0、v≥0 得 u+v≥v≥0，逐項加入）；空和為 0，所以 P(∅)=0≥0 也成立。 S02.2 · implies操作前 P(S) 操作後 \sum_{s\in S}w_s=1 條件：無 規則：def_unfold · 依賴：S01 葉節點依據：def_unfold + numeric_evaluation 依 P 的定義，P(S) 就是全部權重之和，S01 已算得為 1。 S02.3 · implies操作前 E_1\cap E_2=\varnothing 操作後 \sum_{s\in E_1\cup E_2}w_s=\sum_{s\in E_1}w_s+\sum_{s\in E_2}w_s 條件：E_1\cap E_2=\varnothing 規則：finite_sum_rules · 依賴：finite_sum_rules, set_operations_def 葉節點依據：finite_sum_rules + set_operations_def E₁∪E₂ 中每個結果恰屬於 E₁ 或 E₂ 之一（不交），所以左邊的有限和可以分成兩組重排，每個權重恰好算一次。S02.1 至 S02.3 合起來證得引理 L_weight_law。 S08.1 · implies操作前 s\in\{X=t\}\cap\{X=t'\} 操作後 t=X(s)=t' 條件：無 規則：function_def · 依賴：S03, function_def 葉節點依據：function_def + eq_refl_symm_trans 若 s 同時在 {X=t} 與 {X=t′} 中，則 X(s)=t 且 X(s)=t′；函數在 s 只有一個值，所以 t=t′。因此不同值的水平集沒有共同元素。 S08.2 · implies操作前 s\in S 操作後 s\in\{X=X(s)\},\ X(s)\in X(S) 條件：無 規則：function_def · 依賴：S03, function_def 葉節點依據：function_def + set_extensionality + image_preimage_def X 是總函數，每個 s∈S 都有值 X(s)，它屬於值域，而 s 屬於這個值的水平集。所以水平集的聯集包含 S；反過來每個水平集都是 S 的子集合，故聯集恰為 S。S08.1 與 S08.2 合起來證得引理 L_level_partition。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S04, S05, S06, S07, S09, S10, S12, and_intro_elim — 目標 G 是 goal 中要求的全部結果；足夠條件 H 是各步結論的合取，皆已正向證成，H⇒G 只用合取引入。 - S12 · inverse_equivalence · image_preimage_def, set_builder, prob_axioms — 四個結果都已檢查，沒有一個符合，集合相等；P(∅)=0 由定義（空和）得出。 - S11 · inverse_equivalence · prob_axioms, S02, set_operations_def — 補集規則由可加性與 P(S)=1 推出，是等式，可雙向使用；兩種算法得到同一數值。 - S10 · inverse_equivalence · image_preimage_def, set_builder, S02 — 四個結果都已判定，集合相等；機率依定義相加，兩邊同值。 - S09 · premise_audit · S02, S08, L_weight_law — 第二次使用可加性需要 ({2}∪{1,3})∩{4}=∅，這由兩兩不交推得。數值核對與一般論證一致，但結論由 S08 的分割與可加性證得。 - S08.2 · premise_audit · function_def, set_extensionality, image_preimage_def — 總性保證每個結果都落入一個水平集。若漏掉正權重結果，所列水平集的機率和會小於 1；只漏零權重結果時和仍可為 1，但表仍不是 S 上的總函數。本例全部權重為正，漏任何結果都會失去正質量。 - S08.1 · premise_audit · function_def, eq_refl_symm_trans — 只用到單值性與等號的對稱、傳遞。 - S08 · premise_audit · L_level_partition, S04 — 引理需要 X 是總函數（每個結果有值）且單值（不會同時屬於兩個水平集），兩者由 S03 提供。 - S07 · inverse_equivalence · image_preimage_def, set_extensionality, S02 — 四個結果都已判定，集合相等；機率由定義直接讀出，雙向成立。 - S06 · inverse_equivalence · S02, S05, numeric_evaluation — 依 P 的定義兩邊表示同一個數，精確計算可逆向核對：5/8−1/8=1/2=w₁。 - S05 · inverse_equivalence · image_preimage_def, set_builder, set_extensionality — S 的四個元素都已判定，列出的元素滿足條件、其餘不滿足，兩個集合相同。 - S04 · inverse_equivalence · image_preimage_def, set_extensionality — 兩邊有相同的元素（外延性），列舉的重複不改變集合，雙向成立。 - S03 · premise_audit · G2, function_def, mko_rv_def — 只核對函數定義的兩個要求；沒有使用權重。 - S02.3 · premise_audit · finite_sum_rules, set_operations_def — 不交是本引理採用的充分前提，使每個結果只計一次。若交集含正權重，右邊重複計入該質量，等式會失敗；只有零權重的重疊則不改變數值。本例所有權重都為正，因此本例的任何重疊都造成重複質量。 - S02.2 · premise_audit · S01, def_unfold — 直接展開定義並引用 S01 的數值；若權重總和不是 1，此步就失敗。 - S02.1 · premise_audit · order_basics, finite_sum_rules — 本步只證明每項非負推出有限和非負；不主張逆向「和非負推出每項非負」。非負項的和為 0 時各項為 0 是另一個命題，不是這個逆命題，本步不使用它。 - S02 · premise_audit · S01, L_weight_law, G1 — 需要權重非負且總和恰為 1（S01），以及 S 有限使和式有意義。反向（任何機率律都來自權重）在有限全冪集上也成立，但本稿不需要也不宣稱。 - S01 · premise_audit · G3, numeric_evaluation — 只是精確有理數計算，可獨立重算；結論是權重合法，不涉及 X。 ## 錯誤控制與反例 隨機變數不是一次抽樣結果MKO 的誤解之一是把隨機變數當成一次抽樣得到的數。X 是整張表 s↦X(s)；「X=1」指的是事件 {1,3}，是結果的集合，而 P(X=1)=5/8 是這個事件的機率。某次試驗得到 1 只是一個觀察，不是 X 本身。 值域大小不是機率值域有 3 個值，但這不表示每個值的機率是 1/3。P(X=1)=5/8、P(X=0)=1/4、P(X=4)=1/8，機率只由權重決定。沒有給權重時也不能假設等可能（a2）。 相同輸出值的權重全部相加X(1)=X(3)=1，所以 P(X=1) 必須是 w₁+w₃=5/8。只看第一個找到的結果會得到 1/2，漏掉了結果 3。S08 的分割論證保證每個結果恰被算進一個值。 - X 取三個值，所以 P(X=1)=1/3 → reject — 點機率由權重決定：P(X=1)=w₁+w₃=5/8≠1/3。 - X(1)=1 且 w₁=1/2，所以 P(X=1)=1/2 → reject — 結果 3 也有 X(3)=1，必須加上 w₃=1/8，得 5/8。 - 四個結果中有兩個取值 1，所以 P(X=1)=2/4 → reject — 這假設了等可能，但題目給的權重不相等；依給定權重 P(X=1)=5/8。 - {s: X(s)∈{2,3}} 是空的，所以不是事件 → reject — ∅∈𝒫(S)=F，是事件，機率為 0。 ## 結論與限制 X 是總函數 S→ℝ，值域為 {0,1,4}（三個值，S 有四個結果）。原像事件 {X=1}={1,3}、{X≥1}={1,3,4}、{X∈{2,3}}=∅ 都是事件。點機率 P(X=0)=1/4、P(X=1)=w₁+w₃=5/8、P(X=4)=1/8，因水平集分割 S，三者之和為 1；P(X≥1)=3/4，以補集法交叉核對一致。 - 本稿只處理有限 S 與全冪集事件族；一般可測空間中原像是否為事件需要可測性，另列義務。 - 點機率構成的分布（pushforward）在 S09 只以「總和為 1」描述，未正式定義為新的機率律。 ## 驗證及來源綁定 10 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: e3ee00cdf7973380a94ca35efae4aee08d70223d37aeaa04c4bea83e742cc89e - original source SHA-256: 271553651a5de4e20f2099e671fec4d0d536a0ca7d03824e10700a37afda8f57 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-random-variable-01.json)