# 協方差：對稱性、仿射規則與「零協方差不蘊含獨立」

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-covariance/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-covariance-01 · production-20261019-adopted-96



## 目標與範圍

在同一個精確有限 joint law 上：(1) 證明 Cov(Y,X)=Cov(X,Y)；(2) 證明 Cov(aX+b,cY+d)=ac·Cov(X,Y)；(3) 證明 X、Y 獨立時 Cov(X,Y)=0，因此非零協方差可否證獨立；(4) 對 X 均勻取 −1、0、1 且 Y=X² 的 joint law，算出 E[X]、E[Y]、E[XY] 與 Cov(X,Y)=0，並證明 X、Y 不獨立。

只在 MKO 的範圍內：所有期望都由同一個精確有限 joint law 計算（假設 a1）；非零協方差可否證獨立，零協方差一般不能證獨立（假設 a2）。不處理相關係數、條件期望或無限樣本空間；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- distributive
- finite_sum_rules
- mul_comm
- numeric_evaluation
- marginal_def
- finite_sum_regroup


- G1 — (S,p) 是有限 joint law：S 為互異整數對，p(s)≥0 為精確有理數且 Σ_{s∈S} p(s)=1。X、Y 是座標：在 s=(x,y) 上 X=x、Y=y。所有期望都是 E[g]=Σ_{s∈S} p(s)g(s)，用同一個 (S,p)。
- G2 — a、b、c、d 是實數常數。
- G3 — 例子：S={(−1,1),(0,0),(1,1)}，每個值對質量 1/3。


- (S,p) — 有限 joint law：互異整數值對與精確質量
- E[g] — 在同一 joint law 上的期望 Σ_{s∈S} p(s)g(s)
- \operatorname{Cov}(X,Y) — 協方差 E[XY]−E[X]E[Y]
- a,\ b,\ c,\ d — 仿射變換的實數係數
- S_X,\ S_Y — S 中出現的第一座標與第二座標的集合
- p_X,\ p_Y — X 與 Y 的邊際質量





## 規則與來源


- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- 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。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- 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）。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- add_zero · prerequisite — 加法單位元：u+0=u。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_cov_def · cited — 給同一有限joint law上的X,Y，Cov(X,Y)=E[XY]-E[X]E[Y]。協方差對兩變數對稱，仿射變換滿足Cov(aX+b,cY+d)=ac Cov(X,Y)。 · mko-covariance
- mko_expectation_def · cited — 對非空有限 S、歸一化非負權重 w_s 與實值隨機變數 X，定義 E[X]=Σ_(s∈S)w_s X(s)。 · mko-expectation
- mko_joint_def · cited — 二維有限聯合分布列出互異值對(x,y)及非負精確質量，總和恰為1。邊際、矩形事件及單點質量都從同一joint law聚合。 · mko-finite-joint-distribution
- mko_indep_def · cited — 有限值隨機變數X,Y獨立，若對每個值對(x,y)皆有P(X=x,Y=y)=P(X=x)P(Y=y)。 · mko-random-variable-independence
- marginal_def · prerequisite — 邊際：p_X(x)=P(X=x)=Σ_{y:(x,y)∈S} p(x,y)，p_Y(y)=P(Y=y)=Σ_{x:(x,y)∈S} p(x,y)；P(X=x,Y=y) 在 (x,y)∈S 時是 p(x,y)，否則是 0。
- finite_sum_regroup · prerequisite — 有限和重組：若有限集合分割成兩兩不交的子集（每個元素恰屬其中一個），則全體的和等於各子集上的和再相加；加入值為 0 的項不改變有限和。
- L_lin_exp · lemma — 在同一有限 joint law 上，對 (X,Y) 的實值函數 U_1 到 U_m 與實數 c_1 到 c_m：E[Σ_{k=1}^{m} c_k U_k]=Σ_{k=1}^{m} c_k E[U_k]；常數 c 的期望為 c。
- L_indep_prod · lemma — 若 X、Y 在有限 joint law 上獨立，則 E[XY]=E[X]E[Y]。





## 逐步主鏈

S01 · definition操作前

