有限機率模型的變異數：平移、縮放與零變異數的刻畫

目標與範圍

在有限合法機率模型中證明 Var(X)≥0、Var(X+c)=Var(X)、Var(kX)=k²Var(X)，以及 Var(X)=0 ⇔ X 在所有正權重結果上取同一個值。再以 S={1,2,3,4}、w₁=1/2、w₂=1/4、w₃=1/4、w₄=0、X=(1,3,−1,10) 計算 μ=1、Var(X)=2、Var(X+5)=2、Var(−3X)=18，並以 Z=(2,2,2,7) 說明零權重結果上的不同值不影響零變異數。

限定 MKO：有限非空樣本空間、非負歸一化權重、實值總函數，使用機率分布變異數而非樣本估計，並區分正權重支持與全樣本空間（a1、a2）。全部以精確有理數計算。期望值的線性性引自 mko-expectation。不處理 Var(X+Y)、協方差、標準差或 E[X²]−μ² 公式；不改動 canonical MKO 或英文 edition。

已知條件與符號

• finite_sum_rules
• square_nonneg
• order_basics
• distributive
• power_laws
• numeric_evaluation

• G1 — 一般模型：S 有限非空，對所有 s 有 w_s≥0 且 Σ_{s∈S} w_s=1；X:S→ℝ 為總函數；μ=E[X]=Σ w_s X(s)；c、k 為實數。
• G2 — 實例：S={1,2,3,4}，w₁=1/2、w₂=1/4、w₃=1/4、w₄=0。
• G3 — X(1)=1、X(2)=3、X(3)=−1、X(4)=10；Z(1)=Z(2)=Z(3)=2、Z(4)=7。

• \mu=E[X] — X 的期望值
• \mathrm{Var}(X)=\sum_s w_s(X(s)-\mu)^2 — X 的變異數
• \mathrm{supp}=\{s\in S\mid w_s>0\} — 正權重支持
• c,k — 平移量與縮放係數（實數）
• t_s — 變異數和式中的第 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。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=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。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_variance_def · cited — 令 μ=E[X]，對有限合法機率模型定義 V(X)=Var(X)=Σ_s w_s(X(s)−μ)²≥0。平移不改變變異數，Var(kX)=k²Var(X)；Var(X)=0 當且僅當 X 在所有正權重的基本結果上取同一個值。 · mko-variance
• mko_expectation_lin · 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
• support_def · prerequisite — 正權重支持：supp={s∈S ∣ w_s>0}。因 w_s≥0，s∉supp 恰表示 w_s=0。
• L_shift · lemma — 在 G1 的模型中，對任意實數 c：Var(X+c)=Var(X)。
• L_scale · lemma — 在 G1 的模型中，對任意實數 k：Var(kX)=k²Var(X)。
• L_nonneg_sum_zero · lemma — 若有限多個實數 t_s 都 ≥0 且 Σ_s t_s=0，則每個 t_s=0。
• L_var_zero · lemma — 在 G1 的模型中：Var(X)=0 ⇔ 對每個 s∈supp 有 X(s)=μ。
• L_const_support · lemma — 在 G1 的模型中：Var(X)=0 ⇔ 存在實數 c 使得對每個 s∈supp 有 X(s)=c。

逐步主鏈

w=(\tfrac12,\tfrac14,\tfrac14,0)

w_s\ge0,\ \sum_s w_s=1,\ \mathrm{supp}=\{1,2,3\}

\mu=E[X]

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

X(s)-\mu\ \ (s=1,2,3,4)

0,\ 2,\ -2,\ 9

\mathrm{Var}(X)=\sum_s w_s(X(s)-\mu)^2

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

w_s\ge0,\ (X(s)-\mu)^2\ge0

\mathrm{Var}(X)\ge0

\mathrm{Var}(X+c)

\mathrm{Var}(X)

\mathrm{Var}(kX)

k^2\,\mathrm{Var}(X)

\mathrm{Var}(X+5),\ X+5=(6,8,4,15)

\mathrm{Var}(X+5)=\mathrm{Var}(X)=2

\mathrm{Var}(-3X),\ -3X=(-3,-9,3,-30)

