# 有限機率模型的變異數：平移、縮放與零變異數的刻畫 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-variance/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-variance-01 · production-20261019-adopted-96 ## 目標與範圍 在有限合法機率模型中證明 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 — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - 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。 ## 逐步主鏈 S01 · implies操作前 w=(\tfrac12,\tfrac14,\tfrac14,0) 操作後 w_s\ge0,\ \sum_s w_s=1,\ \mathrm{supp}=\{1,2,3\} 條件：無 規則：numeric_evaluation · 依賴：G2, support_def 葉節點依據：numeric_evaluation + support_def 先驗模型：四個權重都非負，總和 1/2+1/4+1/4+0=1，所以合法。正權重支持是 {1,2,3}；結果 4 屬於樣本空間 S，但權重為 0，不在支持中。MKO 假設 a2 要求把這兩者分開。 S02 · equivalent操作前 \mu=E[X] 操作後 \tfrac12\cdot1+\tfrac14\cdot3+\tfrac14\cdot(-1)+0\cdot10=1 條件：無 規則：mko_expectation_lin · 依賴：S01, G3, mko_expectation_lin 葉節點依據：mko_expectation_lin + numeric_evaluation 依期望值定義：1/2+3/4−1/4+0=1。結果 4 的值 10 乘上權重 0，貢獻為 0。 S03 · equivalent操作前 X(s)-\mu\ \ (s=1,2,3,4) 操作後 0,\ 2,\ -2,\ 9 條件：無 規則：numeric_evaluation · 依賴：S02, G3 葉節點依據：numeric_evaluation 逐點計算偏差：1−1=0、3−1=2、−1−1=−2、10−1=9。偏差對每個結果都有定義，包括零權重的結果 4。 S04 · equivalent操作前 \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 條件：無 規則：mko_variance_def · 依賴：S03, S01, mko_variance_def 葉節點依據：mko_variance_def + power_laws + numeric_evaluation 代入定義：0+1+1+0=2。零權重結果 4 的偏差 9 很大，但乘上權重 0 後貢獻為 0。 S05 · implies操作前 w_s\ge0,\ (X(s)-\mu)^2\ge0 操作後 \mathrm{Var}(X)\ge0 條件：無 規則：square_nonneg · 依賴：G1, mko_variance_def 葉節點依據：square_nonneg + order_basics + mul_zero + finite_sum_rules 一般性質。每一項 t_s=w_s(X(s)−μ)²：平方非負；若 w_s=0，t_s=0；若 w_s>0，把 0≤(X(s)−μ)² 兩邊乘以正數 w_s 保持順序，得 t_s≥0。非負數的有限和非負，所以 Var(X)≥0。 S06 · equivalent操作前 \mathrm{Var}(X+c) 操作後 \mathrm{Var}(X) 條件：無 規則：L_shift · 依賴：G1, mko_variance_def 葉節點依據：mko_expectation_lin + eq_replace 依引理 L_shift：平移不改變變異數。證明在 S06.1、S06.2：平均也平移 c，所以偏差不變。 S07 · equivalent操作前 \mathrm{Var}(kX) 操作後 k^2\,\mathrm{Var}(X) 條件：無 規則：L_scale · 依賴：G1, mko_variance_def 葉節點依據：mko_expectation_lin + power_laws + finite_sum_rules 依引理 L_scale：縮放 k 倍使變異數乘以 k²。證明在 S07.1 至 S07.3；對所有實數 k 成立，包括 k=0 與負 k。 S08 · implies操作前 \mathrm{Var}(X+5),\ X+5=(6,8,4,15) 操作後 \mathrm{Var}(X+5)=\mathrm{Var}(X)=2 條件：無 規則：L_shift · 依賴：S06, S04, G3 葉節點依據：mko_variance_def + numeric_evaluation 依 S06（c=5），Var(X+5)=2。直接核對：X+5 的值為 6、8、4、15，平均 1/2·6+1/4·8+1/4·4+0·15=6=μ+5，偏差 0、2、−2、9 與原來相同，變異數仍為 2。 S09 · implies操作前 \mathrm{Var}(-3X),\ -3X=(-3,-9,3,-30) 操作後 \mathrm{Var}(-3X)=(-3)^2\cdot2=18 條件：無 規則：L_scale · 依賴：S07, S04, G3 葉節點依據：mko_variance_def + numeric_evaluation 依 S07（k=−3），Var(−3X)=9·2=18。直接核對：−3X 的值為 −3、−9、3、−30，平均 −3=−3μ，偏差 0、−6、6、−27，變異數 1/4·36+1/4·36+0·729=18。負係數不使變異數變負。 S10 · implies操作前 t_s\ge0,\ \sum_s t_s=0 操作後 t_s=0\ \ \forall s 條件：無 規則：L_nonneg_sum_zero · 依賴：finite_sum_rules, order_basics 葉節點依據：order_basics + finite_sum_rules + contradiction 準備零變異數刻畫所需的引理 L_nonneg_sum_zero：非負數的有限和為零，則每一項都是零。證明在 S10.1、S10.2。 S11 · equivalent操作前 \mathrm{Var}(X)=0 操作後 X(s)=\mu\ \ \forall s\in\mathrm{supp} 條件：無 規則：L_var_zero · 依賴：G1, mko_variance_def, support_def 葉節點依據：L_nonneg_sum_zero + zero_product + square_nonneg + case_analysis 依引理 L_var_zero：變異數為零恰好表示 X 在每個正權重結果上等於平均。條件只涉及支持，零權重結果的值不受限制。證明在 S11.1（⇒）與 S11.2（⇐）。 S12 · equivalent操作前 \mathrm{Var}(X)=0 操作後 \exists c\ \forall s\in\mathrm{supp}:\ X(s)=c 條件：無 規則：L_const_support · 依賴：S11 葉節點依據：L_var_zero + exists_intro + finite_sum_rules 把 S11 改寫成 MKO 的說法：變異數為零恰好表示 X 在所有正權重結果上取同一個值。依引理 L_const_support，證明在 S12.1、S12.2。 S13 · implies操作前 Z=2\ \text{on}\ \mathrm{supp}=\{1,2,3\},\ Z(4)=7 操作後 \mathrm{Var}(Z)=0 條件：無 規則：L_const_support · 依賴：S12, S01, G3 葉節點依據：L_const_support + numeric_evaluation Z 在支持 {1,2,3} 上都等於 2，依 S12 得 Var(Z)=0，雖然 Z 在整個 S 上不是常數（Z(4)=7）。直接核對：μ_Z=2·(1/2+1/4+1/4)+7·0=2，Var(Z)=0+0+0+0·25=0。 S14 · implies操作前 X(1)=1\neq3=X(2),\ 1,2\in\mathrm{supp} 操作後 \mathrm{Var}(X)\neq0 條件：無 規則：contrapositive · 依賴：S12, S01, G3, S04 葉節點依據：contrapositive + L_const_support X 在支持中的兩個結果取不同值 1 與 3，所以沒有共同值；依 S12 的 ⇒ 方向取逆否，Var(X)≠0。這與 S04 的 Var(X)=2>0 一致。 S15 · implies操作前 \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} 條件：無 規則：and_intro_elim · 依賴：S04, S05, S06, S07, S08, S09, S12, S13 葉節點依據：and_intro_elim 整理：四個一般性質都已證明；實例中 μ=1、Var(X)=2、Var(X+5)=2、Var(−3X)=18，Var(Z)=0 而 Z 只在零權重結果上不同。 ## 局部子步與引理 S06.1 · equivalent操作前 E[X+c] 操作後 \mu+c 條件：無 規則：mko_expectation_lin · 依賴：G1, mko_expectation_lin 葉節點依據：mko_expectation_lin 依期望值線性性（a=1、b=c）：E[X+c]=E[X]+c=μ+c。這需要權重總和為 1。 S06.2 · equivalent操作前 \sum_s w_s\bigl((X(s)+c)-(\mu+c)\bigr)^2 操作後 \sum_s w_s(X(s)-\mu)^2 條件：無 規則：eq_replace · 依賴：S06.1, eq_replace 葉節點依據：eq_replace + add_assoc + add_comm + add_inverse + add_zero 對每個 s：(X(s)+c)−(μ+c)=X(s)−μ（加法結合、交換與反元素）。每一項都換成相等的項，和不變。S06.1 與 S06.2 合起來證得引理 L_shift。 S07.1 · equivalent操作前 E[kX] 操作後 k\mu 條件：無 規則：mko_expectation_lin · 依賴：G1, mko_expectation_lin 葉節點依據：mko_expectation_lin 依期望值線性性（a=k、b=0）：E[kX]=kμ。 S07.2 · equivalent操作前 (kX(s)-k\mu)^2 操作後 k^2(X(s)-\mu)^2 條件：無 規則：power_laws · 依賴：S07.1, distributive, power_laws 葉節點依據：distributive + power_laws + mul_comm 先用分配律提出 k：kX(s)−kμ=k(X(s)−μ)；再用 (ab)²=a²b²。偏差乘 k，平方後帶出 k²，負號在平方中消失。 S07.3 · equivalent操作前 \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) 條件：無 規則：finite_sum_rules · 依賴：S07.2, finite_sum_rules 葉節點依據：finite_sum_rules + def_unfold 常數 k² 可從有限和中提出，剩下的和依定義是 Var(X)。S07.1 至 S07.3 合起來證得引理 L_scale。k=0 時得 Var(0)=0，與常數變數的變異數一致。 S10.1 · implies操作前 t_r>0\ \text{for some}\ r 操作後 \sum_s t_s=t_r+\sum_{s\neq r}t_s\ge t_r>0 條件：t_s\ge0 規則：order_basics · 依賴：finite_sum_rules, order_basics 葉節點依據：finite_sum_rules + order_basics 暫時假設某一項 t_r>0。把和拆成 t_r 加上其餘各項；其餘各項非負，其和也非負，所以總和 ≥t_r>0。 S10.2 · implies操作前 \sum_s t_s>0\ \text{and}\ \sum_s t_s=0 操作後 \neg\exists r:\ t_r>0,\ \text{so}\ t_s=0 條件：無 規則：contradiction · 依賴：S10.1, contradiction 葉節點依據：contradiction + order_basics S10.1 的結論與假設 Σ t_s=0 矛盾，所以沒有任何 t_r>0。每個 t_s 既 ≥0 又不 >0，依三分律 t_s=0。S10.1 與 S10.2 合起來證得引理 L_nonneg_sum_zero。 S11.1 · implies操作前 \mathrm{Var}(X)=0,\ s\in\mathrm{supp} 操作後 X(s)=\mu 條件：w_s>0 規則：L_nonneg_sum_zero · 依賴：S05, S10, zero_product, square_nonneg 葉節點依據：L_nonneg_sum_zero + zero_product + square_nonneg （⇒）S05 中已知每項 t_s=w_s(X(s)−μ)²≥0，而它們的和 Var(X)=0，依 L_nonneg_sum_zero 每項 t_s=0。對 s∈supp，w_s>0 故 w_s≠0，由零積性質得 (X(s)−μ)²=0，再由平方為零 ⇔ 底數為零得 X(s)=μ。 S11.2 · implies操作前 X(s)=\mu\ \ \forall s\in\mathrm{supp} 操作後 \mathrm{Var}(X)=\sum_s 0=0 條件：無 規則：case_analysis · 依賴：G1, support_def, case_analysis 葉節點依據：case_analysis + support_def + mul_zero + finite_sum_rules （⇐）每個 s 不是在支持內就是在支持外。在支持內：X(s)−μ=0，t_s=w_s·0=0。在支持外：w_s=0，t_s=0·(X(s)−μ)²=0。所有項都是 0，和為 0。S11.1 與 S11.2 合起來證得引理 L_var_zero。 S12.1 · implies操作前 \mathrm{Var}(X)=0 操作後 X(s)=\mu\ \ \forall s\in\mathrm{supp}\ \Rightarrow\ c=\mu 條件：無 規則：L_var_zero · 依賴：S11, exists_intro 葉節點依據：L_var_zero + exists_intro （⇒）由 L_var_zero 的 ⇒ 方向，X 在支持上處處等於 μ，取 c=μ 即得共同值。 S12.2 · implies操作前 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 條件：無 規則：L_var_zero · 依賴：S11, G1, support_def 葉節點依據：L_var_zero + finite_sum_rules + support_def + mul_zero （⇐）把 μ 的和式分成支持內外兩部分：支持外的權重都是 0，貢獻 0，也使支持內權重之和為 1；所以 μ=c·1=c。於是 X(s)=c=μ 對每個 s∈supp 成立，由 L_var_zero 的 ⇐ 方向得 Var(X)=0。S12.1 與 S12.2 合起來證得引理 L_const_support。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-variance-01.json)