X,\ Y\ \text{on one law}\ (S,p)

操作後

\operatorname{Cov}(X,Y)=E[XY]-E[X]E[Y],\quad E[g]=\sum_{s\in S}p(s)\,g(s)

條件：\text{all expectations use the same }(S,p)

規則：mko_cov_def · 依賴：G1, mko_expectation_def

葉節點依據：mko_cov_def + mko_expectation_def + def_unfold

依 MKO 定義協方差：先算 E[X]、E[Y]、E[XY]，再相減。三個期望都用 G1 的同一個 joint law，樣本空間是 S、權重是 p（p 非負且總和恰為 1，正是期望定義要求的歸一化權重）。



S02 · equivalent操作前

\operatorname{Cov}(Y,X)=E[YX]-E[Y]E[X]

操作後

\operatorname{Cov}(Y,X)=E[XY]-E[X]E[Y]=\operatorname{Cov}(X,Y)

條件：無

規則：mul_comm · 依賴：S01

葉節點依據：mul_comm + eq_replace + def_unfold

在每個 s∈S 上 Y(s)X(s)=X(s)Y(s)（實數乘法交換），所以 YX 與 XY 是同一個函數，期望相同；E[Y]E[X]=E[X]E[Y] 也是乘法交換。因此交換兩個變數不改變協方差。



S03 · theorem_application操作前

E\Big[\sum_{k=1}^{m}c_kU_k\Big]

操作後

\sum_{k=1}^{m}c_k\,E[U_k],\quad E[c]=c

條件：U_k\ \text{functions of}\ (X,Y)\ \text{on the same}\ (S,p)

規則：L_lin_exp · 依賴：S01, G1

葉節點依據：L_lin_exp

協方差的計算需要期望的線性。引理 L_lin_exp 在 S03.1、S03.2 證明；它只需要所有 U_k 都定義在同一個 (S,p) 上，不需要任何獨立性。



S04 · theorem_application操作前

E[aX+b],\ E[cY+d]

操作後

E[aX+b]=a\,E[X]+b,\quad E[cY+d]=c\,E[Y]+d

條件：無

規則：L_lin_exp · 依賴：S03, G2

葉節點依據：L_lin_exp

取 m=2、U_1=X、U_2=1（常數函數）、c_1=a、c_2=b：E[aX+b]=aE[X]+bE[1]=aE[X]+b。對 Y 以 c、d 同理。



S05 · equivalent操作前

(aX+b)(cY+d)

操作後

ac\,XY+ad\,X+bc\,Y+bd

條件：無

規則：distributive · 依賴：G2, distributive

葉節點依據：distributive + mul_comm + mul_assoc

在每個 s∈S 上逐點展開乘積：(aX(s)+b)(cY(s)+d)=acX(s)Y(s)+adX(s)+bcY(s)+bd。這是實數的分配律與交換律，對所有 s 成立，所以兩個函數相等（N1 是四次多線性恆等式的格點核對）。



S06 · theorem_application操作前

E[(aX+b)(cY+d)]

操作後

ac\,E[XY]+ad\,E[X]+bc\,E[Y]+bd

條件：無

規則：L_lin_exp · 依賴：S03, S05

葉節點依據：L_lin_exp + eq_replace

把 S05 的展開代入期望，再用引理（m=4，U 依序為 XY、X、Y、1，係數 ac、ad、bc、bd）。這裡 E[XY] 必須用同一 joint law 計算，不能用兩個邊際相乘代替。



S07 · equivalent操作前

E[aX+b]\,E[cY+d]=(a\,E[X]+b)(c\,E[Y]+d)

操作後

ac\,E[X]E[Y]+ad\,E[X]+bc\,E[Y]+bd

條件：無

規則：distributive · 依賴：S04

葉節點依據：distributive + mul_comm + mul_assoc

對兩個實數 aE[X]+b 與 cE[Y]+d 的乘積用分配律展開，結構與 S05 相同。



S08 · equivalent操作前

\operatorname{Cov}(aX+b,cY+d)=E[(aX+b)(cY+d)]-E[aX+b]\,E[cY+d]

