Covariance: symmetry, the affine rule, and why zero covariance does not imply independence

Goal and scope

On one exact finite joint law: (1) prove Cov(Y,X)=Cov(X,Y); (2) prove Cov(aX+b,cY+d)=ac·Cov(X,Y); (3) prove that independence of X and Y gives Cov(X,Y)=0, so a nonzero covariance refutes independence; (4) for the joint law with X uniform on −1, 0, 1 and Y=X², compute E[X], E[Y], E[XY] and Cov(X,Y)=0, and prove that X and Y are not independent.

Stays inside the MKO: every expectation is computed from one exact finite joint law (assumption a1); nonzero covariance can refute independence, while zero covariance cannot in general prove it (assumption a2). Correlation coefficients, conditional expectation and infinite sample spaces are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• distributive
• finite_sum_rules
• mul_comm
• numeric_evaluation
• marginal_def
• finite_sum_regroup

• G1 — (S,p) is a finite joint law: S consists of distinct integer pairs, each p(s)≥0 is an exact rational and Σ_{s∈S} p(s)=1. X and Y are the coordinates: at s=(x,y), X=x and Y=y. Every expectation is E[g]=Σ_{s∈S} p(s)g(s) with this one (S,p).
• G2 — a, b, c, d are real constants.
• G3 — Example: S={(−1,1),(0,0),(1,1)}, each pair with mass 1/3.

• (S,p) — finite joint law: distinct integer pairs with exact masses
• E[g] — expectation on the same joint law, Σ_{s∈S} p(s)g(s)
• \operatorname{Cov}(X,Y) — covariance E[XY]−E[X]E[Y]
• a,\ b,\ c,\ d — real coefficients of the affine maps
• S_X,\ S_Y — the sets of first and of second coordinates occurring in S
• p_X,\ p_Y — marginal masses of X and Y

Rules and sources

• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{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 — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• add_zero · prerequisite — Additive identity: u+0=u.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_cov_def · cited — For X,Y on the same finite joint law, Cov(X,Y)=E[XY]−E[X]E[Y]. Covariance is symmetric in the two variables, and affine transformations satisfy Cov(aX+b,cY+d)=ac Cov(X,Y). · mko-covariance
• mko_expectation_def · cited — For nonempty finite S, normalized nonnegative weights w_s, and a real random variable X, define E[X]=Σ_(s∈S)w_s X(s). · mko-expectation
• mko_joint_def · cited — A two-dimensional finite joint distribution lists distinct pairs (x,y) and nonnegative exact masses summing exactly to 1. Marginals, rectangle events and single-pair masses all aggregate from that same joint law. · mko-finite-joint-distribution
• mko_indep_def · cited — Finite-valued X,Y are independent if every pair (x,y) satisfies P(X=x,Y=y)=P(X=x)P(Y=y). · mko-random-variable-independence
• marginal_def · prerequisite — Marginals: p_X(x)=P(X=x)=Σ_{y:(x,y)∈S} p(x,y) and p_Y(y)=P(Y=y)=Σ_{x:(x,y)∈S} p(x,y); P(X=x,Y=y) is p(x,y) when (x,y)∈S and 0 otherwise.
• finite_sum_regroup · prerequisite — Regrouping a finite sum: if a finite set is split into pairwise disjoint pieces (each element in exactly one), the sum over the whole set equals the total of the sums over the pieces; adding terms equal to 0 does not change a finite sum.
• L_lin_exp · lemma — On one finite joint law, for real functions U_1 to U_m of (X,Y) and reals c_1 to c_m: E[Σ_{k=1}^{m} c_k U_k]=Σ_{k=1}^{m} c_k E[U_k]; a constant c has expectation c.
• L_indep_prod · lemma — If X and Y are independent on a finite joint law, then E[XY]=E[X]E[Y].

Main derivation

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}

Substeps and lemmas

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

Reverse audits

