Independence of random variables: checking the complete finite joint table, with zero covariance only a consequence

Goal and scope

(1) Joint table J₁: X∈{0,1}, Y∈{0,1,2}, P(0,0)=1/12, P(0,1)=1/12, P(0,2)=1/6, P(1,0)=1/6, P(1,1)=1/6, P(1,2)=1/3. Aggregate both marginals from the joint table, check the product equation at all 6 value pairs, and decide whether X and Y are independent; also prove that independence implies independence of any coordinate events {X∈S} and {Y∈T} and E[XY]=E[X]E[Y]. (2) Joint table J₂: X uniform on {−1,0,1} and Y=X². Prove Cov(X,Y)=0 although X and Y are not independent. (3) Use joint table J₃ to show that checking a single value pair is not enough.

Works inside the MKO's scope: the complete finite joint support and exact rational masses belong to one probability model (assumption a1); mainly two variables are handled, and three or more variables appear only in a negative control showing that pairwise independence does not give mutual independence (assumption a2). Zero covariance serves only as a necessary consequence, never as a converse certificate. Continuous distributions and IID sequences (the next node) are not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• prob_axioms
• frac_rules
• distributive
• finite_sum_rules
• numeric_evaluation

• G1 — J₁: value sets X∈{0,1}, Y∈{0,1,2}; p(0,0)=1/12, p(0,1)=1/12, p(0,2)=1/6, p(1,0)=1/6, p(1,1)=1/6, p(1,2)=1/3.
• G2 — J₂: value sets X∈{−1,0,1}, Y∈{0,1}; p(−1,1)=1/3, p(0,0)=1/3, p(1,1)=1/3, and the remaining pairs (−1,0), (0,1), (1,0) have mass 0 (that is, Y=X²).
• G3 — J₃: value sets X∈{0,1}, Y∈{0,1,2}; p(0,0)=1/4, p(0,1)=1/4, p(0,2)=0, p(1,0)=1/4, p(1,1)=0, p(1,2)=1/4.

• p(x,y)=P(X=x,Y=y) — the joint mass
• P(X=x),\ P(Y=y) — the marginals aggregated from the joint table
• J_1,J_2,J_3 — the three joint tables
• E[\cdot] — expectation, a weighted sum over the joint table
• \operatorname{Cov}(X,Y)=E[XY]-E[X]E[Y] — the covariance
• S,T — subsets of the value sets of X and Y (rectangle events)

Rules and sources

• prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A).
• 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.
• 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.
• 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.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_rv_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). Equivalently, all inverse images of value events are independent. This slice checks the complete finite joint table; zero covariance is only a consequence, never a converse certificate. · mko-random-variable-independence
• 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
• expectation_def · prerequisite — For a finite joint table, E[g(X,Y)]=Σ_{(x,y)} g(x,y)p(x,y); in particular E[X]=Σ_x x P(X=x) and Cov(X,Y)=E[XY]−E[X]E[Y].
• L_rect · lemma — If p(x,y)=P(X=x)P(Y=y) for all value pairs, then for any subsets S, T of the value sets: P(X∈S, Y∈T)=P(X∈S)P(Y∈T).
• L_EXY · lemma — If p(x,y)=P(X=x)P(Y=y) for all value pairs, then E[XY]=E[X]E[Y], so Cov(X,Y)=0.

Main derivation

J_1:\ p(x,y)\ge0

\sum_{(x,y)}p(x,y)=\tfrac1{12}+\tfrac1{12}+\tfrac16+\tfrac16+\tfrac16+\tfrac13=1

P(X=0)=\sum_{y}p(0,y),\ P(X=1)=\sum_{y}p(1,y)

P(X=0)=\tfrac1{12}+\tfrac1{12}+\tfrac16=\tfrac13,\ \ P(X=1)=\tfrac16+\tfrac16+\tfrac13=\tfrac23

P(Y=y)=\sum_{x}p(x,y)

P(Y=0)=\tfrac1{12}+\tfrac16=\tfrac14,\ P(Y=1)=\tfrac1{12}+\tfrac16=\tfrac14,\ P(Y=2)=\tfrac16+\tfrac13=\tfrac12

X,Y\ \text{independent}

\forall x\in\{0,1\}\ \forall y\in\{0,1,2\}:\ p(x,y)=P(X=x)P(Y=y)

