Finite joint distribution: validating a joint mass table and aggregating marginals and events from one joint law

Goal and scope

Given the support S={(0,0),(0,1),(1,0),(1,1),(2,1)} with masses p(0,0)=1/6, p(0,1)=1/3, p(1,0)=1/4, p(1,1)=1/12, p(2,1)=1/6, verify that (S,p) is a two-dimensional finite joint distribution; from this one joint law compute the marginals of X and Y, the rectangle event P(X∈{1,2}, Y=1) and the single-pair mass P(X=2, Y=0); finally construct a different joint law with the same marginals, showing that two marginals do not in general determine the joint distribution.

Stays inside the MKO: a finite joint law whose support consists of distinct integer pairs with exact rational masses (assumption a1), treated as a mathematical model, not as data fitting or a continuous density (assumption a2). The guide validates one concrete table and proves the product-law lemma in general; it does not treat independence, covariance or conditional expectation (later nodes of the MKO), and does not change the canonical MKO or its English edition.

Givens and symbols

• cartesian_product_def
• frac_rules
• finite_sum_rules
• order_basics
• numeric_evaluation
• finite_sum_regroup

• G1 — Table: S={(0,0),(0,1),(1,0),(1,1),(2,1)} with p(0,0)=1/6, p(0,1)=1/3, p(1,0)=1/4, p(1,1)=1/12, p(2,1)=1/6, all exact rationals.
• G2 — X and Y are the two coordinates of the same pair: at (x,y), X=x and Y=y. Every event probability is aggregated from this one table.
• G3 — A={1,2} and B={1}.

• S — support: the listed distinct integer pairs
• p(x,y) — exact mass of the pair (x,y); pairs outside S have mass 0
• X,\ Y — coordinate projections: X=x and Y=y at the pair (x,y)
• p_X,\ p_Y — marginal masses of X and of Y
• A\times B — rectangle event: first coordinate in A and second coordinate in B
• Q — the other joint law formed by multiplying the two marginals

Rules and sources

• 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.
• 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.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• 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).
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• 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_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
• joint_event_sum · prerequisite — A finite joint law (S,p) gives event probabilities: for C⊆ℤ², P((X,Y)∈C)=Σ_{s∈S∩C} p(s); pairs not in S have mass 0. This is the additivity of the probability axioms over disjoint single-pair events.
• 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), the probabilities of the events {x}×ℤ and ℤ×{y}.
• finite_sum_regroup · prerequisite — Regrouping a finite sum: if a finite set S is split into pairwise disjoint pieces S_1, S_2 and so on (each element in exactly one piece), then Σ_{s∈S} f(s) equals the total of the sums over the pieces.
• L_product_law · lemma — Let p_X on a finite integer set S_X and p_Y on a finite integer set S_Y be nonnegative exact rational masses, each summing exactly to 1. Then Q(x,y)=p_X(x)p_Y(y) on S_X×S_Y is a finite joint law whose two marginals are exactly p_X and p_Y.

Main derivation

\text{table }(S,p)

\text{(i) distinct pairs, (ii) } p(s)\ge 0 \text{ exact, (iii) } \sum_{s\in S}p(s)=1

(0,0),\ (0,1),\ (1,0),\ (1,1),\ (2,1)

\text{five pairwise distinct pairs}

p=\tfrac16,\ \tfrac13,\ \tfrac14,\ \tfrac1{12},\ \tfrac16

p(s)>0\ \text{for every } s\in S

\sum_{s\in S}p(s)=\tfrac16+\tfrac13+\tfrac14+\tfrac1{12}+\tfrac16

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

\text{(i), (ii), (iii) checked}

(S,p)\ \text{is a finite joint law}

C\subseteq\mathbb{Z}^2

P((X,Y)\in C)=\sum_{s\in S\cap C}p(s)

p_X(x)=\sum_{y:(x,y)\in S}p(x,y)

p_X(0)=\tfrac12,\ p_X(1)=\tfrac13,\ p_X(2)=\tfrac16

\sum_{x}p_X(x)=\sum_{x}\sum_{y:(x,y)\in S}p(x,y)

\sum_{x}p_X(x)=\sum_{s\in S}p(s)=1

p_Y(y)=\sum_{x:(x,y)\in S}p(x,y)

p_Y(0)=\tfrac{5}{12},\ p_Y(1)=\tfrac{7}{12}

P(X\in A,\ Y\in B)=P((X,Y)\in A\times B)

P(X\in A,\ Y\in B)=\tfrac14

P(X\in A)\,P(Y\in B)=\left(\tfrac13+\tfrac16\right)\tfrac{7}{12}