操作後

\operatorname{Cov}(aX+b,cY+d)=ac\,(E[XY]-E[X]E[Y])=ac\operatorname{Cov}(X,Y)

條件：無

規則：eq_replace · 依賴：S01, S06, S07

葉節點依據：eq_replace + add_inverse + distributive + add_comm

把 S06 與 S07 代入定義後相減：adE[X]、bcE[Y]、bd 三項互相抵消，剩下 acE[XY]−acE[X]E[Y]=ac(E[XY]−E[X]E[Y])=ac·Cov(X,Y)。常數 b、d 消失，係數 a、c 相乘（含正負號）。N2 是這個代數恆等式的核對。



S09 · implies操作前

S=\{(-1,1),(0,0),(1,1)\},\ p\equiv\tfrac13

操作後

\text{a finite joint law with}\ Y=X^2\ \text{on}\ S

條件：無

規則：mko_joint_def · 依賴：G3, mko_joint_def

葉節點依據：mko_joint_def + cartesian_product_def + numeric_evaluation

三個值對的第一座標 −1、0、1 互異，所以值對互異；質量 1/3>0；總和 3·(1/3)=1。故它是有限 joint law。每個值對的第二座標等於第一座標的平方：(−1)²=1、0²=0、1²=1，所以在這個 law 上 Y=X²。



S10 · equivalent操作前

E[X]=\tfrac13(-1)+\tfrac13(0)+\tfrac13(1)

操作後

E[X]=0

條件：無

規則：numeric_evaluation · 依賴：S01, S09

葉節點依據：numeric_evaluation + frac_rules

依定義 E[X]=Σ p(s)X(s)，三個值對的 X 值是 −1、0、1，各乘 1/3 相加得 0。



S11 · equivalent操作前

E[Y]=\tfrac13(1)+\tfrac13(0)+\tfrac13(1)

操作後

E[Y]=\tfrac23

條件：無

規則：numeric_evaluation · 依賴：S01, S09

葉節點依據：numeric_evaluation + frac_rules

三個值對的 Y 值是 1、0、1，加權和為 2/3。



S12 · equivalent操作前

E[XY]=\tfrac13(-1)(1)+\tfrac13(0)(0)+\tfrac13(1)(1)

操作後

E[XY]=0

條件：無

規則：numeric_evaluation · 依賴：S01, S09

葉節點依據：numeric_evaluation + frac_rules

XY 在三個值對上的值是 −1、0、1（就是 X³），加權和為 0。E[XY] 是在同一個 joint law 上逐值對計算的，不是 E[X]E[Y]。



S13 · equivalent操作前

\operatorname{Cov}(X,Y)=E[XY]-E[X]E[Y]

操作後

\operatorname{Cov}(X,Y)=0-0\cdot\tfrac23=0

條件：無

規則：eq_replace · 依賴：S01, S10, S11, S12

葉節點依據：eq_replace + numeric_evaluation

代入 S10 到 S12 的三個值：0−0·(2/3)=0。這個例子的協方差為零。



S14 · implies操作前

X,\ Y\ \text{independent on}\ (S,p)

操作後

E[XY]=E[X]E[Y],\ \operatorname{Cov}(X,Y)=0

條件：P(X=x,Y=y)=p_X(x)p_Y(y)\ \text{for all}\ (x,y)\in S_X\times S_Y

規則：L_indep_prod · 依賴：S01, G1

葉節點依據：L_indep_prod + eq_replace + add_inverse

引理 L_indep_prod（S14.1 到 S14.3 證明）給出 E[XY]=E[X]E[Y]，代入 S01 得 Cov(X,Y)=0。這是 MKO 假設 a2 前半句的依據。



S15 · equivalent操作前

X,Y\ \text{independent}\Rightarrow\operatorname{Cov}(X,Y)=0

操作後

\operatorname{Cov}(X,Y)\neq 0\Rightarrow X,Y\ \text{not independent}

條件：無

規則：contrapositive · 依賴：S14

葉節點依據：contrapositive

取 S14 的逆否命題：只要算出非零協方差，就能否證獨立。這是 MKO 假設 a2 的前半句。



