Finite discrete probability distribution: validating a PMF, event probability, expectation and pushforward

Goal and scope

A random variable X takes the values −1, 0, 1, 2 with masses p(−1)=1/6, p(0)=1/3, p(1)=1/4, p(2)=1/4. (1) First check that p is a valid PMF; (2) find P(X≥1); (3) find E[X]; (4) find the pushforward distribution of Y=X², prove it is again a PMF, find E[Y] and cross-check it against Σx²p(x); (5) decide that two candidates q and r are not PMFs: every mass of q lies between 0 and 1 but the total is not 1, while r sums to 1 but has a negative mass.

Treats only mathematical distributions with a finite range of distinct values and exact rational masses (MKO assumption a1); no claim is made that the distribution comes from a sample estimate, a data fit or a real population (MKO assumption a2). The two lemmas on pushforwards and regrouped sums are proved for any finite range; the other computations concern the given numbers only. Joint distributions and Markov chains are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• frac_rules
• finite_sum_rules
• prob_axioms
• numeric_evaluation

• G1 — The range of X is R_X={−1,0,1,2}, four distinct values; p(−1)=1/6, p(0)=1/3, p(1)=1/4, p(2)=1/4, all exact rationals.
• G2 — g(x)=x² and Y=g(X).
• G3 — Two candidates on the same range: q(−1)=1/2, q(0)=1/3, q(1)=1/4, q(2)=0; r(−1)=1/2, r(0)=2/3, r(1)=−1/6, r(2)=0.
• G4 — These distributions are given mathematical distributions, not estimated or fitted from observed data (MKO assumption a2).

• R_X=\{-1,0,1,2\} — the finite range of X
• p(x) — the probability mass function of X
• P(X\in A) — the probability of the event A
• E[X] — the expectation of X
• g(x)=x^2,\ Y=g(X) — the map used for the pushforward and the new random variable
• p_Y(y) — the pushforward mass of Y

Rules and sources

• 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.
• 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).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• 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.
• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• 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.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• mko_pmf_def · cited — The probability mass function p of a finite discrete random variable assigns a nonnegative probability to each element of its finite value range, and all masses sum to 1. Event probabilities add the corresponding masses; expectation is the mass-weighted sum of values. · mko-finite-discrete-probability-distribution
• event_sum · prerequisite — For a subset A of the range, P(X∈A)=Σ_{x∈A} p(x); values outside A are not added.
• expectation_def · prerequisite — Expectation on a finite range: E[X]=Σ_{x∈R_X} x·p(x).
• pushforward_def · prerequisite — For a function g, Y=g(X) has range R_Y=g(R_X) and pushforward mass p_Y(y)=Σ_{x∈R_X, g(x)=y} p(x): the original masses mapped to the same new value are added.
• sum_over_partition · prerequisite — If a finite set S is the union of pairwise disjoint subsets S_y (y∈Y), then Σ_{x∈S} a_x=Σ_{y∈Y} Σ_{x∈S_y} a_x (associativity and commutativity of finite sums).
• L_pushforward_total · lemma — If p is a PMF on the finite range R_X and g is a function on R_X, then the pushforward mass p_Y is a PMF on R_Y=g(R_X).
• L_regroup · lemma — In the setting of L_pushforward_total, Σ_{y∈R_Y} y·p_Y(y)=Σ_{x∈R_X} g(x)·p(x).

Main derivation

p:R_X\to\mathbb{Q}

p\ \text{is a PMF}\iff \forall x\in R_X:\ p(x)\ge 0\ \land\ \sum_{x\in R_X}p(x)=1

R_X=\{-1,0,1,2\}

|R_X|=4,\ \text{values distinct}

p(-1)=\tfrac16,\ p(0)=\tfrac13,\ p(1)=\tfrac14,\ p(2)=\tfrac14

\forall x\in R_X:\ p(x)\ge 0

\sum_{x\in R_X}p(x)=\tfrac16+\tfrac13+\tfrac14+\tfrac14

1

p\ge 0,\ \sum p=1

p\ \text{is a PMF on } R_X

A=\{x\in R_X\mid x\ge 1\}

A=\{1,2\}

P(X\ge 1)=\sum_{x\in A}p(x)

\tfrac14+\tfrac14=\tfrac12

P(X\in R_X\setminus A)=\tfrac16+\tfrac13

\tfrac12,\quad P(A)+P(R_X\setminus A)=1

