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

目標與範圍

在同一個精確有限 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]。

逐步主鏈

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)

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

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

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

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

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

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

(aX+b)(cY+d)

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

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

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

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

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

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

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

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

E[X]=0

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

E[Y]=\tfrac23

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

E[XY]=0

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

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

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

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

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

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

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

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

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

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

局部子步與引理

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

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

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

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)

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

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

逐步反向審查

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