S16 · implies操作前

P(X=0,Y=1)\ \text{vs}\ P(X=0)\,P(Y=1)

操作後

0\neq\tfrac13\cdot\tfrac23=\tfrac29

條件：無

規則：mko_indep_def · 依賴：S09, marginal_def, mko_indep_def

葉節點依據：mko_indep_def + marginal_def + numeric_evaluation

(0,1)∉S，所以 P(X=0,Y=1)=0。P(X=0)=p(0,0)=1/3；P(Y=1)=p(−1,1)+p(1,1)=2/3；乘積 2/9≠0。獨立的定義要求每個值對都相等，這個值對不相等，所以 X、Y 不獨立。



S17 · implies操作前

\operatorname{Cov}(X,Y)=0\ \text{and}\ X,Y\ \text{dependent}

操作後

\operatorname{Cov}(X,Y)=0\not\Rightarrow X,Y\ \text{independent}

條件：無

規則：exists_intro · 依賴：S13, S16, S14

葉節點依據：exists_intro + quantifier_negation

同一個 joint law 上 Cov(X,Y)=0（S13）而 X、Y 不獨立（S16）。所以「每個有限 joint law 上，協方差為零就獨立」這個全稱命題為假；S14 的逆命題不成立。這是 MKO 假設 a2 的後半句。







## 局部子步與引理

S03.1 · equivalent操作前

\sum_{s\in S}p(s)\sum_{k=1}^{m}c_kU_k(s)

操作後

\sum_{k=1}^{m}c_k\sum_{s\in S}p(s)\,U_k(s)=\sum_{k=1}^{m}c_k\,E[U_k]

條件：S\ \text{finite}

規則：finite_sum_rules · 依賴：G1, distributive, finite_sum_rules

葉節點依據：distributive + finite_sum_rules + mul_comm + mul_assoc

把 p(s) 分配進內層和，得到兩個有限和的雙重和；有限和可交換求和次序（反覆使用 Σ(a_i+b_i)=Σa_i+Σb_i），再把常數 c_k 提出（Σ c·a_i=c·Σa_i）。每個 Σ_s p(s)U_k(s) 依定義就是 E[U_k]。全部是有限和，沒有收斂問題。



S03.2 · equivalent操作前

E[c]=\sum_{s\in S}p(s)\,c

操作後

E[c]=c\sum_{s\in S}p(s)=c

條件：\sum_{s\in S}p(s)=1

規則：finite_sum_rules · 依賴：G1, finite_sum_rules

葉節點依據：finite_sum_rules + mul_one + mul_comm

常數函數 c 的期望：提出 c 後剩下 Σ_s p(s)，由 G1 恰為 1，所以 E[c]=c。若質量只近似和為 1，這一步就不成立。S03.1 與 S03.2 合起來證得引理 L_lin_exp。



S14.1 · equivalent操作前

E[XY]=\sum_{(x,y)\in S}xy\,p(x,y)

操作後

E[XY]=\sum_{x\in S_X}\sum_{y\in S_Y}xy\,P(X=x,Y=y)

條件：S\subseteq S_X\times S_Y

規則：finite_sum_regroup · 依賴：G1, marginal_def, finite_sum_regroup

葉節點依據：finite_sum_regroup + mul_zero + add_zero

S_X、S_Y 是 S 中出現的第一、第二座標，所以 S⊆S_X×S_Y。在 S 上 P(X=x,Y=y)=p(x,y)，在 S_X×S_Y 中不屬於 S 的格點上 P(X=x,Y=y)=0，這些項是 0。加入值為 0 的項並依第一座標重組，有限和不變。



S14.2 · implies操作前

\sum_{x\in S_X}\sum_{y\in S_Y}xy\,P(X=x,Y=y)

操作後

\sum_{x\in S_X}\sum_{y\in S_Y}x\,p_X(x)\,y\,p_Y(y)

條件：X,\ Y\ \text{independent}

規則：mko_indep_def · 依賴：S14.1, mko_indep_def

葉節點依據：mko_indep_def + eq_replace + mul_comm

