# Sample space: two observation scales for two coin tosses, and outcomes that are not equally likely [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-sample-space/) 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-sample-space-01 · production-20261019-adopted-96 ## Goal and scope Random experiment: toss a coin twice. (1) Recording the results in order, write the sample space S, and prove that it contains every possible elementary outcome and has exactly 4 elements; (2) recording only the number of heads, write the sample space S′={0,1,2}; (3) under a separately given probability model P (each ordered outcome in S has probability 1/4), compute the probabilities 1/4, 1/2, 1/4 of the outcomes in S′, showing that outcomes in one sample space need not be equally likely; (4) use another valid, non-uniform model Q on S to show that the sample space by itself does not fix probabilities; (5) distinguish the outcome (H,T) from the event {(H,T),(T,H)}. Works inside the MKO's scope: the experiment and observation scale are explicit (assumption a1), and the sample space contains every possible elementary outcome under that description (assumption a2). Probability values are computed only in explicitly given models (G4, G5), as additional data of a later probability model, never derived from the sample space. It does not treat continuous or infinite sample spaces or measure theory, and does not change the canonical MKO or its English edition. ## Givens and symbols - cartesian_product_def - finite_counting_basics - prob_axioms - image_preimage_def - finite_prob_weights - G1 — Experiment: toss the same coin twice. Each toss results in H (heads) or T (tails), with no other result (landing on edge is excluded) (assumption a1). - G2 — Observation scale 1: record both results in order, as an ordered pair (first, second). - G3 — Observation scale 2: record only the number of H among the two tosses. - G4 — Probability model P (additional data, not derived from the sample space): each ordered outcome in S has probability 1/4, as used for example when the coin is fair and the tosses are independent. - G5 — Another probability model Q (additional data): Q((H,H))=9/25, Q((H,T))=6/25, Q((T,H))=6/25, Q((T,T))=4/25, as used for example when H has probability 3/5 and the tosses are independent. - H,\ T — heads, tails - S — the sample space when both results are recorded in order - S' — the sample space when only the number of heads is recorded - h — the function sending an ordered outcome to its number of heads - P,\ Q — two different probability models on S - P' — the probability on S′ obtained from P through h ## 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. - 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. - 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). - 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. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - 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. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain. - 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. - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - 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. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - 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. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_sample_space · cited — If a random experiment has sample space S, every possible elementary outcome x satisfies x∈S. Membership in the space does not itself assume that outcomes are equally likely. · mko-sample-space - finite_prob_weights · prerequisite — Point weights on a finite sample space: if each outcome ω is given p(ω)≥0 and all the p(ω) sum to 1, then setting P(E)=Σ_{ω∈E} p(ω) for every subset E of S gives a P that satisfies the probability axioms. - L_S_complete · lemma — Under G1 and G2, every possible elementary outcome belongs to S={(H,H),(H,T),(T,H),(T,T)}. ## Main derivation S01 · definitionBefore \text{experiment: two tosses, recorded in order} After \text{outcome}=(a,b),\ a,b\in\{H,T\} Conditions: none Rule: mko_sample_space · Uses: G1, G2 Leaf basis: mko_sample_space + def_intro By the MKO, the sample space depends on the experiment and on how it is observed, so both are fixed first: two tosses, recorded in order. An elementary outcome is then an ordered pair (a,b), where a is the first result and b the second, each H or T (G1). S02 · equivalentBefore \{(a,b)\mid a\in\{H,T\},\ b\in\{H,T\}\} After \{H,T\}\times\{H,T\} Conditions: none Rule: cartesian_product_def · Uses: S01 Leaf basis: cartesian_product_def + set_builder The possible ordered records are exactly the ordered pairs with a and b each ranging over {H,T}; by definition this is the Cartesian product {H,T}×{H,T}. S03 · equivalentBefore \{H,T\}\times\{H,T\} After S=\{(H,H),(H,T),(T,H),(T,T)\} Conditions: none Rule: case_analysis · Uses: S02 Leaf basis: case_analysis + cartesian_product_def + set_extensionality Split on a (H or T), and in each case on b (H or T), obtaining four ordered pairs. List them and call this set S. S04 · impliesBefore x\ \text{a possible elementary outcome} After x\in S Conditions: none Rule: L_S_complete · Uses: S01, S03 Leaf basis: forall_intro + case_analysis + cartesian_product_def By Lemma L_S_complete (proved in S04.1 and S04.2), every possible elementary outcome belongs to S. This is exactly the MKO's requirement x∈S, and it meets assumption a2: S contains all possible elementary outcomes. S05 · impliesBefore |\{H,T\}\times\{H,T\}| After |S|=2\cdot 2=4 Conditions: H\neq T Rule: finite_counting_basics · Uses: S02, S03 Leaf basis: finite_counting_basics + cartesian_product_def + numeric_evaluation By finite counting |A×B|=|A|·|B|, |S|=2·2=4. The four listed pairs are pairwise distinct: for example (H,T) and (T,H) differ in the first coordinate, so they are different outcomes; the order is part of the record. S06 · definitionBefore \text{ordered outcome }(a,b)\in S After h:S\to S',\ h(a,b)=\text{number of }H\text{ among }a,b,\ S'=\{0,1,2\} Conditions: none Rule: def_intro · Uses: G3, S03 Leaf basis: def_intro + function_def Switch to observation scale 2 (G3): record only the number of H. Two tosses can show 0, 1 or 2 heads, so the second sample space is S′={0,1,2}. The two scales are linked by the function h:S→S′ sending an ordered outcome to the number of H it contains. S07 · impliesBefore h(H,H),\ h(H,T),\ h(T,H),\ h(T,T) After 2,\ 1,\ 1,\ 0;\quad h(S)=\{0,1,2\}=S' Conditions: none Rule: image_preimage_def · Uses: S03, S04, S06 Leaf basis: image_preimage_def + numeric_evaluation Compute each value: h(H,H)=2, h(H,T)=1, h(T,H)=1, h(T,T)=0. So the image h(S)={0,1,2}=S′: every possible number of heads is in S′ (complete), and every value in S′ can occur. S08 · impliesBefore |S|=4,\ |S'|=3 After S\neq S' Conditions: none Rule: set_extensionality · Uses: S05, S07 Leaf basis: set_extensionality + finite_counting_basics The elements of S are ordered pairs and those of S′ are numbers; even their sizes differ (4 and 3). So one experiment has different sample spaces under different observation scales, as the MKO says. S09 · impliesBefore p(\omega)=\tfrac14\ \ (\omega\in S) After P\ \text{is a probability on }S Conditions: p(\omega)\ge 0; \sum_{\omega\in S}p(\omega)=1 Rule: finite_prob_weights · Uses: G4, S03 Leaf basis: finite_prob_weights + numeric_evaluation G4 is model data given separately; it is not derived from S. The four weights are ≥0 and sum to 4·(1/4)=1, so by finite_prob_weights, P(E)=Σ_{ω∈E} p(ω) is a probability on S. S10 · equivalentBefore h^{-1}(\{0\}),\ h^{-1}(\{1\}),\ h^{-1}(\{2\}) After \{(T,T)\},\ \{(H,T),(T,H)\},\ \{(H,H)\} Conditions: none Rule: image_preimage_def · Uses: S07 Leaf basis: image_preimage_def + set_extensionality + numeric_evaluation By the definition of preimage, h⁻¹({k}) consists of the outcomes in S with k heads. Reading the values of S07: 0 heads only for (T,T); 1 head for (H,T) and (T,H); 2 heads only for (H,H). The three preimages are pairwise disjoint and their union is S. 'Observing k heads' happens exactly when the event h⁻¹({k}) in S occurs. S11 · impliesBefore P'(k)=P(h^{-1}(\{k\})) After P'(0)=\tfrac14,\ P'(1)=\tfrac12,\ P'(2)=\tfrac14 Conditions: \{(H,T)\}\cap\{(T,H)\}=\varnothing Rule: prob_axioms · Uses: S09, S10 Leaf basis: prob_axioms + finite_prob_weights + def_intro + numeric_evaluation Define weights on S′ by P′(k)=P(h⁻¹({k})). By P from S09 and finite additivity: P′(0)=P({(T,T)})=1/4; P′(1)=P({(H,T)})+P({(T,H)})=1/4+1/4=1/2; P′(2)=P({(H,H)})=1/4. All three are ≥0 and sum to 1/4+1/2+1/4=1, so by finite_prob_weights, P′ is a probability on S′. S12 · impliesBefore P'(1)=\tfrac12,\ P'(0)=\tfrac14 After P'(1)\neq P'(0) Conditions: none Rule: numeric_evaluation · Uses: S11 Leaf basis: numeric_evaluation 1/2≠1/4, so in this model the three outcomes of S′ are not equally likely, even though all three are elements of S′. Belonging to one sample space does not imply being equally likely. Wrongly treating S′ as equally likely would give 1/3 to each outcome, which disagrees with P′(1)=1/2. S13 · impliesBefore Q:\ \tfrac{9}{25},\ \tfrac{6}{25},\ \tfrac{6}{25},\ \tfrac{4}{25} After Q\ \text{is a probability on }S,\ Q\neq P Conditions: \text{weights}\ge 0; \text{total}=1 Rule: finite_prob_weights · Uses: G5, S03, S09 Leaf basis: finite_prob_weights + numeric_evaluation The four weights of G5 are ≥0 and sum to (9+6+6+4)/25=1, so by finite_prob_weights Q is also a probability on S. But Q((H,H))=9/25≠4/25=Q((T,T)), so Q is not uniform and differs from P. One sample space S carries two different probability models, so S by itself carries no assumption of equal likelihood. These weights correspond to H having probability 3/5 with independent tosses: (3/5)²=9/25, (3/5)(2/5)=6/25, (2/5)²=4/25. S14 · impliesBefore (H,T)\in S,\ E=\{(H,T),(T,H)\} After (H,T)\in E\subseteq S,\ (H,T)\neq E Conditions: none Rule: subset_def · Uses: S03, S10 Leaf basis: subset_def + set_extensionality (H,T) is an element of S, that is an elementary outcome. 'Exactly one head' corresponds to E=h⁻¹({1})={(H,T),(T,H)}, a subset of S, that is an event. (H,T)∈E, but (H,T)≠E: one is an ordered pair, the other a set containing two ordered pairs. When the outcome is (H,T), the event E occurs. S15 · impliesBefore \text{two observation scales and two models} After S=\{H,T\}^2,\ |S|=4;\ S'=\{0,1,2\};\ P'=(\tfrac14,\tfrac12,\tfrac14);\ Q\neq P Conditions: none Rule: and_intro_elim · Uses: S04, S05, S07, S08, S11, S12, S13, S14 Leaf basis: and_intro_elim Collect the results: recorded in order, S has 4 elements and contains every possible outcome (S04, S05); recording only the number of heads gives S′={0,1,2} (S07, S08); under G4 the outcomes of S′ have probabilities 1/4, 1/2, 1/4 and are not equally likely (S11, S12); S can carry different models (S13); (H,T) is an outcome and {(H,T),(T,H)} is an event (S14). ## Substeps and lemmas S04.1 · impliesBefore x\ \text{possible} After x=(a,b),\ a\in\{H,T\},\ b\in\{H,T\} Conditions: none Rule: def_unfold · Uses: S01, G1 Leaf basis: def_unfold + forall_elim Let x be an arbitrary possible elementary outcome. By the observation scale of S01, x is an ordered pair (a,b); by G1 each toss can only give H or T, so a, b∈{H,T}. S04.2 · impliesBefore x=(a,b),\ a,b\in\{H,T\} After x\in S Conditions: none Rule: forall_intro · Uses: S04.1, S02, S03 Leaf basis: cartesian_product_def + eq_replace + forall_intro By S02, (a,b)∈{H,T}×{H,T}; by S03 this product equals S, so x∈S. Since x was arbitrary, ∀-introduction shows that every possible elementary outcome belongs to S. S04.1 and S04.2 together prove Lemma L_S_complete. ## Reverse audits - S15 · sufficient_goal_reduction · S04, S05, S07, S08, S11, S12, S13, S14, and_intro_elim — Goal G is the conjunction of the five conclusions of the problem; each is proved forwards from the givens by the listed steps, and this step only forms the conjunction; G is never used as a premise. - S14 · premise_audit · S03, S10, subset_def — E⊆S follows because both elements of E lie in S (a complete check). It is not claimed that outcomes and events are interchangeable. - S13 · premise_audit · G5, finite_prob_weights, numeric_evaluation — Validity of Q needs only nonnegativity and total 1 (N6); the link to independence only explains where the weights come from, and the argument does not depend on it (N7 to N9 only check the arithmetic). - S12 · premise_audit · S11, numeric_evaluation — Only two explicit rationals are compared (N5). The conclusion concerns the model G4; it is not claimed that S′ is non-uniform under every model. - S11 · premise_audit · S09, S10, prob_axioms, finite_prob_weights — Additivity is used only for the disjoint single-point events {(H,T)} and {(T,H)}; the values of P′ depend entirely on the model G4, not on S′ itself. - S10 · inverse_equivalence · image_preimage_def, set_extensionality — Each preimage is decided element by element over the four elements of S, so both sides have the same elements and the step holds both ways. - S09 · premise_audit · G4, finite_prob_weights, prob_axioms — It needs the two conditions nonnegativity and total 1; N2 checks the latter. It does not claim that G4 is the only possible model (S13 gives another). - S08 · premise_audit · S05, S07, set_extensionality — Different sizes are enough to show that the sets differ. Both are legitimate sample spaces, each relative to its own observation scale. - S07 · premise_audit · S03, S04, image_preimage_def, L_S_complete — Since S contains every possible outcome (S04), h(S) is the set of all possible numbers of heads; this is a complete computation over the four elements of S, not a sample. - S06 · premise_audit · G3, def_intro — This step only defines; completeness of S′ is checked in S07 through the values of h. - S05 · premise_audit · finite_counting_basics, cartesian_product_def — It needs {H,T} to have two distinct elements (H≠T); the conclusion is a count and says nothing about probabilities. - S04.2 · premise_audit · S02, S03, forall_intro — It needs the set equality of S03; it does not claim that the elements of S are equally likely. - S04.1 · premise_audit · G1, S01 — Only the descriptions of the experiment and of the record in G1 and G2 are used; x is arbitrary. - S04 · premise_audit · L_S_complete, G1 — Completeness rests on G1's 'each toss is H or T'; if the experiment allowed the coin to land on edge, S would not be complete. - S03 · inverse_equivalence · case_analysis, cartesian_product_def, set_extensionality — The case split exhausts the two values of {H,T}, so the listed set and the product have the same elements: each listed pair is in the product, and each element of the product is listed. - S02 · inverse_equivalence · cartesian_product_def — This directly rewrites the definition of a Cartesian product; both directions are given by the definition. - S01 · premise_audit · G1, G2, mko_sample_space — This step only makes the experiment and observation scale explicit (assumption a1) and derives no new fact; a different way of recording gives a different sample space (see S06). ## Error controls and negative controls One sample space does not mean equally likelyThe MKO names the mistake of believing that outcomes in one sample space must be equally likely. S′={0,1,2} is a legitimate sample space, yet under the model P its three outcomes have probabilities 1/4, 1/2, 1/4 (S11), not 1/3 each. Even the uniform weights on S are separate data from G4; the model Q of G5 is not uniform on the same S (S13). An outcome is not an eventThe MKO warns against confusing a single outcome with an event set. (H,T) is an element of S; 'exactly one head' is, in S, the event {(H,T),(T,H)} with two outcomes (S14). The same description corresponds to the outcome 1 in S′ but to an event in S; one must first say which sample space is in use. Omitting a possible outcomeWhen results are recorded in order, (H,T) and (T,H) are different outcomes (S05). Writing S as {(H,H),(H,T),(T,T)} omits the possible outcome (T,H) and violates assumption a2; later event and probability computations would lose their correct domain. The proof of L_S_complete (S04.1, S04.2) is what rules out such an omission. - S′={0,1,2} is a sample space, so each outcome has probability 1/3 → reject — Under the model P, P′(1)=1/2≠1/3 (S11); a sample space carries no assumption of equal likelihood. - S has 4 elements, so (H,H) must have probability 1/4 → reject — On the same S, the model Q gives (H,H) probability 9/25 (S13). - When results are recorded in order, {(H,H),(H,T),(T,T)} is the sample space → reject — (T,H) is a possible outcome but is missing, violating assumption a2. - (H,T) and {(H,T),(T,H)} are the same object → reject — The first is an ordered pair (an outcome), the second a two-element set (an event). - S and S′ differ, so at least one of them is not a sample space of this experiment → reject — Each is relative to a different observation scale (G2, G3), and both are legitimate sample spaces (S04, S07). ## Result and limitations Recording two coin tosses in order, the sample space S={(H,H),(H,T),(T,H),(T,T)} contains every possible elementary outcome and has exactly 4 elements; recording only the number of heads gives the sample space S′={0,1,2}. Under the separately given model P, the outcomes of S′ have probabilities 1/4, 1/2, 1/4 and are not equally likely; S also carries the non-uniform model Q. So a sample space only says which outcomes are possible and does not fix probabilities. (H,T) is an outcome; {(H,T),(T,H)} is an event. - G4 and G5 are modelling assumptions; this guide does not discuss whether they fit an actual coin, which is a statistical question. - finite_prob_weights is used as a prerequisite and is not derived from the probability axioms in this guide. ## Verification and source binding 11 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: c0d1f9b0e3d3e27afde0183074318b955b8122887189e0f0232556ac536804a1 - original source SHA-256: c0d1f9b0e3d3e27afde0183074318b955b8122887189e0f0232556ac536804a1 - 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-sample-space-01.json)