有限離散機率分布：核 PMF 資格、事件機率、期望與推前分布

目標與範圍

隨機變數 X 取值 −1、0、1、2，質量 p(−1)=1/6、p(0)=1/3、p(1)=1/4、p(2)=1/4。（一）先核 p 是否為合格 PMF；（二）求 P(X≥1)；（三）求 E[X]；（四）求 Y=X² 的推前分布、證明它仍是 PMF，求 E[Y] 並以 Σx²p(x) 交叉核對；（五）判定兩個候選 q、r 不是 PMF：q 每項介於 0 與 1 但總和不為 1，r 總和為 1 但有負項。

只處理有限值域、值互異、質量為精確有理數的數學分布（MKO 假設 a1）；不宣稱分布來自樣本估計、資料擬合或真實族群（MKO 假設 a2）。推前分布與重組求和的兩個引理對任意有限值域證明；其餘計算只對給定數字。不處理聯合分布或 Markov 鏈；不改動 canonical MKO 或英文 edition。

已知條件與符號

• frac_rules
• finite_sum_rules
• prob_axioms
• numeric_evaluation

• G1 — X 的值域 R_X={−1,0,1,2}，四個值互異；p(−1)=1/6，p(0)=1/3，p(1)=1/4，p(2)=1/4，都是精確有理數。
• G2 — g(x)=x²，Y=g(X)。
• G3 — 同一值域上的兩個候選：q(−1)=1/2、q(0)=1/3、q(1)=1/4、q(2)=0；r(−1)=1/2、r(0)=2/3、r(1)=−1/6、r(2)=0。
• G4 — 這些分布都是給定的數學分布，不是由觀測資料估計或擬合而來（MKO 假設 a2）。

• R_X=\{-1,0,1,2\} — X 的有限值域
• p(x) — X 的機率質量函數
• P(X\in A) — 事件 A 的機率
• E[X] — X 的期望
• g(x)=x^2,\ Y=g(X) — 推前所用的函數與新隨機變數
• p_Y(y) — Y 的推前質量

規則與來源

• 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）。
• 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。
• prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• 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。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• mko_pmf_def · cited — 有限離散隨機變數的機率質量函數 p 對每個有限值域元素指定非負機率，且所有質量和為 1。事件機率由相應質量相加，期望為值與質量的加權和。 · mko-finite-discrete-probability-distribution
• event_sum · prerequisite — 對值域的子集 A，P(X∈A)=Σ_{x∈A} p(x)；A 以外的值不加入。
• expectation_def · prerequisite — 有限值域的期望：E[X]=Σ_{x∈R_X} x·p(x)。
• pushforward_def · prerequisite — 對函數 g，Y=g(X) 的值域是 R_Y=g(R_X)，推前質量 p_Y(y)=Σ_{x∈R_X, g(x)=y} p(x)，即把映到同一新值的原質量相加。
• sum_over_partition · prerequisite — 若有限集合 S 是兩兩不交的子集 S_y（y∈Y）的聯集，則 Σ_{x∈S} a_x=Σ_{y∈Y} Σ_{x∈S_y} a_x（有限和的結合與交換律）。
• L_pushforward_total · lemma — 若 p 是有限值域 R_X 上的 PMF、g 是定義在 R_X 上的函數，則推前質量 p_Y 是 R_Y=g(R_X) 上的 PMF。
• L_regroup · lemma — 在 L_pushforward_total 的設定下，Σ_{y∈R_Y} y·p_Y(y)=Σ_{x∈R_X} g(x)·p(x)。

逐步主鏈

p:R_X\to\mathbb{Q}

p\ \text{is a PMF}\iff \forall x\in R_X:\ p(x)\ge 0\ \land\ \sum_{x\in R_X}p(x)=1

R_X=\{-1,0,1,2\}

|R_X|=4,\ \text{values distinct}

p(-1)=\tfrac16,\ p(0)=\tfrac13,\ p(1)=\tfrac14,\ p(2)=\tfrac14

\forall x\in R_X:\ p(x)\ge 0

\sum_{x\in R_X}p(x)=\tfrac16+\tfrac13+\tfrac14+\tfrac14

1

p\ge 0,\ \sum p=1

p\ \text{is a PMF on } R_X

A=\{x\in R_X\mid x\ge 1\}

A=\{1,2\}

P(X\ge 1)=\sum_{x\in A}p(x)

\tfrac14+\tfrac14=\tfrac12

P(X\in R_X\setminus A)=\tfrac16+\tfrac13