在獨立的假設下，對每一個格點 (x,y)（包括不在 S 中的格點）都有 P(X=x,Y=y)=p_X(x)p_Y(y)，逐項代入，再用乘法交換重排各因子。



S14.3 · equivalent操作前

\sum_{x\in S_X}\sum_{y\in S_Y}x\,p_X(x)\,y\,p_Y(y)

操作後

\Big(\sum_{x}x\,p_X(x)\Big)\Big(\sum_{y}y\,p_Y(y)\Big)=E[X]\,E[Y]

條件：無

規則：distributive · 依賴：S14.2, distributive, finite_sum_rules, finite_sum_regroup

葉節點依據：distributive + finite_sum_rules + finite_sum_regroup + mul_comm

內層對 y 求和時 x p_X(x) 是常數，提出後得 x p_X(x)·Σ_y y p_Y(y)；外層再把常數 Σ_y y p_Y(y) 提出，得到兩個和的乘積。最後 Σ_x x p_X(x)=Σ_x Σ_y x p(x,y)=Σ_{s∈S} X(s)p(s)=E[X]（依第一座標重組），E[Y] 同理。S14.1 到 S14.3 合起來證得引理 L_indep_prod。







## 逐步反向審查


- S17 · sufficient_goal_reduction · S13, S16, exists_intro — 目標 G：零協方差一般不能證獨立。足夠條件 H：存在一個協方差為零但不獨立的有限 joint law；H⇒G 因為一個反例就否定全稱命題。H 由 S09 到 S16 正向證成。
- S16 · premise_audit · S09, marginal_def, mko_indep_def — 否證只需一個值對不相等；需要支撐列表完整，才能確定 (0,1) 的質量是 0。
- S15 · inverse_equivalence · contrapositive — 命題與其逆否命題邏輯等價，雙向成立；但這與「逆命題」不同，逆命題沒有被證明。
- S14.3 · inverse_equivalence · distributive, finite_sum_rules, finite_sum_regroup — 提出常數與重組有限和都是等值改寫，可倒推。此子步不使用 L_indep_prod。
- S14.2 · premise_audit · S14.1, mko_indep_def — 這一步依賴獨立假設對「每個」值對成立；只對部分值對成立不夠。沒有獨立假設時不能做此代換。此子步不使用 L_indep_prod。
- S14.1 · inverse_equivalence · finite_sum_regroup, marginal_def — 刪去值為 0 的項就回到原和，雙向成立。此子步不使用 L_indep_prod。
- S14 · premise_audit · S01, L_indep_prod — 只證「獨立 ⇒ 協方差為零」；反向「協方差為零 ⇒ 獨立」不宣稱，而且 S16、S17 會證明它一般是錯的。
- S13 · inverse_equivalence · S10, S11, S12, eq_replace — 等值代入可倒推，兩邊是同一個數。
- S12 · inverse_equivalence · numeric_evaluation — 精確有理數求值，兩邊是同一個數。
- S11 · inverse_equivalence · numeric_evaluation — 精確有理數求值，兩邊是同一個數。
- S10 · inverse_equivalence · numeric_evaluation — 精確有理數求值，兩邊是同一個數。
- S09 · premise_audit · G3, mko_joint_def — 逐項核了三項資格與 Y=X² 的三個值對；不宣稱反向。
- S08 · inverse_equivalence · S06, S07, distributive, add_inverse — 每一步都是等值代換與加減同項，可倒推；兩邊是同一個實數。
- S07 · inverse_equivalence · distributive, mul_comm — 實數的展開與因式分解互逆，雙向成立。
- S06 · premise_audit · S03, S05, L_lin_exp — 需要 S05 的逐點等式（相等的函數有相等的期望）與引理；線性不需要獨立性。
- S05 · inverse_equivalence · distributive, mul_comm — 因式分解是展開的反向，兩式在每個 s 上相等，雙向成立。
- S04 · premise_audit · S03, G2, L_lin_exp — 只需引理與 a、b、c、d 為常數；aX+b 與 cY+d 都定義在同一個 (S,p) 上。
- S03.2 · inverse_equivalence · finite_sum_rules, mul_one — 提出常數與乘以 1 都可倒推；所用條件是 Σp=1。此子步不使用 L_lin_exp。
- S03.1 · inverse_equivalence · distributive, finite_sum_rules — 分配律與有限和的重排都是等值改寫，可逐步倒推。此子步不使用 L_lin_exp。
- S03 · premise_audit · G1, L_lin_exp — 引理的前提是同一個有限 joint law 與總和為 1 的權重；兩者都由 G1 提供。
- S02 · inverse_equivalence · mul_comm, eq_replace — 兩邊只差乘法順序，同一改寫倒過來就回到原式，雙向成立。
- S01 · premise_audit · G1, mko_cov_def, mko_expectation_def — 此步只寫出定義，不推出新事實；它要求三個期望來自同一個 (S,p)。





