有限模型的期望值：線性性的證明與相依變數的實例

目標與範圍

在非空有限樣本空間 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]。

逐步主鏈

Z:S\to\mathbb{R}

E[Z]=\sum_{s\in S}w_sZ(s)

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

w_s\ge0,\ \sum_s w_s=1

E[c]

c

E[aX+b]

aE[X]+b

E[X+Y]

E[X]+E[Y]

E[X]

\tfrac12\cdot2+\tfrac14\cdot(-2)+\tfrac14\cdot0=\tfrac12

E[Y]

\tfrac12\cdot1+\tfrac14\cdot3+\tfrac14\cdot(-1)=1

E[X+Y],\ X+Y=(3,1,-1)

E[X+Y]=\tfrac32=E[X]+E[Y]

E[-3X+5],\ -3X+5=(-1,11,5)

E[-3X+5]=-3\cdot\tfrac12+5=\tfrac72

P(X=2,\,Y=1)=w_1=\tfrac12,\ P(X=2)P(Y=1)=\tfrac14

X,Y\ \text{not independent}

XY=(2,-6,0)

E[XY]=-\tfrac12\neq\tfrac12=E[X]E[Y]

\tfrac{2+(-2)+0}{3}=0

0\neq\tfrac12=E[X]

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

局部子步與引理

\sum_{s\in S}w_s\,c

c\sum_{s\in S}w_s=c\cdot 1=c

\sum_{s}w_s\,(aX(s)+b)

\sum_{s}\bigl(a\,w_sX(s)+b\,w_s\bigr)

\sum_{s}\bigl(a\,w_sX(s)+b\,w_s\bigr)

a\sum_{s}w_sX(s)+b\sum_{s}w_s

a\sum_{s}w_sX(s)+b\sum_{s}w_s

aE[X]+b\cdot1=aE[X]+b

\sum_{s}w_s\,(X(s)+Y(s))

\sum_{s}\bigl(w_sX(s)+w_sY(s)\bigr)

\sum_{s}\bigl(w_sX(s)+w_sY(s)\bigr)

\sum_{s}w_sX(s)+\sum_{s}w_sY(s)=E[X]+E[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。線性性只是有限和的拆分，與聯合分布無關。

常數項乘的是總權重 1

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