Random variables on a finite sample space: range, preimage events and point probabilities

Goal and scope

S={1,2,3,4}, event family F=𝒫(S), weights w₁=1/2, w₂=1/4, w₃=1/8, w₄=1/8. The random variable X:S→ℝ is given by the table X(1)=1, X(2)=0, X(3)=1, X(4)=4 (that is, X(s)=(s−2)²). Find the range of X, the preimage events {X=1}, {X≥1} and {X∈{2,3}}, and the point probability P(X=t) of each value, and prove that these point probabilities sum to 1.

Stays inside the MKO's finite slice: S nonempty and finite, F the full power set, X a total function, weights explicit rationals. The range and preimage events read only the function data and do not use the weights; point probabilities use the separately given weights (MKO assumption a2). The lemma building a probability law from weights is proved here; general measurable spaces, continuous densities and general representations of distributions are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• function_def
• image_preimage_def
• set_builder
• prob_axioms
• finite_sum_rules
• numeric_evaluation

• G1 — S={1,2,3,4} is nonempty and finite, and the event family is the full power set F=𝒫(S) (MKO assumption a1).
• G2 — Function data: X(1)=1, X(2)=0, X(3)=1, X(4)=4.
• G3 — For point-probability questions the weights are given separately: w₁=1/2, w₂=1/4, w₃=1/8, w₄=1/8, and P(E)=Σ_{s∈E} w_s for E⊆S.

• S=\{1,2,3,4\} — the sample space (elementary outcomes)
• w_s — the weight P({s}) of outcome s
• X:S\to\mathbb{R} — the random variable, i.e. the whole function table
• X(S) — the range of X (duplicates removed)
• \{X\in T\} — the preimage event {s∈S ∣ X(s)∈T}

Rules and sources

• 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.
• 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.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• 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).
• 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.
• 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.
• 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.
• 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.
• 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.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_rv_def · cited — On a nonempty finite sample space S with event family F=𝒫(S) and a valid probability law P, a real random variable is a total function X:S→R. For any subset T of ℝ, the preimage {s∈S:X(s)∈T} is an event. P(X=t) sums the weights of all outcomes with X(s)=t. · mko-random-variable
• L_weight_law · lemma — Let S be finite with F=𝒫(S), and let w_s≥0 for all s with Σ_{s∈S} w_s=1. Then P(E)=Σ_{s∈E} w_s satisfies: P(E)≥0; P(S)=1; and P(E₁∪E₂)=P(E₁)+P(E₂) whenever E₁∩E₂=∅.
• L_level_partition · lemma — For a total function X:S→ℝ with range R=X(S), the level sets {X=t} (t∈R) are pairwise disjoint and their union is S.

Main derivation

w_1=\tfrac12,\ w_2=\tfrac14,\ w_3=\tfrac18,\ w_4=\tfrac18

w_s\ge 0,\ \sum_{s\in S}w_s=1

w_s\ge0,\ \sum_{s}w_s=1

P(E)=\sum_{s\in E}w_s\ \text{is a valid probability law on}\ \mathcal{P}(S)

X(1)=1,\ X(2)=0,\ X(3)=1,\ X(4)=4

X:S\to\mathbb{R}\ \text{total function}

X(S)=\{X(1),X(2),X(3),X(4)\}

X(S)=\{0,1,4\}

\{X=1\}=\{s\in S\mid X(s)=1\}

\{1,3\}\in\mathcal{P}(S)

P(X=1)=P(\{1,3\})

w_1+w_3=\tfrac12+\tfrac18=\tfrac58

\{X=0\},\ \{X=4\}

\{2\},\ \{4\};\ P(X=0)=\tfrac14,\ P(X=4)=\tfrac18

\{X=0\},\ \{X=1\},\ \{X=4\}

\text{pairwise disjoint},\ \{2\}\cup\{1,3\}\cup\{4\}=S

P(X=0)+P(X=1)+P(X=4)

P(S)=1

\{X\ge 1\}=X^{-1}([1,\infty))

\{1,3,4\},\ P=\tfrac12+\tfrac18+\tfrac18=\tfrac34

\{X\ge1\}=S\setminus\{X=0\}

P(X\ge1)=1-\tfrac14=\tfrac34

X^{-1}(\{2,3\})

\varnothing\in\mathcal{P}(S),\ P(\varnothing)=0

\text{S04 to S12}

X(S)=\{0,1,4\};\ P(X=0)=\tfrac14,\ P(X=1)=\tfrac58,\ P(X=4)=\tfrac18;\ \textstyle\sum=1

Substeps and lemmas

w_s\ge 0\ \ (s\in E)

P(E)=\sum_{s\in E}w_s\ge 0

P(S)

\sum_{s\in S}w_s=1

E_1\cap E_2=\varnothing

\sum_{s\in E_1\cup E_2}w_s=\sum_{s\in E_1}w_s+\sum_{s\in E_2}w_s