\tfrac{7}{24}\neq\tfrac{6}{24}=P(X\in A,\ Y\in B)

P(X=2,\ Y=0)

0\neq\tfrac{5}{72}=p_X(2)\,p_Y(0)

p_X\ \text{on}\ \{0,1,2\},\ p_Y\ \text{on}\ \{0,1\}

Q(x,y)=p_X(x)\,p_Y(y)\ \text{is a finite joint law with marginals}\ p_X,\ p_Y

J(2,0)=0,\ Q(2,0)=\tfrac{5}{72}

J\neq Q\ \text{while}\ J,\ Q\ \text{have the same marginals}

Substeps and lemmas

\tfrac16+\tfrac13+\tfrac14+\tfrac1{12}+\tfrac16

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{1}{12}+\tfrac{2}{12}

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{1}{12}+\tfrac{2}{12}

\tfrac{12}{12}=1

S\cap(\{x\}\times\mathbb{Z}),\ x=0,1,2

\{(0,0),(0,1)\},\ \{(1,0),(1,1)\},\ \{(2,1)\}

p(0,0)+p(0,1),\ p(1,0)+p(1,1),\ p(2,1)

\tfrac12,\ \tfrac13,\ \tfrac16

S\cap(A\times B)

\{(1,1),\ (2,1)\}

p(1,1)+p(2,1)

\tfrac{1}{12}+\tfrac{2}{12}=\tfrac14

Q(x,y)=p_X(x)\,p_Y(y),\ (x,y)\in S_X\times S_Y

\text{distinct pairs},\ Q(x,y)\ge 0\ \text{exact rational}

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

\sum_{x\in S_X}p_X(x)\cdot\sum_{y\in S_Y}p_Y(y)=1\cdot 1=1

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

p_X(x)\sum_{y}p_Y(y)=p_X(x),\ p_Y(y)\sum_{x}p_X(x)=p_Y(y)

Reverse audits

• S14 · sufficient_goal_reduction · S12, S13, function_def, exists_intro — Goal G: marginals do not in general determine the joint law. Sufficient condition H: two different joint laws with the same marginals exist; H⇒G because one counterexample refutes a universal claim. H is constructed forwards in S12 and S13; G is never used as a premise.
• S13.3 · inverse_equivalence · finite_sum_rules, mul_one — Σ c·a_i=c·Σ a_i and multiplying by 1 are rewrites of equal values, so the step is two-way. This sub-step does not use L_product_law.
• S13.2 · inverse_equivalence · distributive, finite_sum_rules, finite_sum_regroup — Pulling out a constant factor and regrouping a finite sum are rewrites of equal values and can be reversed; the conditions used are that each marginal totals 1. This sub-step does not use L_product_law.
• S13.1 · premise_audit · cartesian_product_def, order_basics — Nonnegative times nonnegative is nonnegative; no converse is claimed. This sub-step does not use L_product_law.
• S13 · premise_audit · S07, S08, S09, L_product_law — The lemma needs each marginal to be nonnegative with total 1, which S07 to S09 confirm. The step only constructs Q and does not claim that Q equals the original joint law.
• S12 · premise_audit · S06, S07, S09, G1 — It needs the support list to be complete (assumption a1): the mass of (2,0) is 0 precisely because (2,0) is not listed.
• S11 · premise_audit · S07, S09, S10, numeric_evaluation — It only compares two exact numbers; it says they differ for this table, not for every joint law (for the product law Q they agree).
• S10.2 · inverse_equivalence · frac_rules, numeric_evaluation — An exact rewrite of equal fractions, two-way.
• S10.1 · inverse_equivalence · cartesian_product_def, set_extensionality — All five pairs of S were decided, so both sides are the same set and the step holds both ways.
• S10 · premise_audit · S06, G3, cartesian_product_def — It needs 'at the same time': (x,y)∈A×B exactly when x∈A and y∈B. Using 'or' instead gives a different event with a different value.
• S09 · premise_audit · S06, marginal_def — It requires the list for each y to be complete: S has exactly two pairs with second coordinate 0 and exactly three with 1, five in all, matching the size of S.
• S08 · inverse_equivalence · finite_sum_regroup, S07.1 — Regrouping changes only how the finite sum is grouped, not its value; both sides are the same number, so the step is two-way. The condition is the partition: each pair is counted exactly once.
• S07.2 · inverse_equivalence · frac_rules, numeric_evaluation — Exact fraction arithmetic rewrites equal values, so the two sides are the same three rationals.
• S07.1 · inverse_equivalence · set_operations_def, set_extensionality — All five pairs were decided one by one, so both sides are the same sets element by element, and the step holds both ways.
• S07 · premise_audit · S06, marginal_def — It requires the listed pairs to be the complete intersection of S with {x}×ℤ; missing one pair gives a wrong marginal. No converse is claimed: the individual masses cannot be recovered from the marginal.
• S06 · premise_audit · S05, joint_event_sum, prob_axioms — It needs S05: if the masses did not sum to 1 or some mass were negative, the numbers obtained would not be probabilities. The step applies a definition and derives nothing else.
• S05 · sufficient_goal_reduction · S01, S02, S03, S04, and_intro_elim — Goal G: (S,p) is a finite joint law. Sufficient condition H: requirements (i), (ii) and (iii) all hold; H⇒G by the definition. H is proved forwards in S02 to S04; G is never used as a premise.
• S04.2 · inverse_equivalence · frac_rules, numeric_evaluation — Integer addition and combining over a common denominator are rewrites of equal values and can be undone step by step.
• S04.1 · inverse_equivalence · frac_rules — Backward, cancel the same nonzero factor k to return to the original fractions; the two sides agree term by term.
• S04 · inverse_equivalence · frac_rules, numeric_evaluation — Both sides name the same rational number, and S04.2 can be read backwards to the form in S04.1, so the step holds both ways.
• S03 · premise_audit · G1, order_basics — It needs only the sign of each of the five masses; positive implies nonnegative, and no converse is claimed.
• S02 · premise_audit · G1, cartesian_product_def — The grouping covers all 10 comparisons with none missed; one differing coordinate suffices for two pairs to differ, and no converse is needed.
• S01 · premise_audit · G1, mko_joint_def — This step only unfolds the definition and lists the three obligations; it derives no new fact.