• S17 · sufficient_goal_reduction · S13, S16, exists_intro — Goal G: zero covariance does not in general prove independence. Sufficient condition H: some finite joint law has zero covariance but is not independent; H⇒G because one counterexample refutes a universal claim. H is proved forwards in S09 to S16.
• S16 · premise_audit · S09, marginal_def, mko_indep_def — Refutation needs only one pair where equality fails; the support list must be complete to know that the mass of (0,1) is 0.
• S15 · inverse_equivalence · contrapositive — A statement and its contrapositive are logically equivalent, so the step is two-way; this is different from the converse, which is not proved.
• S14.3 · inverse_equivalence · distributive, finite_sum_rules, finite_sum_regroup — Pulling out constants and regrouping finite sums are rewrites of equal values and can be reversed. This sub-step does not use L_indep_prod.
• S14.2 · premise_audit · S14.1, mko_indep_def — This step depends on the independence hypothesis holding for every pair; holding for some pairs is not enough. Without independence the substitution cannot be made. This sub-step does not use L_indep_prod.
• S14.1 · inverse_equivalence · finite_sum_regroup, marginal_def — Deleting the zero terms returns the original sum, so it holds both ways. This sub-step does not use L_indep_prod.
• S14 · premise_audit · S01, L_indep_prod — Only 'independent ⇒ zero covariance' is proved; the converse 'zero covariance ⇒ independent' is not claimed, and S16 and S17 show it is false in general.
• S13 · inverse_equivalence · S10, S11, S12, eq_replace — Substituting equals can be reversed; both sides are the same number.
• S12 · inverse_equivalence · numeric_evaluation — Exact rational evaluation; both sides are the same number.
• S11 · inverse_equivalence · numeric_evaluation — Exact rational evaluation; both sides are the same number.
• S10 · inverse_equivalence · numeric_evaluation — Exact rational evaluation; both sides are the same number.
• S09 · premise_audit · G3, mko_joint_def — The three requirements and Y=X² were checked on each of the three pairs; no converse is claimed.
• S08 · inverse_equivalence · S06, S07, distributive, add_inverse — Every move replaces equals or adds and removes the same term, so it can be reversed; both sides are the same real number.
• S07 · inverse_equivalence · distributive, mul_comm — Expanding and factoring reals are inverse rewrites, so it holds both ways.
• S06 · premise_audit · S03, S05, L_lin_exp — It needs the pointwise identity of S05 (equal functions have equal expectations) and the lemma; linearity needs no independence.
• S05 · inverse_equivalence · distributive, mul_comm — Factoring is the reverse of expanding; the two expressions agree at every s, so the step holds both ways.
• S04 · premise_audit · S03, G2, L_lin_exp — It needs only the lemma and that a, b, c, d are constants; aX+b and cY+d both live on the same (S,p).
• S03.2 · inverse_equivalence · finite_sum_rules, mul_one — Pulling out a constant and multiplying by 1 can both be reversed; the condition used is Σp=1. This sub-step does not use L_lin_exp.
• S03.1 · inverse_equivalence · distributive, finite_sum_rules — Distributivity and rearranging finite sums are rewrites of equal values and can be reversed step by step. This sub-step does not use L_lin_exp.
• S03 · premise_audit · G1, L_lin_exp — The lemma's hypotheses are one finite joint law and weights summing to 1, both supplied by G1.
• S02 · inverse_equivalence · mul_comm, eq_replace — The two sides differ only in the order of multiplication; the same rewrite read backwards returns the original, so it holds both ways.
• S01 · premise_audit · G1, mko_cov_def, mko_expectation_def — This step only states the definition and derives no new fact; it requires the three expectations to come from the same (S,p).

Error controls and negative controls

Zero covariance is not independence

The common mistake named by the MKO is to declare independence on seeing Cov=0. In this guide Y=X² is completely determined by X, yet Cov(X,Y)=0 (S13); the single pair (0,1) refutes independence (S16). S14 gives only the direction 'independent ⇒ Cov=0'.

All expectations must come from one joint law

Take L1: (0,0) and (1,1) with 1/2 each; and L2: (0,0), (0,1), (1,0), (1,1) with 1/4 each. Both have marginals P(X=1)=P(Y=1)=1/2, but Cov=1/2−1/4=1/4 on L1 and Cov=1/4−1/4=0 on L2. So covariance is fixed by the joint law, not by the marginals; mixing E[XY] from L2 with E[X], E[Y] from L1 gives a number unrelated to L1.

The affine rule: constants vanish, coefficients multiply

In S08, b and d vanish completely and a, c appear as the product ac with the sign kept. For example Cov(2X+1,−3Y+5)=−6·Cov(X,Y), not 6·Cov(X,Y) and not −6·Cov(X,Y)+5. N10 and N11 check this on the example with U=2X+1 and V=−3X+5: the direct computation agrees with 2·(−3)·Cov(X,X)=−4.

• In the example Cov(X,Y)=0, so X and Y are independent → reject — P(X=0,Y=1)=0 but P(X=0)P(Y=1)=2/9.
• Cov(2X+1,−3Y+5)=6·Cov(X,Y)+5 → reject — By S08 it equals 2·(−3)·Cov(X,Y)=−6·Cov(X,Y); the constants 1 and 5 do not appear.
• Knowing the two marginal tables of X and Y suffices to compute Cov(X,Y) → reject — L1 and L2 have the same marginals but covariances 1/4 and 0.
• It is possible that X and Y are independent while Cov(X,Y)=1/5 → reject — S14: on a finite joint law, independence implies Cov(X,Y)=0.

Result and limitations

On one finite joint law, Cov(Y,X)=Cov(X,Y) and Cov(aX+b,cY+d)=ac·Cov(X,Y); independence implies Cov=0, so a nonzero covariance refutes independence. For the law with X uniform on −1, 0, 1 and Y=X², E[X]=0, E[Y]=2/3, E[XY]=0 and Cov(X,Y)=0, but P(X=0,Y=1)=0≠2/9=P(X=0)P(Y=1), so X and Y are dependent: zero covariance does not imply independence.

• Regrouping of finite sums (finite_sum_regroup) and marginal_def are premises of this guide; they are not derived here from more basic axioms.
• N10 and N11 cross-check S08 only on the example law with U=2X+1 and V=−3X+5 and cannot replace the general proof of S08; N12 and N13 are the numbers of L1 and L2 in the error controls.

Verification and source binding

13 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)