# Random variables on a finite sample space: range, preimage events and point probabilities [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-random-variable/) 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-01 · production-20261019-adopted-96 ## 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 uv holds; u0 give uwvw. - 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 S01 · impliesBefore w_1=\tfrac12,\ w_2=\tfrac14,\ w_3=\tfrac18,\ w_4=\tfrac18 After w_s\ge 0,\ \sum_{s\in S}w_s=1 Conditions: none Rule: numeric_evaluation · Uses: G3 Leaf basis: numeric_evaluation + frac_rules First validate the weights: all four are positive rationals, hence nonnegative; their sum is 1/2+1/4+1/8+1/8=4/8+2/8+1/8+1/8=8/8=1. This is the precondition for using the probability law later. S02 · impliesBefore w_s\ge0,\ \sum_{s}w_s=1 After P(E)=\sum_{s\in E}w_s\ \text{is a valid probability law on}\ \mathcal{P}(S) Conditions: S\ \text{finite} Rule: L_weight_law · Uses: S01, G1 Leaf basis: prob_axioms + finite_sum_rules + order_basics By Lemma L_weight_law, the P defined from valid weights satisfies the probability axioms (nonnegativity, total probability 1, additivity for disjoint events). Since F=𝒫(S), every subset E is an event and P(E) is defined. The lemma is proved in S02.1 to S02.3. S03 · definitionBefore X(1)=1,\ X(2)=0,\ X(3)=1,\ X(4)=4 After X:S\to\mathbb{R}\ \text{total function} Conditions: none Rule: mko_rv_def · Uses: G1, G2 Leaf basis: function_def + mko_rv_def Each of the four outcomes has exactly one real value, so X is a total function S→ℝ, which is the MKO's definition of a random variable. X means the whole table s↦X(s), not a number obtained in one trial. S04 · equivalentBefore X(S)=\{X(1),X(2),X(3),X(4)\} After X(S)=\{0,1,4\} Conditions: none Rule: image_preimage_def · Uses: S03 Leaf basis: image_preimage_def + set_extensionality The range is the set of all values: {1,0,1,4}. A set does not count an element twice, so X(S)={0,1,4}, with only 3 values while S has 4 outcomes; this is because X(1)=X(3)=1. S05 · equivalentBefore \{X=1\}=\{s\in S\mid X(s)=1\} After \{1,3\}\in\mathcal{P}(S) Conditions: none Rule: image_preimage_def · Uses: S03, G1 Leaf basis: image_preimage_def + set_builder + set_extensionality Check the four outcomes one by one: X(1)=1 yes, X(2)=0 no, X(3)=1 yes, X(4)=4 no, so the preimage {X=1}={1,3}. It is a subset of S and F=𝒫(S), so it is an event. This step reads only the function data. S06 · equivalentBefore P(X=1)=P(\{1,3\}) After w_1+w_3=\tfrac12+\tfrac18=\tfrac58 Conditions: none Rule: mko_rv_def · Uses: S02, S05 Leaf basis: mko_rv_def + def_unfold + numeric_evaluation The point probability is the sum of the weights of all outcomes with X(s)=1: P({1,3})=w₁+w₃=1/2+1/8=5/8. Both outcomes must be added; counting only w₁ would give the wrong value 1/2. S07 · equivalentBefore \{X=0\},\ \{X=4\} After \{2\},\ \{4\};\ P(X=0)=\tfrac14,\ P(X=4)=\tfrac18 Conditions: none Rule: image_preimage_def · Uses: S02, S03 Leaf basis: image_preimage_def + set_extensionality + def_unfold Scan in the same way: only X(2)=0 and only X(4)=4, so {X=0}={2} and {X=4}={4}, with point probabilities w₂=1/4 and w₄=1/8. S08 · impliesBefore \{X=0\},\ \{X=1\},\ \{X=4\} After \text{pairwise disjoint},\ \{2\}\cup\{1,3\}\cup\{4\}=S Conditions: none Rule: L_level_partition · Uses: S03, S04 Leaf basis: function_def + set_operations_def By Lemma L_level_partition, the level sets of the values in the range form a partition of S: pairwise disjoint with union S. The proof is in S08.1 and S08.2; in this example one sees directly that {2}, {1,3}, {4} are disjoint and together give {1,2,3,4}. S09 · impliesBefore P(X=0)+P(X=1)+P(X=4) After P(S)=1 Conditions: none Rule: L_weight_law · Uses: S02, S06, S07, S08 Leaf basis: prob_axioms + set_operations_def + numeric_evaluation The three level sets are pairwise disjoint (S08), so two-set additivity applied twice gives P({2}∪{1,3}∪{4})=P({2}∪{1,3})+P({4})=P({2})+P({1,3})+P({4}), and the left side is P(S)=1. Numerically: 1/4+5/8+1/8=1. So the point probabilities add up to exactly 1. S10 · equivalentBefore \{X\ge 1\}=X^{-1}([1,\infty)) After \{1,3,4\},\ P=\tfrac12+\tfrac18+\tfrac18=\tfrac34 Conditions: none Rule: image_preimage_def · Uses: S02, S03 Leaf basis: image_preimage_def + set_builder + numeric_evaluation Take T=[1,∞). Filter the outcomes by X(s)≥1: X(1)=1, X(3)=1 and X(4)=4 qualify and X(2)=0 does not, so {X≥1}={1,3,4} with probability w₁+w₃+w₄=3/4. S11 · equivalentBefore \{X\ge1\}=S\setminus\{X=0\} After P(X\ge1)=1-\tfrac14=\tfrac34 Conditions: none Rule: prob_axioms · Uses: S07, S10, S02 Leaf basis: prob_axioms + set_operations_def + numeric_evaluation Cross-check: only the value 0 in the range is below 1, so {X≥1} is the complement of {X=0}={2}. By the complement rule P(Eᶜ)=1−P(E), this gives 1−1/4=3/4, agreeing with the direct sum in S10. S12 · equivalentBefore X^{-1}(\{2,3\}) After \varnothing\in\mathcal{P}(S),\ P(\varnothing)=0 Conditions: none Rule: image_preimage_def · Uses: S03, G1 Leaf basis: image_preimage_def + set_builder + prob_axioms Take T={2,3}: no outcome has value 2 or 3, so the preimage is empty. The empty set is also a subset of S, belongs to F=𝒫(S), and is an event, with probability the empty sum 0. This shows that the MKO's 'the preimage of any subset of ℝ is an event' includes the empty case. S13 · impliesBefore \text{S04 to S12} After X(S)=\{0,1,4\};\ P(X=0)=\tfrac14,\ P(X=1)=\tfrac58,\ P(X=4)=\tfrac18;\ \textstyle\sum=1 Conditions: none Rule: and_intro_elim · Uses: S04, S05, S06, S07, S09, S10, S12 Leaf basis: and_intro_elim Summary: range {0,1,4}; preimage events {X=1}={1,3}, {X≥1}={1,3,4}, {X∈{2,3}}=∅; point probabilities 1/4, 5/8, 1/8, summing to 1. The range and events use only the function data; only the point probabilities use the weights. ## Substeps and lemmas S02.1 · impliesBefore w_s\ge 0\ \ (s\in E) After P(E)=\sum_{s\in E}w_s\ge 0 Conditions: none Rule: order_basics · Uses: S01, order_basics Leaf basis: order_basics + finite_sum_rules Adding nonnegative numbers stays nonnegative (from u≥0 and v≥0 we get u+v≥v≥0, adding one term at a time); the empty sum is 0, so P(∅)=0≥0 as well. S02.2 · impliesBefore P(S) After \sum_{s\in S}w_s=1 Conditions: none Rule: def_unfold · Uses: S01 Leaf basis: def_unfold + numeric_evaluation By the definition of P, P(S) is the sum of all weights, which S01 computed to be 1. S02.3 · impliesBefore E_1\cap E_2=\varnothing After \sum_{s\in E_1\cup E_2}w_s=\sum_{s\in E_1}w_s+\sum_{s\in E_2}w_s Conditions: E_1\cap E_2=\varnothing Rule: finite_sum_rules · Uses: finite_sum_rules, set_operations_def Leaf basis: finite_sum_rules + set_operations_def Each outcome of E₁∪E₂ lies in exactly one of E₁, E₂ (they are disjoint), so the finite sum on the left can be regrouped into two groups, counting each weight exactly once. S02.1 to S02.3 together prove Lemma L_weight_law. S08.1 · impliesBefore s\in\{X=t\}\cap\{X=t'\} After t=X(s)=t' Conditions: none Rule: function_def · Uses: S03, function_def Leaf basis: function_def + eq_refl_symm_trans If s lies in both {X=t} and {X=t′}, then X(s)=t and X(s)=t′; a function has only one value at s, so t=t′. Hence level sets of different values have no common element. S08.2 · impliesBefore s\in S After s\in\{X=X(s)\},\ X(s)\in X(S) Conditions: none Rule: function_def · Uses: S03, function_def Leaf basis: function_def + set_extensionality + image_preimage_def X is total, so every s∈S has a value X(s), which lies in the range, and s lies in the level set of that value. So the union of the level sets contains S; conversely every level set is a subset of S, so the union is exactly S. S08.1 and S08.2 together prove Lemma L_level_partition. ## 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 drawOne 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 probabilityThe 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 valueX(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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-random-variable-01.json)