# Independence of random variables: checking the complete finite joint table, with zero covariance only a consequence [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-random-variable-independence/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-random-variable-independence-01 · production-20261019-adopted-96 ## 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 S01 · definitionBefore J_1:\ p(x,y)\ge0 After \sum_{(x,y)}p(x,y)=\tfrac1{12}+\tfrac1{12}+\tfrac16+\tfrac16+\tfrac16+\tfrac13=1 Conditions: none Rule: mko_joint_def · Uses: G1, mko_joint_def Leaf basis: mko_joint_def + numeric_evaluation First confirm that J₁ is the complete joint table of one probability model: 6 distinct value pairs, all masses nonnegative, and with denominator 12 the total is 1+1+2+2+2+4=12, that is 1. Marginals and products are computed from this table from here on. S02 · equivalentBefore P(X=0)=\sum_{y}p(0,y),\ P(X=1)=\sum_{y}p(1,y) After P(X=0)=\tfrac1{12}+\tfrac1{12}+\tfrac16=\tfrac13,\ \ P(X=1)=\tfrac16+\tfrac16+\tfrac13=\tfrac23 Conditions: none Rule: prob_axioms · Uses: S01, prob_axioms Leaf basis: prob_axioms + frac_rules + numeric_evaluation The event {X=x} is the disjoint union of the 3 pair events {X=x,Y=y}, so by additivity sum that row (the MKO: first aggregate the marginals from the joint table). S03 · equivalentBefore P(Y=y)=\sum_{x}p(x,y) After P(Y=0)=\tfrac1{12}+\tfrac16=\tfrac14,\ P(Y=1)=\tfrac1{12}+\tfrac16=\tfrac14,\ P(Y=2)=\tfrac16+\tfrac13=\tfrac12 Conditions: none Rule: prob_axioms · Uses: S01, prob_axioms Leaf basis: prob_axioms + frac_rules + numeric_evaluation Likewise sum each column. The three marginals add to 1/4+1/4+1/2=1, a consistency check. S04 · definitionBefore X,Y\ \text{independent} After \forall x\in\{0,1\}\ \forall y\in\{0,1,2\}:\ p(x,y)=P(X=x)P(Y=y) Conditions: none Rule: mko_rv_indep_def · Uses: mko_rv_indep_def Leaf basis: mko_rv_indep_def + def_unfold By the MKO, independence requires every value pair to pass the product equation; the product of the value sets has 2·3=6 pairs, and all must be checked, including any pair of mass 0. S05 · impliesBefore x=0:\ P(X=0)=\tfrac13 After \tfrac13\cdot\tfrac14=\tfrac1{12}=p(0,0),\ \tfrac13\cdot\tfrac14=\tfrac1{12}=p(0,1),\ \tfrac13\cdot\tfrac12=\tfrac16=p(0,2) Conditions: none Rule: frac_rules · Uses: S02, S03, G1 Leaf basis: frac_rules + numeric_evaluation The three pairs of the first row: the products are 1/12, 1/12 and 1/6, exactly equal to the masses in G1. S06 · impliesBefore x=1:\ P(X=1)=\tfrac23 After \tfrac23\cdot\tfrac14=\tfrac16=p(1,0),\ \tfrac23\cdot\tfrac14=\tfrac16=p(1,1),\ \tfrac23\cdot\tfrac12=\tfrac13=p(1,2) Conditions: none Rule: frac_rules · Uses: S02, S03, G1 Leaf basis: frac_rules + numeric_evaluation The three pairs of the second row: the products are 1/6, 1/6 and 1/3, again equal to the masses. S07 · impliesBefore 6\ \text{of}\ 6\ \text{value pairs factor} After X,Y\ \text{independent under}\ J_1 Conditions: none Rule: case_analysis · Uses: S04, S05, S06 Leaf basis: case_analysis + mko_rv_indep_def S05 and S06 cover all 6 pairs of {0,1}×{0,1,2} (the cases x=0 and x=1 are exhaustive) and every pair passes, so by the definition in S04, X and Y are independent. This is an exhaustive check of the complete finite table, not a sample. S08 · impliesBefore S=\{1\},\ T=\{1,2\} After P(X\in S,Y\in T)=\tfrac16+\tfrac13=\tfrac12=\tfrac23\cdot\tfrac34=P(X\in S)P(Y\in T) Conditions: none Rule: L_rect · Uses: S07 Leaf basis: finite_sum_rules + distributive + prob_axioms The MKO says independence is equivalent to independence of all inverse images of value events. By Lemma L_rect, the product equation for value pairs implies it for every rectangle event. Example: S={1}, T={1,2}; the left side is p(1,1)+p(1,2)=1/2 and the right side (2/3)(1/4+1/2)=(2/3)(3/4)=1/2. The lemma is proved in sub-steps S08.1 and S08.2. S09 · impliesBefore X,Y\ \text{independent} After E[XY]=E[X]E[Y],\ \ \operatorname{Cov}(X,Y)=0 Conditions: none Rule: L_EXY · Uses: S07, expectation_def Leaf basis: finite_sum_rules + distributive + expectation_def The MKO notes that independence implies zero covariance (second moments of finite-valued variables are automatically finite). By Lemma L_EXY, the pair product equation gives E[XY]=E[X]E[Y]. The lemma is proved in sub-steps S09.1 and S09.2. This is a necessary consequence, not a sufficient condition (see S12). S10 · impliesBefore E[X]=\tfrac23,\ E[Y]=0\cdot\tfrac14+1\cdot\tfrac14+2\cdot\tfrac12=\tfrac54 After E[XY]=1\cdot1\cdot\tfrac16+1\cdot2\cdot\tfrac13=\tfrac56=\tfrac23\cdot\tfrac54 Conditions: none Rule: numeric_evaluation · Uses: S02, S03, S09, G1 Leaf basis: numeric_evaluation + expectation_def Direct check of S09: only the pairs with x=1 and y≠0 contribute to E[XY], giving 1/6+2/3=5/6; E[X]E[Y]=(2/3)(5/4)=10/12=5/6. They agree, Cov=0, as the lemma predicts. S11 · impliesBefore J_2:\ P(X=x)=\tfrac13\ (x=-1,0,1),\ P(Y=0)=\tfrac13,\ P(Y=1)=\tfrac23 After E[X]=0,\ E[XY]=(-1)(1)\tfrac13+0+(1)(1)\tfrac13=0\ \Rightarrow\ \operatorname{Cov}(X,Y)=0-0\cdot\tfrac23=0 Conditions: none Rule: expectation_def · Uses: G2, expectation_def, prob_axioms Leaf basis: expectation_def + prob_axioms + numeric_evaluation Marginals of J₂: X takes each of its three values with probability 1/3; Y=0 comes only from (0,0), with probability 1/3; Y=1 comes from (−1,1) and (1,1), with probability 2/3. E[X]=(−1+0+1)/3=0; E[XY] has only the two nonzero terms −1/3 and 1/3, which sum to 0. Hence Cov(X,Y)=0. S12 · impliesBefore p(0,1)=0,\ P(X=0)P(Y=1)=\tfrac13\cdot\tfrac23=\tfrac29 After 0\neq\tfrac29\ \Rightarrow\ X,Y\ \text{not independent, although}\ \operatorname{Cov}=0 Conditions: none Rule: quantifier_negation · Uses: S11, G2, mko_rv_indep_def Leaf basis: quantifier_negation + mko_rv_indep_def + numeric_evaluation The pair (0,1) cannot occur (X=0 forces Y=0), so its mass is 0, but the product is 2/9≠0. The product equation fails at one value pair, so X and Y are not independent, although S11 gives Cov=0. Zero covariance therefore cannot certify independence, the misconception the MKO names. S13 · impliesBefore J_3:\ P(X=0)=\tfrac12,\ P(Y=0)=\tfrac12,\ P(Y=1)=\tfrac14 After p(0,0)=\tfrac14=\tfrac12\cdot\tfrac12\ \text{but}\ p(0,1)=\tfrac14\neq\tfrac18=\tfrac12\cdot\tfrac14 Conditions: none Rule: quantifier_negation · Uses: G3, prob_axioms, mko_rv_indep_def Leaf basis: quantifier_negation + prob_axioms + numeric_evaluation Marginals of J₃: P(X=0)=1/4+1/4+0=1/2 and P(X=1)=1/2; P(Y=0)=1/2, P(Y=1)=1/4, P(Y=2)=1/4. The pair (0,0) passes the product equation, so checking only it would wrongly suggest independence; but (0,1) fails: 1/4≠1/8. So under J₃, X and Y are not independent, and every value pair must be checked. S14 · impliesBefore \text{S07},\ \text{S08},\ \text{S09},\ \text{S12},\ \text{S13} After J_1:\ X\perp Y;\ J_2:\ \operatorname{Cov}=0,\ X\not\perp Y;\ J_3:\ X\not\perp Y Conditions: none Rule: and_intro_elim · Uses: S07, S08, S09, S10, S12, S13 Leaf basis: and_intro_elim Combine: all 6 value pairs of J₁ pass, so X and Y are independent, which implies independence of rectangle events and zero covariance; J₂ has zero covariance but is not independent; J₃ passes one value pair but is not independent. ## Substeps and lemmas S08.1 · equivalentBefore P(X\in S,Y\in T) After \sum_{x\in S}\sum_{y\in T}p(x,y) Conditions: none Rule: prob_axioms · Uses: prob_axioms, mko_joint_def Leaf basis: prob_axioms + mko_joint_def The event {X∈S, Y∈T} is the disjoint union of the pair events {X=x,Y=y} with x∈S and y∈T, so by additivity its probability is the sum of these masses. S08.2 · impliesBefore \sum_{x\in S}\sum_{y\in T}P(X=x)P(Y=y) After \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) Conditions: p(x,y)=P(X=x)P(Y=y)\ \forall x,y Rule: distributive · Uses: S08.1, finite_sum_rules, distributive Leaf basis: finite_sum_rules + distributive + prob_axioms Substitute the hypothesis p(x,y)=P(X=x)P(Y=y); the inner sum pulls out P(X=x), which does not depend on y, and the outer sum pulls out Σ_y P(Y=y) (distributivity of finite sums); by additivity the two sums are P(X∈S) and P(Y∈T). S08.1 and S08.2 together prove Lemma L_rect. S09.1 · impliesBefore E[XY]=\sum_{x}\sum_{y}xy\,p(x,y) After E[XY]=\sum_{x}\sum_{y}\big(xP(X=x)\big)\big(yP(Y=y)\big) Conditions: p(x,y)=P(X=x)P(Y=y)\ \forall x,y Rule: expectation_def · Uses: expectation_def Leaf basis: expectation_def + mul_comm + mul_assoc By the definition of expectation, sum over all value pairs; then replace each p(x,y) by P(X=x)P(Y=y) and rearrange each term as (xP(X=x))(yP(Y=y)) by commutativity and associativity. S09.2 · equivalentBefore \sum_{x}\sum_{y}\big(xP(X=x)\big)\big(yP(Y=y)\big) After \Big(\sum_{x}xP(X=x)\Big)\Big(\sum_{y}yP(Y=y)\Big)=E[X]E[Y] Conditions: none Rule: finite_sum_rules · Uses: S09.1, finite_sum_rules Leaf basis: finite_sum_rules + distributive + expectation_def Distributivity of finite double sums factors it into the product of two single sums, which are E[X] and E[Y]. So Cov=E[XY]−E[X]E[Y]=0. S09.1 and S09.2 together prove Lemma L_EXY. ## 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 independenceThe 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 enoughIn 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 enoughJ₃ 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-random-variable-independence-01.json)