E[X]=\sum_{x\in R_X}x\,p(x)

\tfrac{7}{12}

g(-1)=1,\ g(0)=0,\ g(1)=1,\ g(2)=4

R_Y=\{0,1,4\};\ g^{-1}(0)=\{0\},\ g^{-1}(1)=\{-1,1\},\ g^{-1}(4)=\{2\}

p_Y(y)=\sum_{x\in g^{-1}(y)}p(x)

p_Y(0)=\tfrac13,\ p_Y(1)=\tfrac16+\tfrac14=\tfrac{5}{12},\ p_Y(4)=\tfrac14

p_Y\ \text{on } R_Y=\{0,1,4\}

p_Y\ \text{is a PMF};\ \tfrac13+\tfrac{5}{12}+\tfrac14=1

E[Y]=\sum_{y\in R_Y}y\,p_Y(y)

0\cdot\tfrac13+1\cdot\tfrac{5}{12}+4\cdot\tfrac14=\tfrac{17}{12}

\sum_{y\in R_Y}y\,p_Y(y)

\sum_{x\in R_X}x^2p(x)=\tfrac16+0+\tfrac14+1=\tfrac{17}{12}

\sum_{x}q(x)=\tfrac12+\tfrac13+\tfrac14+0

\tfrac{13}{12}\neq 1;\ q\ \text{is not a PMF}

r(1)=-\tfrac16,\ \sum_x r(x)=1

r\ \text{is not a PMF}

Substeps and lemmas

\tfrac16+\tfrac13+\tfrac14+\tfrac14

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

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

\tfrac{12}{12}=1

\sum_{x\in R_X}x\,p(x)

(-1)\cdot\tfrac16+0\cdot\tfrac13+1\cdot\tfrac14+2\cdot\tfrac14

(-1)\cdot\tfrac16+0\cdot\tfrac13+1\cdot\tfrac14+2\cdot\tfrac14

-\tfrac{2}{12}+0+\tfrac{3}{12}+\tfrac{6}{12}=\tfrac{7}{12}

p(x)\ge 0\ \forall x

p_Y(y)=\sum_{x\in g^{-1}(y)}p(x)\ge 0

\sum_{y\in R_Y}p_Y(y)=\sum_{y\in R_Y}\sum_{x\in g^{-1}(y)}p(x)

\sum_{x\in R_X}p(x)=1

\sum_{y\in R_Y}y\sum_{x\in g^{-1}(y)}p(x)

\sum_{y\in R_Y}\sum_{x\in g^{-1}(y)}g(x)p(x)=\sum_{x\in R_X}g(x)p(x)

Reverse audits