x=0:\ P(X=0)=\tfrac13

\tfrac13\cdot\tfrac14=\tfrac1{12}=p(0,0),\ \tfrac13\cdot\tfrac14=\tfrac1{12}=p(0,1),\ \tfrac13\cdot\tfrac12=\tfrac16=p(0,2)

x=1:\ P(X=1)=\tfrac23

\tfrac23\cdot\tfrac14=\tfrac16=p(1,0),\ \tfrac23\cdot\tfrac14=\tfrac16=p(1,1),\ \tfrac23\cdot\tfrac12=\tfrac13=p(1,2)

6\ \text{of}\ 6\ \text{value pairs factor}

X,Y\ \text{independent under}\ J_1

S=\{1\},\ T=\{1,2\}

P(X\in S,Y\in T)=\tfrac16+\tfrac13=\tfrac12=\tfrac23\cdot\tfrac34=P(X\in S)P(Y\in T)

X,Y\ \text{independent}

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

E[X]=\tfrac23,\ E[Y]=0\cdot\tfrac14+1\cdot\tfrac14+2\cdot\tfrac12=\tfrac54

E[XY]=1\cdot1\cdot\tfrac16+1\cdot2\cdot\tfrac13=\tfrac56=\tfrac23\cdot\tfrac54

J_2:\ P(X=x)=\tfrac13\ (x=-1,0,1),\ P(Y=0)=\tfrac13,\ P(Y=1)=\tfrac23

E[X]=0,\ E[XY]=(-1)(1)\tfrac13+0+(1)(1)\tfrac13=0\ \Rightarrow\ \operatorname{Cov}(X,Y)=0-0\cdot\tfrac23=0

p(0,1)=0,\ P(X=0)P(Y=1)=\tfrac13\cdot\tfrac23=\tfrac29

0\neq\tfrac29\ \Rightarrow\ X,Y\ \text{not independent, although}\ \operatorname{Cov}=0

J_3:\ P(X=0)=\tfrac12,\ P(Y=0)=\tfrac12,\ P(Y=1)=\tfrac14

p(0,0)=\tfrac14=\tfrac12\cdot\tfrac12\ \text{but}\ p(0,1)=\tfrac14\neq\tfrac18=\tfrac12\cdot\tfrac14

\text{S07},\ \text{S08},\ \text{S09},\ \text{S12},\ \text{S13}

J_1:\ X\perp Y;\ J_2:\ \operatorname{Cov}=0,\ X\not\perp Y;\ J_3:\ X\not\perp Y

Substeps and lemmas

P(X\in S,Y\in T)

\sum_{x\in S}\sum_{y\in T}p(x,y)

\sum_{x\in S}\sum_{y\in T}P(X=x)P(Y=y)

\Big(\sum_{x\in S}P(X=x)\Big)\Big(\sum_{y\in T}P(Y=y)\Big)=P(X\in S)P(Y\in T)

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

E[XY]=\sum_{x}\sum_{y}\big(xP(X=x)\big)\big(yP(Y=y)\big)

\sum_{x}\sum_{y}\big(xP(X=x)\big)\big(yP(Y=y)\big)

\Big(\sum_{x}xP(X=x)\Big)\Big(\sum_{y}yP(Y=y)\Big)=E[X]E[Y]

Reverse audits