Error controls and negative controls

Two marginal tables are not a joint law

The common mistake named by the MKO is to take two marginal tables as the joint distribution. Here J and Q have exactly the same marginals (1/2, 1/3, 1/6 and 5/12, 7/12), yet their masses at (2,0) are 0 and 5/72 (S14). Marginals are aggregates of the joint table, and aggregation loses information, so they cannot be inverted.

The total must be exactly 1

Replacing the masses by 0.166, 0.333, 0.25, 0.083 and 0.166 still gives exact rational numbers when the finite decimals are read literally. However, their total is 0.998 rather than 1, so the table fails requirement (iii). If intended merely as truncated approximations, they must not be treated as the original exact masses. S04 uses the original fractions and obtains exactly 12/12=1.

A rectangle event needs both coordinates at once

P(X∈A, Y∈B) is the event that both coordinate conditions hold at once, here 1/4. Computing P(X∈A)+P(Y∈B)−P(X∈A, Y∈B)=1/2+7/12−1/4=5/6 gives the 'or' event; computing P(X∈A)P(Y∈B)=7/24 treats the marginals as the joint law. Neither is the rectangle probability (S10, S11).

• Multiplying the marginals gives the joint law: P(X=x,Y=y)=p_X(x)p_Y(y) holds for this table → reject — At (2,0) the mass of J is 0 while p_X(2)p_Y(0)=5/72.
• The table with masses 0.166, 0.333, 0.25, 0.083, 0.166 is a valid finite joint distribution → reject — The total is 0.998≠1; the MKO requires the total to be exactly 1.
• P(X∈{1,2}, Y=1)=P(X∈{1,2})·P(Y=1)=7/24 → reject — Aggregating the joint law gives 1/12+1/6=1/4=6/24≠7/24.
• Listing (0,1) twice with mass 1/6 each is still a joint table in the sense of the MKO → reject — The MKO requires the support to list distinct pairs; a repeated pair must be merged into one row (mass 1/3) before the table qualifies.

Result and limitations

(S,p) is a valid two-dimensional finite joint distribution (distinct pairs, positive exact rational masses, total exactly 1). From this one joint law, p_X(0)=1/2, p_X(1)=1/3, p_X(2)=1/6, p_Y(0)=5/12, p_Y(1)=7/12, the rectangle event P(X∈{1,2}, Y=1)=1/4 and the single-pair mass P(X=2,Y=0)=0. The product law Q=p_X p_Y has the same marginals but Q(2,0)=5/72≠0, so two marginals do not determine the joint distribution.

• Regrouping of finite sums (finite_sum_regroup) and joint_event_sum are premises of this guide; they are not derived here from more basic axioms.
• N14 and N15 check the numbers in the error controls and are valid for those numbers only.

Verification and source binding

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

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

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