\tfrac12,\quad P(A)+P(R_X\setminus A)=1

E[X]=\sum_{x\in R_X}x\,p(x)

\tfrac{7}{12}

g(-1)=1,\ g(0)=0,\ g(1)=1,\ g(2)=4

R_Y=\{0,1,4\};\ g^{-1}(0)=\{0\},\ g^{-1}(1)=\{-1,1\},\ g^{-1}(4)=\{2\}

p_Y(y)=\sum_{x\in g^{-1}(y)}p(x)

p_Y(0)=\tfrac13,\ p_Y(1)=\tfrac16+\tfrac14=\tfrac{5}{12},\ p_Y(4)=\tfrac14

p_Y\ \text{on } R_Y=\{0,1,4\}

p_Y\ \text{is a PMF};\ \tfrac13+\tfrac{5}{12}+\tfrac14=1

E[Y]=\sum_{y\in R_Y}y\,p_Y(y)

0\cdot\tfrac13+1\cdot\tfrac{5}{12}+4\cdot\tfrac14=\tfrac{17}{12}

\sum_{y\in R_Y}y\,p_Y(y)

\sum_{x\in R_X}x^2p(x)=\tfrac16+0+\tfrac14+1=\tfrac{17}{12}

\sum_{x}q(x)=\tfrac12+\tfrac13+\tfrac14+0

\tfrac{13}{12}\neq 1;\ q\ \text{is not a PMF}

r(1)=-\tfrac16,\ \sum_x r(x)=1

r\ \text{is not a PMF}

局部子步與引理

\tfrac16+\tfrac13+\tfrac14+\tfrac14

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{3}{12}

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{3}{12}

\tfrac{12}{12}=1

\sum_{x\in R_X}x\,p(x)

(-1)\cdot\tfrac16+0\cdot\tfrac13+1\cdot\tfrac14+2\cdot\tfrac14

(-1)\cdot\tfrac16+0\cdot\tfrac13+1\cdot\tfrac14+2\cdot\tfrac14

-\tfrac{2}{12}+0+\tfrac{3}{12}+\tfrac{6}{12}=\tfrac{7}{12}

p(x)\ge 0\ \forall x

p_Y(y)=\sum_{x\in g^{-1}(y)}p(x)\ge 0

\sum_{y\in R_Y}p_Y(y)=\sum_{y\in R_Y}\sum_{x\in g^{-1}(y)}p(x)

\sum_{x\in R_X}p(x)=1

\sum_{y\in R_Y}y\sum_{x\in g^{-1}(y)}p(x)

\sum_{y\in R_Y}\sum_{x\in g^{-1}(y)}g(x)p(x)=\sum_{x\in R_X}g(x)p(x)

逐步反向審查