• S14 · sufficient_goal_reduction · S07, S08, S09, S12, S13, and_intro_elim — The goal is the conjunction of the three tasks; each part is proved forwards by the listed steps, and H⇒G by conjunction introduction.
• S13 · premise_audit · quantifier_negation, prob_axioms, numeric_evaluation — One passing pair does not give the universal statement (N11), while one failing pair refutes it (N12).
• S12 · premise_audit · mko_rv_indep_def, quantifier_negation, numeric_evaluation — Refuting the universal statement needs one failing value pair (N10); pairs of mass 0 must be checked too.
• S11 · premise_audit · expectation_def, prob_axioms, numeric_evaluation — Exact computation (N9); zero covariance is just a fact here and implies nothing yet about independence.
• S10 · premise_audit · S09, numeric_evaluation — This is an independent recomputation for J₁ (N8), not a proof of the lemma.
• S09.2 · inverse_equivalence · finite_sum_rules, distributive — Distributivity of finite sums is an equation, valid both ways.
• S09.1 · premise_audit · expectation_def, mul_comm, mul_assoc — The substitution needs the product equation for all value pairs.
• S09 · premise_audit · S07, L_EXY — Only independence ⇒ zero covariance is claimed; the converse is refuted by J₂.
• S08.2 · premise_audit · S08.1, finite_sum_rules, distributive, prob_axioms — It needs the product equation for all value pairs; if it held only for some pairs, the substitution would not be valid.
• S08.1 · inverse_equivalence · prob_axioms, mko_joint_def — Additivity is an equation, valid both ways; distinct pairs ensure nothing is double counted.
• S08 · premise_audit · S07, L_rect, numeric_evaluation — The converse (rectangle independence ⇒ pair independence) follows with S={x}, T={y}, but this step does not need it; the numbers are checked by N7.
• S07 · sufficient_goal_reduction · S04, S05, S06, case_analysis — Goal: independence. Sufficient condition: all 6 pairs pass; H⇒G by the definition, and H is proved forwards from the givens.
• S06 · premise_audit · frac_rules, numeric_evaluation — Exact comparisons (N5, N6).
• S05 · premise_audit · frac_rules, numeric_evaluation — Each equation is an exact rational comparison (N4, N13).
• S04 · premise_audit · mko_rv_indep_def — It only unfolds the definition; the quantifier ranges over the complete set of value pairs, not a few samples.
• S03 · inverse_equivalence · prob_axioms, frac_rules — Exact computation; both sides have the same value (N3).
• S02 · inverse_equivalence · prob_axioms, frac_rules — Exact rational sums; both sides have the same value (N2).
• S01 · premise_audit · mko_joint_def, G1 — It only checks the setting (N1); if the total were not 1 there would be no probability model and later decisions would be meaningless.

Error controls and negative controls

Zero covariance is not a certificate of independence

The MKO's misconception is to declare independence from zero covariance. S09 proves independence ⇒ Cov=0, but in J₂, Y is completely determined by X (Y=X²) and still Cov=0. Zero covariance rules out only 'linear' association, not other dependence.

Checking one value pair is not enough

In J₃ the pair (0,0) satisfies 1/4=(1/2)(1/2) but (0,1) does not. Independence quantifies over every value pair, including pairs of mass 0 (in J₂ it is exactly the zero-mass pair (0,1) that fails).

Marginals alone are not enough

J₃ has marginals X: (1/2,1/2) and Y: (1/2,1/4,1/4). The independent table with the same marginals is (1/4,1/8,1/8; 1/4,1/8,1/8), which differs from J₃. Marginals do not determine the joint law, so the joint table must be compared pair by pair.

• In J₂, Cov(X,Y)=0, so X and Y are independent → reject — p(0,1)=0 but P(X=0)P(Y=1)=2/9.
• In J₃, P(X=0,Y=0)=P(X=0)P(Y=0), so X and Y are independent → reject — (0,1) fails: 1/4≠(1/2)(1/4)=1/8.
• J₃ has the same marginals as an independent table, so X, Y are independent under J₃ → reject — Marginals do not determine the joint table; J₃ has p(0,1)=1/4 while the independent table has 1/8.
• X, Y are independent fair 0/1 variables and Z=(X+Y) mod 2; X, Y, Z are pairwise independent, so the three are mutually independent → reject — P(X=0,Y=0,Z=1)=0 but (1/2)³=1/8; pairwise independence does not give mutual independence.

Result and limitations

J₁ has marginals P(X=0)=1/3, P(X=1)=2/3, P(Y=0)=1/4, P(Y=1)=1/4, P(Y=2)=1/2, and all 6 value pairs satisfy p(x,y)=P(X=x)P(Y=y), so X and Y are independent; hence any coordinate events {X∈S} and {Y∈T} are independent too (for example 1/2=(2/3)(3/4)), and E[XY]=5/6=E[X]E[Y]. In J₂ (Y=X²), Cov(X,Y)=0 but p(0,1)=0≠2/9, so they are not independent. In J₃, (0,0) passes but (0,1) fails, so they are not independent.

• The pairwise independence of X, Y, Z in the fourth negative control is stated for illustration and not checked pair by pair in this guide.
• L_EXY is used only for finite-valued variables; infinite-valued or continuous variables need integrability conditions and are outside this guide's scope.

Verification and source binding

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

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

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