s\in\{X=t\}\cap\{X=t'\}

t=X(s)=t'

s\in S

s\in\{X=X(s)\},\ X(s)\in X(S)

Reverse audits

• S13 · sufficient_goal_reduction · S04, S05, S06, S07, S09, S10, S12, and_intro_elim — Goal G is the full list of results requested in the goal; the sufficient condition H is the conjunction of the step results, all proved forwards, and H⇒G uses only conjunction introduction.
• S12 · inverse_equivalence · image_preimage_def, set_builder, prob_axioms — All four outcomes were checked and none qualifies, so the sets are equal; P(∅)=0 follows from the definition (empty sum).
• S11 · inverse_equivalence · prob_axioms, S02, set_operations_def — The complement rule follows from additivity and P(S)=1 and is an equation, usable both ways; the two computations give the same value.
• S10 · inverse_equivalence · image_preimage_def, set_builder, S02 — All four outcomes were decided, so the sets are equal; the probability is summed by definition and both sides have the same value.
• S09 · premise_audit · S02, S08, L_weight_law — The second use of additivity needs ({2}∪{1,3})∩{4}=∅, which follows from pairwise disjointness. The numeric check agrees with the general argument, but the conclusion is proved from the partition in S08 and additivity.
• S08.2 · premise_audit · function_def, set_extensionality, image_preimage_def — Totality puts every outcome in a level set. Omitting a positive-weight outcome makes the total mass of the listed level sets less than 1. Omitting only a zero-weight outcome can leave total mass 1, but the table still is not a total function on S. Here all weights are positive, so omitting any outcome loses positive mass.
• S08.1 · premise_audit · function_def, eq_refl_symm_trans — Only single-valuedness and symmetry and transitivity of equality are used.
• S08 · premise_audit · L_level_partition, S04 — The lemma needs X to be total (every outcome has a value) and single-valued (no outcome lies in two level sets); both come from S03.
• S07 · inverse_equivalence · image_preimage_def, set_extensionality, S02 — All four outcomes were decided, so the sets are equal; the probabilities are read directly from the definition, so the step holds both ways.
• S06 · inverse_equivalence · S02, S05, numeric_evaluation — By the definition of P both sides name the same number, and the exact arithmetic can be checked backwards: 5/8−1/8=1/2=w₁.
• S05 · inverse_equivalence · image_preimage_def, set_builder, set_extensionality — All four elements of S were decided; the listed elements satisfy the condition and the others do not, so the two sets are equal.
• S04 · inverse_equivalence · image_preimage_def, set_extensionality — Both sides have the same elements (extensionality), and listing an element twice does not change the set, so the step holds both ways.
• S03 · premise_audit · G2, function_def, mko_rv_def — Only the two requirements of a function are checked; the weights are not used.
• S02.3 · premise_audit · finite_sum_rules, set_operations_def — Disjointness is the sufficient hypothesis used by the lemma, counting every outcome once. If the overlap has positive mass, the right side counts that mass twice and the equality fails; an overlap consisting only of zero-weight outcomes changes no value. All weights in this worked example are positive, so every overlap here does duplicate mass.
• S02.2 · premise_audit · S01, def_unfold — This unfolds the definition and cites the value from S01; if the weights did not sum to 1, this step would fail.
• S02.1 · premise_audit · order_basics, finite_sum_rules — This step proves only that nonnegative terms have a nonnegative finite sum; it does not claim the converse that a nonnegative sum forces every term to be nonnegative. The fact that nonnegative terms summing to zero are all zero is a separate statement, not that converse, and is not used here.
• S02 · premise_audit · S01, L_weight_law, G1 — It needs nonnegative weights summing exactly to 1 (S01) and a finite S so that the sums make sense. The converse (every probability law comes from weights) also holds on a finite full power set, but it is neither needed nor claimed here.
• S01 · premise_audit · G3, numeric_evaluation — This is exact rational arithmetic and can be recomputed independently; the conclusion is that the weights are valid, and X is not involved.

Error controls and negative controls

A random variable is not the result of one draw

One misconception identified in the MKO is taking a random variable for the number obtained in one draw. X is the whole table s↦X(s); 'X=1' names the event {1,3}, a set of outcomes, and P(X=1)=5/8 is the probability of that event. Getting 1 in some trial is one observation, not X itself.

The size of the range is not a probability

The range has 3 values, but that does not make each value have probability 1/3. P(X=1)=5/8, P(X=0)=1/4, P(X=4)=1/8; probabilities come only from the weights. Without given weights one may not assume equal likelihood either (a2).

Add the weights of every outcome with the same value

X(1)=X(3)=1, so P(X=1) must be w₁+w₃=5/8. Stopping at the first outcome found gives 1/2 and misses outcome 3. The partition argument of S08 guarantees that every outcome is counted for exactly one value.

• X takes three values, so P(X=1)=1/3 → reject — Point probabilities come from the weights: P(X=1)=w₁+w₃=5/8≠1/3.
• X(1)=1 and w₁=1/2, so P(X=1)=1/2 → reject — Outcome 3 also has X(3)=1, so w₃=1/8 must be added, giving 5/8.
• Two of the four outcomes have value 1, so P(X=1)=2/4 → reject — This assumes equal likelihood, but the given weights are not equal; with the given weights P(X=1)=5/8.
• {s: X(s)∈{2,3}} is empty, so it is not an event → reject — ∅∈𝒫(S)=F, so it is an event, with probability 0.

Result and limitations

X is a total function S→ℝ with range {0,1,4} (three values while S has four outcomes). The preimage events {X=1}={1,3}, {X≥1}={1,3,4} and {X∈{2,3}}=∅ are all events. The point probabilities are P(X=0)=1/4, P(X=1)=w₁+w₃=5/8 and P(X=4)=1/8, and since the level sets partition S they sum to 1; P(X≥1)=3/4, confirmed by the complement.

• This guide treats only finite S with the full power set as event family; in general measurable spaces, whether preimages are events requires measurability, which is a separate obligation.
• The distribution formed by the point probabilities (the pushforward) is described in S09 only by its total 1 and is not formally defined as a new probability law.

Verification and source binding

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

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

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