有限樣本空間的隨機變數：值域、原像事件與點機率

目標與範圍

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 — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• 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。

逐步主鏈

w_1=\tfrac12,\ w_2=\tfrac14,\ w_3=\tfrac18,\ w_4=\tfrac18

w_s\ge 0,\ \sum_{s\in S}w_s=1

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)

X(1)=1,\ X(2)=0,\ X(3)=1,\ X(4)=4

X:S\to\mathbb{R}\ \text{total function}

X(S)=\{X(1),X(2),X(3),X(4)\}

X(S)=\{0,1,4\}

\{X=1\}=\{s\in S\mid X(s)=1\}

\{1,3\}\in\mathcal{P}(S)

P(X=1)=P(\{1,3\})

w_1+w_3=\tfrac12+\tfrac18=\tfrac58

\{X=0\},\ \{X=4\}

\{2\},\ \{4\};\ P(X=0)=\tfrac14,\ P(X=4)=\tfrac18

\{X=0\},\ \{X=1\},\ \{X=4\}

\text{pairwise disjoint},\ \{2\}\cup\{1,3\}\cup\{4\}=S

P(X=0)+P(X=1)+P(X=4)

P(S)=1

\{X\ge 1\}=X^{-1}([1,\infty))

\{1,3,4\},\ P=\tfrac12+\tfrac18+\tfrac18=\tfrac34

\{X\ge1\}=S\setminus\{X=0\}

P(X\ge1)=1-\tfrac14=\tfrac34

X^{-1}(\{2,3\})

\varnothing\in\mathcal{P}(S),\ P(\varnothing)=0

\text{S04 to S12}

X(S)=\{0,1,4\};\ P(X=0)=\tfrac14,\ P(X=1)=\tfrac58,\ P(X=4)=\tfrac18;\ \textstyle\sum=1

局部子步與引理

w_s\ge 0\ \ (s\in E)

P(E)=\sum_{s\in E}w_s\ge 0

P(S)

\sum_{s\in S}w_s=1

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

s\in\{X=t\}\cap\{X=t'\}

t=X(s)=t'

s\in S

s\in\{X=X(s)\},\ X(s)\in X(S)

逐步反向審查

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