\mathrm{Var}(-3X)=(-3)^2\cdot2=18

t_s\ge0,\ \sum_s t_s=0

t_s=0\ \ \forall s

\mathrm{Var}(X)=0

X(s)=\mu\ \ \forall s\in\mathrm{supp}

\mathrm{Var}(X)=0

\exists c\ \forall s\in\mathrm{supp}:\ X(s)=c

Z=2\ \text{on}\ \mathrm{supp}=\{1,2,3\},\ Z(4)=7

\mathrm{Var}(Z)=0

X(1)=1\neq3=X(2),\ 1,2\in\mathrm{supp}

\mathrm{Var}(X)\neq0

\text{S04 to S14}

\mathrm{Var}\ge0,\ \mathrm{Var}(X+c)=\mathrm{Var}(X),\ \mathrm{Var}(kX)=k^2\mathrm{Var}(X),\ \mathrm{Var}=0\iff\text{const on supp}

局部子步與引理

E[X+c]

\mu+c

\sum_s w_s\bigl((X(s)+c)-(\mu+c)\bigr)^2

\sum_s w_s(X(s)-\mu)^2

E[kX]

k\mu

(kX(s)-k\mu)^2

k^2(X(s)-\mu)^2

\sum_s w_s\,k^2(X(s)-\mu)^2

k^2\sum_s w_s(X(s)-\mu)^2=k^2\,\mathrm{Var}(X)

t_r>0\ \text{for some}\ r

\sum_s t_s=t_r+\sum_{s\neq r}t_s\ge t_r>0

\sum_s t_s>0\ \text{and}\ \sum_s t_s=0

\neg\exists r:\ t_r>0,\ \text{so}\ t_s=0

\mathrm{Var}(X)=0,\ s\in\mathrm{supp}

X(s)=\mu

X(s)=\mu\ \ \forall s\in\mathrm{supp}

\mathrm{Var}(X)=\sum_s 0=0

\mathrm{Var}(X)=0

X(s)=\mu\ \ \forall s\in\mathrm{supp}\ \Rightarrow\ c=\mu

X(s)=c\ \ \forall s\in\mathrm{supp}

\mu=\sum_{s\in\mathrm{supp}}w_s c+\sum_{s\notin\mathrm{supp}}0\cdot X(s)=c,\ \text{so}\ \mathrm{Var}(X)=0

逐步反向審查