## 錯誤控制與反例

零協方差不等於獨立MKO 指出的常見誤解是看到 Cov=0 就宣稱獨立。本稿的例子 Y=X² 完全由 X 決定，卻有 Cov(X,Y)=0（S13）；而 (0,1) 這一個值對就否證了獨立（S16）。S14 只給「獨立 ⇒ Cov=0」這一個方向。

所有期望必須來自同一 joint law考慮 L1：(0,0)、(1,1) 各 1/2；L2：(0,0)、(0,1)、(1,0)、(1,1) 各 1/4。兩者的邊際都是 P(X=1)=P(Y=1)=1/2，但 L1 上 Cov=1/2−1/4=1/4，L2 上 Cov=1/4−1/4=0。所以協方差由 joint law 決定，不由邊際決定；把 L2 的 E[XY] 與 L1 的 E[X]、E[Y] 混用，會得到與 L1 無關的數。

仿射規則：常數消失，係數相乘S08 中 b、d 完全消失，a、c 以乘積 ac 出現，正負號保留。例如 Cov(2X+1,−3Y+5)=−6·Cov(X,Y)，不是 6·Cov(X,Y)，也不是 −6·Cov(X,Y)+5。N10、N11 在例子中以 U=2X+1、V=−3X+5 核對：直接計算與 2·(−3)·Cov(X,X)=−4 一致。


- 例子中 Cov(X,Y)=0，所以 X、Y 獨立 → reject — P(X=0,Y=1)=0，但 P(X=0)P(Y=1)=2/9。
- Cov(2X+1,−3Y+5)=6·Cov(X,Y)+5 → reject — 依 S08 等於 2·(−3)·Cov(X,Y)=−6·Cov(X,Y)；常數 1、5 不出現。
- 只要知道 X 與 Y 的兩個邊際表，就能算出 Cov(X,Y) → reject — L1 與 L2 的邊際相同，協方差卻分別是 1/4 與 0。
- X、Y 獨立而 Cov(X,Y)=1/5 是可能的 → reject — S14：在有限 joint law 上獨立蘊含 Cov(X,Y)=0。





## 結論與限制

在同一有限 joint law 上，Cov(Y,X)=Cov(X,Y)，Cov(aX+b,cY+d)=ac·Cov(X,Y)；獨立蘊含 Cov=0，所以非零協方差可否證獨立。對 X 均勻取 −1、0、1 且 Y=X² 的 law，E[X]=0、E[Y]=2/3、E[XY]=0、Cov(X,Y)=0，但 P(X=0,Y=1)=0≠2/9=P(X=0)P(Y=1)，X、Y 不獨立：零協方差不蘊含獨立。


- 有限和重組（finite_sum_regroup）與 marginal_def 是本稿的前提，不在本稿中由更基本的公理推出。
- N10、N11 只在例子的 joint law 上以 U=2X+1、V=−3X+5 交叉核對 S08，不能取代 S08 的一般證明；N12、N13 是錯誤控制中 L1、L2 的數值。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 66770666a1625742c7623b7027ec9998c2e93b136060117940329d5723701fbc
- original source SHA-256: 66770666a1625742c7623b7027ec9998c2e93b136060117940329d5723701fbc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-covariance-01.json)