# 有限模型的期望值：線性性的證明與相依變數的實例 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-expectation/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-expectation-01 · production-20261019-adopted-96 ## 目標與範圍 在非空有限樣本空間 S、非負且總和為 1 的權重 w_s 下，證明 E[c]=c、E[aX+b]=aE[X]+b、E[X+Y]=E[X]+E[Y]（X、Y 定義在同一個 S 上，不假設獨立）。再在 S={1,2,3}、w₁=1/2、w₂=1/4、w₃=1/4，X=(2,−2,0)、Y=(1,3,−1) 上計算 E[X]、E[Y]、E[X+Y]、E[−3X+5]，說明 X、Y 不獨立而線性性仍成立，並以 E[XY]≠E[X]E[Y] 說明線性性不推出乘積公式。 限定 MKO 的有限已知機率模型：權重非負且總和恰為 1，變數在同一個有限 S 上總定義，一般有限和性質容許 G1 的實數係數 a、b、c 與非負歸一化權重；具體例子採整數係數與明示有理權重，全部精確計算（a1、a2）。一般性質以有限和證明；實例只作驗證與反例。不處理樣本平均、長期收斂、無限樣本空間或可積性；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - finite_sum_rules - distributive - function_def - prob_axioms - numeric_evaluation - G1 — 一般模型：S 非空有限，對所有 s 有 w_s≥0，Σ_{s∈S} w_s=1；X、Y:S→ℝ 在同一個 S 上總定義；a、b、c 為實數。 - G2 — 實例：S={1,2,3}，w₁=1/2、w₂=1/4、w₃=1/4。 - G3 — X(1)=2、X(2)=−2、X(3)=0；Y(1)=1、Y(2)=3、Y(3)=−1。 - w_s — 結果 s 的權重 - E[Z]=\sum_{s\in S}w_sZ(s) — Z 的期望值 - X,Y — 同一個 S 上的兩個隨機變數 - a,b,c — 實數常數 - XY — 逐點乘積 s↦X(s)Y(s) ## 規則與來源 - 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。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。 - prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_expectation_def · cited — 對非空有限 S、歸一化非負權重 w_s 與實值隨機變數 X，定義 E[X]=Σ_(s∈S)w_s X(s)。在同一機率模型上 E[aX+b]=aE[X]+b、E[X+Y]=E[X]+E[Y]，不需假設 X、Y 獨立；常數 c 的期望為 c。 · mko-expectation - pointwise_rv · prerequisite — 同一個 S 上的隨機變數逐點運算：(aX+b)(s)=aX(s)+b，(X+Y)(s)=X(s)+Y(s)，(XY)(s)=X(s)Y(s)；常數 c 是函數 s↦c。 - indep_def · prerequisite — 有限模型中 X 與 Y 獨立，指對所有實數 x、y 有 P(X=x 且 Y=y)=P(X=x)P(Y=y)，其中每個機率是符合條件的結果權重之和。 - L_const · lemma — 在 G1 的模型中，對常數 c：E[c]=c。 - L_affine · lemma — 在 G1 的模型中：E[aX+b]=aE[X]+b。 - L_sum · lemma — 在 G1 的模型中，X、Y 定義在同一個 S 上：E[X+Y]=E[X]+E[Y]。 ## 逐步主鏈 S01 · definition操作前 Z:S\to\mathbb{R} 操作後 E[Z]=\sum_{s\in S}w_sZ(s) 條件：w_s\ge0,\ \sum_s w_s=1 規則：mko_expectation_def · 依賴：G1, pointwise_rv 葉節點依據：mko_expectation_def + pointwise_rv 依 MKO 定義期望值：每個結果的值乘上它的權重，再對全部結果相加。aX+b、X+Y、XY 與常數 c 都是同一個 S 上逐點定義的隨機變數，所以也都有期望值。 S02 · implies操作前 w_1=\tfrac12,\ w_2=\tfrac14,\ w_3=\tfrac14 操作後 w_s\ge0,\ \sum_s w_s=1 條件：無 規則：numeric_evaluation · 依賴：G2 葉節點依據：numeric_evaluation 先驗實例的權重：三者都為正，總和 1/2+1/4+1/4=1。MKO 要求先驗權重再計算期望。 S03 · equivalent操作前 E[c] 操作後 c 條件：\sum_s w_s=1 規則：L_const · 依賴：S01 葉節點依據：finite_sum_rules + mul_one 依引理 L_const，常數的期望就是該常數。證明在 S03.1，關鍵是權重總和恰為 1。 S04 · equivalent操作前 E[aX+b] 操作後 aE[X]+b 條件：\sum_s w_s=1 規則：L_affine · 依賴：S01 葉節點依據：distributive + finite_sum_rules + def_unfold 依引理 L_affine，仿射變換的期望等於期望的仿射變換。證明分三個子步：逐點展開、拆開和式、代回定義與歸一化。 S05 · equivalent操作前 E[X+Y] 操作後 E[X]+E[Y] 條件：X,Y\ \text{on the same}\ S 規則：L_sum · 依賴：S01 葉節點依據：distributive + finite_sum_rules + def_unfold 依引理 L_sum，和的期望等於期望的和。證明只用到 X、Y 定義在同一個 S 上，沒有用到任何關於 X、Y 聯合行為的假設，所以不需要獨立性。 S06 · equivalent操作前 E[X] 操作後 \tfrac12\cdot2+\tfrac14\cdot(-2)+\tfrac14\cdot0=\tfrac12 條件：無 規則：mko_expectation_def · 依賴：S01, S02, G3 葉節點依據：mko_expectation_def + numeric_evaluation 代入定義：1/2·2+1/4·(−2)+1/4·0=1−1/2+0=1/2。注意 1/2 不是 X 的任何一個可能值（X 只取 2、−2、0）。 S07 · equivalent操作前 E[Y] 操作後 \tfrac12\cdot1+\tfrac14\cdot3+\tfrac14\cdot(-1)=1 條件：無 規則：mko_expectation_def · 依賴：S01, S02, G3 葉節點依據：mko_expectation_def + numeric_evaluation 同理：1/2+3/4−1/4=1。 S08 · implies操作前 E[X+Y],\ X+Y=(3,1,-1) 操作後 E[X+Y]=\tfrac32=E[X]+E[Y] 條件：無 規則：L_sum · 依賴：S05, S06, S07, G3 葉節點依據：mko_expectation_def + numeric_evaluation 依 S05，E[X+Y]=E[X]+E[Y]=1/2+1=3/2。直接核對：X+Y 的逐點值為 3、1、−1，1/2·3+1/4·1+1/4·(−1)=3/2，兩者一致。 S09 · implies操作前 E[-3X+5],\ -3X+5=(-1,11,5) 操作後 E[-3X+5]=-3\cdot\tfrac12+5=\tfrac72 條件：無 規則：L_affine · 依賴：S04, S06, G3 葉節點依據：mko_expectation_def + numeric_evaluation 依 S04（a=−3、b=5）：E[−3X+5]=−3·(1/2)+5=7/2。直接核對：逐點值 −1、11、5，1/2·(−1)+1/4·11+1/4·5=−1/2+4=7/2。 S10 · implies操作前 P(X=2,\,Y=1)=w_1=\tfrac12,\ P(X=2)P(Y=1)=\tfrac14 操作後 X,Y\ \text{not independent} 條件：無 規則：indep_def · 依賴：G2, G3, indep_def 葉節點依據：indep_def + quantifier_negation + numeric_evaluation 只有結果 1 有 X=2，也只有結果 1 有 Y=1，所以 P(X=2)=1/2、P(Y=1)=1/2，而 P(X=2 且 Y=1)=w₁=1/2。乘積 1/4≠1/2，獨立的定義在 x=2、y=1 失敗，X、Y 不獨立。然而 S08 仍成立：線性性不需要獨立。 S11 · implies操作前 XY=(2,-6,0) 操作後 E[XY]=-\tfrac12\neq\tfrac12=E[X]E[Y] 條件：無 規則：mko_expectation_def · 依賴：S01, S06, S07, G3 葉節點依據：mko_expectation_def + pointwise_rv + numeric_evaluation 逐點乘積 XY 的值為 2·1=2、(−2)·3=−6、0·(−1)=0，E[XY]=1/2·2+1/4·(−6)+1/4·0=1−3/2=−1/2。但 E[X]E[Y]=1/2·1=1/2。所以由線性性不能推出 E[XY]=E[X]E[Y]；期望也可以是負數。 S12 · implies操作前 \tfrac{2+(-2)+0}{3}=0 操作後 0\neq\tfrac12=E[X] 條件：無 規則：mko_expectation_def · 依賴：S06, G3 葉節點依據：mko_expectation_def + numeric_evaluation 若把三個值當成等可能而取普通平均，得 0，與 E[X]=1/2 不同。題目給的權重是 1/2、1/4、1/4，不是各 1/3，所以普通平均不是本模型的期望值。 S13 · implies操作前 \text{S03 to S12} 操作後 E[c]=c,\ E[aX+b]=aE[X]+b,\ E[X+Y]=E[X]+E[Y];\ E[XY]\neq E[X]E[Y]\ \text{here} 條件：無 規則：and_intro_elim · 依賴：S03, S04, S05, S08, S09, S10, S11 葉節點依據：and_intro_elim 整理：三條線性性質對所有有限合法模型成立（S03 至 S05）；實例中 E[X]=1/2、E[Y]=1、E[X+Y]=3/2、E[−3X+5]=7/2，X、Y 相依而線性性照樣成立，E[XY]=−1/2 則不等於 E[X]E[Y]=1/2。 ## 局部子步與引理 S03.1 · equivalent操作前 \sum_{s\in S}w_s\,c 操作後 c\sum_{s\in S}w_s=c\cdot 1=c 條件：\sum_s w_s=1 規則：finite_sum_rules · 依賴：S01, G1, finite_sum_rules 葉節點依據：finite_sum_rules + mul_comm + mul_one 依有限和規則提出常數 c：Σ w_s c=cΣ w_s；再用 G1 的 Σ w_s=1 得 c·1=c。若權重總和不是 1，結果會是 c 乘以總和，而不是 c。此步證得引理 L_const。 S04.1 · equivalent操作前 \sum_{s}w_s\,(aX(s)+b) 操作後 \sum_{s}\bigl(a\,w_sX(s)+b\,w_s\bigr) 條件：無 規則：distributive · 依賴：S01, pointwise_rv, distributive 葉節點依據：distributive + mul_comm + mul_assoc + eq_replace 依逐點定義，(aX+b)(s)=aX(s)+b；對每個 s 用分配律與乘法交換律：w_s(aX(s)+b)=a·w_sX(s)+b·w_s。每一項都換成相等的式子。 S04.2 · equivalent操作前 \sum_{s}\bigl(a\,w_sX(s)+b\,w_s\bigr) 操作後 a\sum_{s}w_sX(s)+b\sum_{s}w_s 條件：無 規則：finite_sum_rules · 依賴：S04.1, finite_sum_rules 葉節點依據：finite_sum_rules 有限和可拆成兩個和（Σ(u_s+v_s)=Σu_s+Σv_s），常數可提出（Σ c·u_s=cΣu_s）。 S04.3 · equivalent操作前 a\sum_{s}w_sX(s)+b\sum_{s}w_s 操作後 aE[X]+b\cdot1=aE[X]+b 條件：\sum_s w_s=1 規則：def_unfold · 依賴：S04.2, S01, G1 葉節點依據：def_unfold + mul_one 第一個和依定義正是 E[X]；第二個和由 G1 等於 1。S04.1 至 S04.3 合起來證得引理 L_affine。常數 b 被乘上的是總權重 1，不是結果個數。 S05.1 · equivalent操作前 \sum_{s}w_s\,(X(s)+Y(s)) 操作後 \sum_{s}\bigl(w_sX(s)+w_sY(s)\bigr) 條件：X,Y\ \text{on the same}\ S 規則：distributive · 依賴：S01, pointwise_rv, distributive 葉節點依據：distributive + pointwise_rv + eq_replace 因 X、Y 在同一個 S 上，(X+Y)(s)=X(s)+Y(s) 對每個 s 都有定義；再對每項用分配律。若兩者定義在不同樣本空間上，逐點和根本沒有意義。 S05.2 · equivalent操作前 \sum_{s}\bigl(w_sX(s)+w_sY(s)\bigr) 操作後 \sum_{s}w_sX(s)+\sum_{s}w_sY(s)=E[X]+E[Y] 條件：無 規則：finite_sum_rules · 依賴：S05.1, finite_sum_rules, S01 葉節點依據：finite_sum_rules + def_unfold 拆開有限和，兩個和依定義分別是 E[X] 與 E[Y]。S05.1 與 S05.2 合起來證得引理 L_sum；整個過程沒有出現 P(X=x 且 Y=y)，所以與獨立與否無關。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S03, S04, S05, S08, S09, S10, S11, and_intro_elim — 目標 G 為 goal 中的證明與計算；足夠條件 H 為各步結論的合取，皆已正向證成，H⇒G 只用合取引入。 - S12 · premise_audit · S06, numeric_evaluation — 這裡只是比較本例的兩個數。對所有實值 X 都保證普通平均等於期望值，當且僅當每個權重都等於 1/|S|；對單一 X，非均勻權重也可能偶合相等（例如常數 X）。 - S11 · premise_audit · mko_expectation_def, pointwise_rv, numeric_evaluation — 一個反例就足以否定「乘積期望總等於期望乘積」；本步不討論獨立時乘積公式是否成立。 - S10 · premise_audit · indep_def, numeric_evaluation, quantifier_negation — 獨立要求對所有 x、y 成立，一組 (x,y) 失敗就足以否定。 - S09 · premise_audit · S04, S06 — 負係數 a 也適用，因引理對所有實數 a、b 成立；直接計算只是核對。 - S08 · premise_audit · S05, S06, S07 — 結論由一般引理得到；直接計算只是交叉核對，不是證明的來源。 - S07 · inverse_equivalence · mko_expectation_def, numeric_evaluation — 定義展開與精確計算。 - S06 · inverse_equivalence · mko_expectation_def, numeric_evaluation — 定義展開與精確計算，兩邊表示同一個數。 - S05.2 · inverse_equivalence · finite_sum_rules, def_unfold — 拆和與折回定義都是等式，雙向成立。 - S05.1 · inverse_equivalence · distributive, pointwise_rv, eq_replace — 逐項等值代換，雙向成立。 - S05 · inverse_equivalence · L_sum — 引理由兩個等式子步證成，串起來仍是等式。 - S04.3 · inverse_equivalence · def_unfold, G1, mul_one — 折回定義與代入已知值都是等值替換，雙向成立。 - S04.2 · inverse_equivalence · finite_sum_rules — 兩條有限和規則都是等式，可雙向使用。 - S04.1 · inverse_equivalence · distributive, mul_comm, eq_replace — 逐項等值代換，和式不變，雙向成立。 - S04 · inverse_equivalence · L_affine — 引理的每個子步都是等式，串起來仍是等式。 - S03.1 · inverse_equivalence · finite_sum_rules, mul_one, G1 — 每一個等號都是恆等式或代入已知值，雙向成立。 - S03 · inverse_equivalence · L_const — 這是數值相等，兩邊表示同一個數，雙向可替換。 - S02 · premise_audit · G2, numeric_evaluation — 精確有理數計算，可獨立重算。 - S01 · premise_audit · G1, mko_expectation_def, pointwise_rv — 只是定義；需要的前提是權重合法與 S 有限，使和式有意義。 ## 錯誤控制與反例 未給等可能就不能平均所有值MKO 的誤解之一是不看權重、直接平均所有值。X 的值 2、−2、0 的普通平均是 0，但權重是 1/2、1/4、1/4，E[X]=1/2（S12）。期望值是加權和，每個結果的值乘它自己的機率。 線性性不需要、也不推出獨立另一個誤解是由線性期望推論獨立或乘積公式。S10 顯示 X、Y 不獨立，但 E[X+Y]=E[X]+E[Y] 仍成立；S11 顯示 E[XY]=−1/2≠E[X]E[Y]=1/2。線性性只是有限和的拆分，與聯合分布無關。 常數項乘的是總權重 1E[aX+b] 的 b 來自 bΣw_s=b·1（S04.3）。漏掉 b 會得 −3/2，把 b 乘以結果個數 3 會得 −3/2+15=27/2，兩者都錯；正確值是 7/2。 - E[X]=(2+(−2)+0)/3=0 → reject — 權重不相等；E[X]=1/2·2+1/4·(−2)+1/4·0=1/2。 - E[X+Y]=E[X]+E[Y] 在此成立，所以 X、Y 獨立 → reject — 線性性對任何同模型變數都成立；P(X=2 且 Y=1)=1/2≠1/4=P(X=2)P(Y=1)，X、Y 不獨立。 - E[XY]=E[X]E[Y]=1/2 → reject — 直接計算 E[XY]=1/2·2+1/4·(−6)+1/4·0=−1/2。 - E[−3X+5]=−3E[X]=−3/2 → reject — 漏了常數項：E[−3X+5]=−3/2+5=7/2。 ## 結論與限制 在任何非空有限、權重非負且總和為 1 的模型上，E[c]=c、E[aX+b]=aE[X]+b、E[X+Y]=E[X]+E[Y]，證明只用有限和規則與同一樣本空間上的逐點運算，不需獨立性。實例中 E[X]=1/2、E[Y]=1、E[X+Y]=3/2、E[−3X+5]=7/2；X、Y 不獨立；E[XY]=−1/2≠1/2=E[X]E[Y]；X 值的普通平均 0 不是 E[X]。 - N12 至 N14 只對本例的權重向量 (1/2,1/4,1/4) 驗證恆等式（多項式格點核對）；一般情形的證明是 S03 至 S05。 - 本稿不處理無限樣本空間的期望、可積性或樣本平均的收斂。 ## 驗證及來源綁定 15 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: cbd356d320de275e46ebf0ed79aac7280e62a2b5e5520a5d0e1191b563a74da0 - original source SHA-256: ca19ba2c31a91326145232e902b561b1b278b0b43f616dd43820b730b9a8e002 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-expectation-01.json)