• S16 · sufficient_goal_reduction · G3, mko_pmf_def, order_basics — Goal G: r is not a PMF. Sufficient condition H: some mass is negative; H⇒G by the definition. H is read off G3 (N13); G is never used as a premise.
• S15 · sufficient_goal_reduction · G3, mko_pmf_def, numeric_evaluation — Goal G: q is not a PMF. Sufficient condition H: the total is not 1; H⇒G by the definition. H comes from exact summation (N10, N11); G is never used as a premise.
• S14.1 · inverse_equivalence · distributive, eq_replace, sum_over_partition — Distributivity, replacement of equals and summing over a partition are all equations; undoing them in order restores the original.
• S14 · inverse_equivalence · L_regroup, numeric_evaluation — The lemma is an equation and holds both ways; the two independent computations give the same 17/12 (N8, N9).
• S13 · inverse_equivalence · expectation_def, frac_rules, numeric_evaluation — Exact evaluation (N8); both sides are the same number.
• S12.2 · inverse_equivalence · sum_over_partition, function_def — Summing over a partition is an equation and holds both ways; the key condition, each x in exactly one block, holds because g is a function.
• S12.1 · premise_audit · pushforward_def, order_basics — Only nonnegativity of p is used; neither p_Y(y)>0 nor any converse is claimed.
• S12 · premise_audit · S05, L_pushforward_total — The lemma needs p to be a PMF (S05) and g to be a function (G2); the numeric check N7 is a consistency check and does not replace the lemma.
• S11 · inverse_equivalence · pushforward_def, frac_rules, numeric_evaluation — Each p_Y(y) is an exact evaluation of its defining sum (N6), so the step is two-way.
• S10 · premise_audit · image_preimage_def, G2 — The three preimages are pairwise disjoint with union R_X, the partition property used in S12.2; g is not injective, so values of Y cannot be matched one-to-one with values of X.
• S09.2 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational arithmetic, independently recomputable.
• S09.1 · inverse_equivalence · finite_sum_rules — Expanding a finite sum and folding it back are inverse moves.
• S09 · inverse_equivalence · expectation_def, numeric_evaluation — Exact evaluation (N5); both sides are the same number.
• S08 · premise_audit · S07, event_sum, prob_axioms — This is a consistency check, not a new inference; it confirms that S07 neither missed nor double-counted a mass.
• S07 · inverse_equivalence · event_sum, frac_rules, numeric_evaluation — Exact evaluation; both sides are the same number (N3). The prerequisite is S05, which confirmed that p is a PMF.
• S06 · inverse_equivalence · set_builder — Membership in set-builder notation is two-way, and all four values were tested.
• S05 · sufficient_goal_reduction · S03, S04, mko_pmf_def — Goal G: p is a PMF. Sufficient condition H: nonnegative with total 1; H⇒G by the definition. H is proved forwards in S03 and S04; G is never used as a premise.
• S04.2 · inverse_equivalence · frac_rules, numeric_evaluation — Integer addition and the fraction rule are equations, independently recomputable (N2).
• S04.1 · inverse_equivalence · frac_rules — Reducing the fractions is the backward move, given the multipliers are nonzero.
• S04 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational evaluation; both sides are the same number (N1), so the step is two-way.
• S03 · premise_audit · G1, order_basics — Nonnegativity is only one of the PMF conditions; it does not give total 1.
• S02 · premise_audit · G1, finite_counting_basics — Only the shape of the range is checked; nothing is said about the sizes of the masses.
• S01 · premise_audit · mko_pmf_def, prob_axioms — This step only states the PMF conditions and derives no new fact; the two conditions match the axioms of nonnegativity and total probability 1.

Error controls and negative controls

Masses between 0 and 1 do not make the total 1

The MKO names the mistake of ignoring the total because every mass lies between 0 and 1. Every mass of q lies in [0,1], yet the total is 13/12; r sums to 1 yet has a negative mass. Both conditions must be checked, adding exact fractions rather than decimal approximations.

A theoretical PMF is not a data fit

Another mistake identified in the MKO is passing off a theoretical PMF as the result of a data fit. The masses 1/6, 1/3, 1/4, 1/4 here are a given mathematical distribution (G4) with no observed data; saying 'exactly 2 of 12 trials gave −1' or 'this distribution was estimated from a sample' goes beyond anything this guide supports. The pushforward is likewise an exact mathematical transformation.

A pushforward merges masses with the same image

Both −1 and 1 map to 1, so p_Y(1)=1/6+1/4=5/12. Taking only p(1)=1/4, or listing the value 1 twice, breaks the total of 1 or the distinctness of values. Also E[X²]=17/12 differs from (E[X])²=49/144: the expectation of a square is in general not the square of the expectation.

• Every mass of q lies between 0 and 1, so q is a PMF → reject — q sums to 13/12≠1.
• r sums to 1, so r is a PMF → reject — r(1)=−1/6<0 violates nonnegativity.
• P(X≥1)=p(2)=1/4, since only 2 is greater than 1 → reject — The event is x≥1, which includes 1; P(X≥1)=1/4+1/4=1/2.
• E[X²]=(E[X])²=49/144 → reject — E[X²]=17/12, which differs from 49/144.
• p_Y(1)=p(1)=1/4, because g(1)=1 → reject — g(−1)=1 maps to 1 as well and must be added: p_Y(1)=5/12.

Result and limitations

p is nonnegative with total exactly 1, so it is a PMF. P(X≥1)=p(1)+p(2)=1/2 and E[X]=7/12. The pushforward of Y=X² is p_Y(0)=1/3, p_Y(1)=5/12, p_Y(4)=1/4, again a PMF (proved for any finite range), and E[Y]=17/12, agreeing with Σx²p(x). q has every mass between 0 and 1 but total 13/12, and r sums to 1 but r(1)=−1/6, so neither is a PMF.

• Lemmas L_pushforward_total and L_regroup are proved for finite ranges only; countable or continuous cases need series or integrals and are not treated here.
• Joint distributions, discrete random processes and finite Markov chains (the MKO's formal next) are not treated, and no statistical inference is made.

Verification and source binding

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

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

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