• S15 · sufficient_goal_reduction · S04, S05, S06, S07, S08, S09, S12, S13, and_intro_elim — 目標 G 為 goal 的證明與計算；足夠條件 H 為各步結論的合取，皆已正向證成，H⇒G 只用合取引入。
• S14 · premise_audit · S12, contrapositive — 兩個支持內的不同值就足以否定共同值；結論只說不為零，數值由 S04 給出。
• S13 · premise_audit · S12, S01 — 只用到 S12 的 ⇐ 方向與支持的判定；直接計算是交叉核對。
• S12.2 · premise_audit · L_var_zero, finite_sum_rules, support_def, mul_zero — 關鍵是 μ 只由支持上的值決定；支持外的值（例如 Z(4)=7）乘以 0 而消失。
• S12.1 · premise_audit · L_var_zero, exists_intro — 存在引入只需見證 c=μ。
• S12 · inverse_equivalence · L_const_support — 兩個方向都在子步中證明。
• S11.2 · premise_audit · case_analysis, support_def, mul_zero — 兩個情形窮盡 S（support_def 保證支持外即 w_s=0）。
• S11.1 · premise_audit · S05, L_nonneg_sum_zero, zero_product, square_nonneg — 對 w_s=0 的結果，t_s=0 不提供任何關於 X(s) 的資訊，所以結論只對支持成立。
• S11 · inverse_equivalence · L_var_zero — 兩個方向分別在子步中證明，所以是等價。
• S10.2 · premise_audit · contradiction, order_basics — 矛盾法釋放 S10.1 的暫時假設；三分律把「≥0 且不 >0」化為「=0」。
• S10.1 · premise_audit · finite_sum_rules, order_basics — 只用到其餘項非負與加法保序；這是暫時假設下的推論，在 S10.2 釋放。
• S10 · premise_audit · L_nonneg_sum_zero — 需要每項非負；若允許負項，例如 1+(−1)=0，結論不成立。
• S09 · premise_audit · S07, S04 — 結論由引理得出；直接計算只是交叉核對。
• S08 · premise_audit · S06, S04 — 結論由引理得出；直接計算只是交叉核對。
• S07.3 · inverse_equivalence · finite_sum_rules, def_unfold — 提出常數與折回定義都是等式，雙向成立。
• S07.2 · inverse_equivalence · distributive, power_laws — 兩條都是對所有實數成立的恆等式，雙向成立。
• S07.1 · inverse_equivalence · mko_expectation_lin — 線性性是等式，可雙向使用。
• S07 · inverse_equivalence · L_scale — 兩邊是同一個數（引理），可雙向替換。
• S06.2 · inverse_equivalence · eq_replace, add_inverse, add_comm — 逐項等值替換，雙向成立。
• S06.1 · inverse_equivalence · mko_expectation_lin — 線性性是等式，可雙向使用。
• S06 · inverse_equivalence · L_shift — 兩邊是同一個數（引理），可雙向替換。
• S05 · premise_audit · square_nonneg, order_basics, finite_sum_rules — 需要權重非負；若允許負權重，結論可能失敗。這是單向推論，不宣稱 Var(X)>0。
• S04 · inverse_equivalence · mko_variance_def, numeric_evaluation — 定義展開與精確計算，兩邊同值。
• S03 · inverse_equivalence · numeric_evaluation — 整數減法，可逆向核對（偏差加 μ 回到原值）。
• S02 · inverse_equivalence · mko_expectation_lin, numeric_evaluation — 定義展開加精確計算，兩邊同值。
• S01 · premise_audit · G2, support_def, numeric_evaluation — 精確計算與定義判讀，可獨立重算。

錯誤控制與反例

零變異數只要求正權重結果同值

MKO 的誤解之一是要求零變異數的變數在零機率結果上也同值。Z 在 S 上不是常數（Z(4)=7），但 w₄=0，Var(Z)=0（S13）。零變異數的正確刻畫是在支持上常值（S12）。

機率分布變異數不是樣本變異數

另一個誤解是混用樣本變異數。若把 1、3、−1、10 當成四筆資料、用 n−1=3 為分母，得 275/12，而不是本模型的 Var(X)=2。本稿的變異數以權重加權，不用 n−1 分母；標準差 √2 是另一個量，本稿未處理。

縮放因子要平方，平移不加到變異數上

Var(−3X)=(−3)²·2=18，不是 −3·2=−6，也不是 3·2=6；Var(X+5)=2，不是 2+5=7。原因分別是 S07.2 的平方與 S06.2 的偏差不變。

• Z(4)=7≠2，所以 Var(Z)>0 → reject — w₄=0，結果 4 的項為 0·25=0；Z 在支持上恆為 2，Var(Z)=0。
• Var(−3X)=−3Var(X)=−6 → reject — 變異數非負；正確為 (−3)²·2=18。
• Var(X+5)=Var(X)+5=7 → reject — 平移使平均也加 5，偏差不變，Var(X+5)=2。
• X 的變異數是 1、3、−1、10 的樣本變異數 275/12 → reject — 本模型的變異數以權重 (1/2,1/4,1/4,0) 加權，等於 2；樣本估計是另一回事。

結論與限制

在任何有限合法模型中 Var(X)≥0、Var(X+c)=Var(X)、Var(kX)=k²Var(X)，且 Var(X)=0 恰在 X 於正權重支持上取同一值時成立。實例：μ=1、Var(X)=2、Var(X+5)=2、Var(−3X)=18；Z=(2,2,2,7) 在支持 {1,2,3} 上恆為 2，所以 Var(Z)=0，Z(4)=7 不影響結果。

• Var(X+Y)、協方差與標準差不在本稿範圍；本稿也不使用 E[X²]−μ² 公式。
• 期望值線性性引自 mko-expectation，其證明見該 MKO 的教學稿，本稿不重證。

驗證及來源綁定

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

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

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