• S16 · sufficient_goal_reduction · G3, mko_pmf_def, order_basics — 目標 G：r 不是 PMF。足夠條件 H：有一項為負；H⇒G 由定義。H 直接由 G3 讀出（N13），沒有把 G 當作前提。
• S15 · sufficient_goal_reduction · G3, mko_pmf_def, numeric_evaluation — 目標 G：q 不是 PMF。足夠條件 H：總和不為 1；H⇒G 由定義。H 由精確求和得到（N10、N11），沒有把 G 當作前提。
• S14.1 · inverse_equivalence · distributive, eq_replace, sum_over_partition — 分配律、等值代換與分割求和都是等式，反向依序還原。
• S14 · inverse_equivalence · L_regroup, numeric_evaluation — 引理是等式，雙向成立；兩條獨立算法得到同一個 17/12（N8、N9）。
• S13 · inverse_equivalence · expectation_def, frac_rules, numeric_evaluation — 精確求值（N8），兩邊同一個數。
• S12.2 · inverse_equivalence · sum_over_partition, function_def — 分割求和是等式，兩個方向都成立；關鍵條件是每個 x 恰在一個區塊中，這由 g 是函數保證。
• S12.1 · premise_audit · pushforward_def, order_basics — 只用 p 的非負性；不宣稱 p_Y(y)>0，也不宣稱反向。
• S12 · premise_audit · S05, L_pushforward_total — 引理的前提是 p 為 PMF（S05）與 g 為函數（G2）；數值核對 N7 是一致性檢查，不取代引理。
• S11 · inverse_equivalence · pushforward_def, frac_rules, numeric_evaluation — 每個 p_Y(y) 都是定義式的精確求值（N6），雙向成立。
• S10 · premise_audit · image_preimage_def, G2 — 三個原像兩兩不交且聯集為 R_X，這是 S12.2 會用到的分割性質；g 不是單射，所以不能把 Y 的值一對一對回 X。
• S09.2 · inverse_equivalence · frac_rules, numeric_evaluation — 精確有理數運算，可獨立重算。
• S09.1 · inverse_equivalence · finite_sum_rules — 有限和的展開與收回互為反向。
• S09 · inverse_equivalence · expectation_def, numeric_evaluation — 精確求值（N5），兩邊同一個數。
• S08 · premise_audit · S07, event_sum, prob_axioms — 這是一致性核對，不是新的推論；它確認 S07 沒有漏算或多算。
• S07 · inverse_equivalence · event_sum, frac_rules, numeric_evaluation — 精確求值，兩邊同一個數（N3）。前提是 S05 已確認 p 是 PMF。
• S06 · inverse_equivalence · set_builder — 集合建構記號的成員條件是雙向的；四個值都逐一判定過。
• S05 · sufficient_goal_reduction · S03, S04, mko_pmf_def — 目標 G：p 是 PMF。足夠條件 H：非負且總和為 1；H⇒G 由定義。H 由 S03、S04 正向證成，沒有把 G 當作前提。
• S04.2 · inverse_equivalence · frac_rules, numeric_evaluation — 整數加法與分數規則都是等式，可獨立重算（N2）。
• S04.1 · inverse_equivalence · frac_rules — 約分即反向，前提是乘數不為零。
• S04 · inverse_equivalence · frac_rules, numeric_evaluation — 精確有理數求值，兩邊是同一個數（N1），雙向成立。
• S03 · premise_audit · G1, order_basics — 非負只是資格的一半；它不推出總和為 1。
• S02 · premise_audit · G1, finite_counting_basics — 只核值域的形狀；不涉及質量的大小。
• S01 · premise_audit · mko_pmf_def, prob_axioms — 此步只寫出資格條件，不推出新事實；兩項條件對應機率公理的非負與總機率為 1。

錯誤控制與反例

每項介於 0 與 1 不代表總和為 1

MKO 指出的誤解是只因每項介於 0 與 1 就忽略總和。q 的每一項都在 [0,1] 內，總和卻是 13/12；r 總和為 1 卻有負項。資格必須同時核兩項，並且用精確分數相加，不用小數近似。

理論分布不是資料擬合

MKO 的另一個誤解是把理論 PMF 冒充資料擬合結果。本稿的 1/6、1/3、1/4、1/4 是給定的數學分布（G4），沒有任何觀測資料；說「12 次試驗中恰有 2 次得到 −1」或「這是由樣本估計的分布」都超出本稿能支持的範圍。推前分布也只是精確的數學轉換。

推前要合併同值的質量

−1 與 1 都映到 1，所以 p_Y(1)=1/6+1/4=5/12。若只取 p(1)=1/4，或把值 1 列兩次，總和就不是 1 或值不再互異。另外 E[X²]=17/12 與 (E[X])²=49/144 不同：平方的期望一般不等於期望的平方。

• q 的每一項都介於 0 與 1，所以 q 是 PMF → reject — q 的總和是 13/12≠1。
• r 的總和為 1，所以 r 是 PMF → reject — r(1)=−1/6<0，違反非負。
• P(X≥1)=p(2)=1/4，因為只有 2 大於 1 → reject — 事件是 x≥1，包含 1；P(X≥1)=1/4+1/4=1/2。
• E[X²]=(E[X])²=49/144 → reject — E[X²]=17/12，與 49/144 不同。
• p_Y(1)=p(1)=1/4，因為 g(1)=1 → reject — g(−1)=1 也映到 1，必須相加：p_Y(1)=5/12。

結論與限制

p 非負且總和恰為 1，是合格的 PMF。P(X≥1)=p(1)+p(2)=1/2；E[X]=7/12。Y=X² 的推前分布為 p_Y(0)=1/3、p_Y(1)=5/12、p_Y(4)=1/4，仍是 PMF（對任意有限值域證明），E[Y]=17/12，與 Σx²p(x) 一致。q 每項介於 0 與 1 但總和 13/12，r 總和為 1 但 r(1)=−1/6，兩者都不是 PMF。

• 引理 L_pushforward_total 與 L_regroup 只對有限值域證明；可數或連續情形需要級數或積分，本稿不處理。
• 本稿不處理聯合分布、離散隨機過程或有限 Markov 鏈（MKO 的 formal next），也不做任何統計推論。

驗證及來源綁定

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

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

同源完整 JSON（含公式、AST、反控制與修訂記錄）