# A complete fibre-pushforward sampling distribution [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-sampling-distribution/) 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-sampling-distribution-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Aggregate equal-valued outcomes of U under both theta laws. A sampling distribution is not a parameter distribution after one observation. ## Givens and symbols - work - G1 — Theta={1/4,3/4}, Omega={00,01,10,11}; P_(1/4)=(9,3,3,1)/16 and P_(3/4)=(1,3,3,9)/16. - G2 — U(x)=(x1+x2)/4 has total table(0,1/4,1/4,1/2) in Omega order, with target g(theta)=theta. - θ — fixed unknown parameter - U — one total statistic ## Rules and sources Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged. - mko_definition · cited — On one common finite sample space, fix a total statistic T independent of the unknown parameter. For each parameter, sum probabilities over statistic fibres and recheck nonnegativity and total mass 1. A sampling distribution is not an observed estimate, likelihood, posterior or distribution of the parameter itself. · mko-sampling-distribution - work · prerequisite — Finite laws have nonnegative probabilities summing to one; a statistic depends only on data, and expectation sums all weighted outcomes. ## Main derivation S01 · impliesBefore U=(0,1/4,1/4,1/2) After U(\Omega)=\{0,1/4,1/2\} Conditions: none Rule: work · Uses: G1, G2, work Leaf basis: work List distinct statistic values without duplicate support entries. S02 · impliesBefore U^{-1}(0),U^{-1}(1/4),U^{-1}(1/2) After \{00\},\{01,10\},\{11\} Conditions: none Rule: work · Uses: G1, G2, S01, work Leaf basis: work The three fibres are disjoint and cover all four outcomes. S03 · impliesBefore P_{1/4}(U=0) After 9/16 Conditions: none Rule: work · Uses: G1, G2, S02, work Leaf basis: work The zero-value fibre contains only 00. S04 · impliesBefore P_{1/4}(U=1/4) After 3/16+3/16=3/8 Conditions: none Rule: work · Uses: G1, G2, S03, work Leaf basis: work The middle fibre contains two observations whose masses must be added. S05 · impliesBefore P_{1/4}(U=1/2)=1/16 After P_{1/4}^U=(9/16,3/8,1/16) Conditions: none Rule: work · Uses: G1, G2, S04, work Leaf basis: work Complete the third entry to form the first full pushforward. S06 · impliesBefore P_{3/4}\text{ on the same fibres} After P_{3/4}^U=(1/16,3/8,9/16) Conditions: none Rule: work · Uses: G1, G2, S05, work Leaf basis: work Reaggregate the second law on the same fibres without changing U. S07 · impliesBefore 9/16+3/8+1/16,\quad1/16+3/8+9/16 After 1,\quad1 Conditions: none Rule: work · Uses: G1, G2, S06, work Leaf basis: work Both sampling distributions are nonnegative and normalized. S08 · impliesBefore x_{\rm obs}=01 After U(x_{\rm obs})=1/4\ne\text{the entire law }P_\theta^U Conditions: none Rule: work · Uses: G1, G2, S07, work Leaf basis: work One estimate is a value, distinct from the full repeated-sampling law. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, G2, S07, work — This distinguishes objects, not an assertion that numerical values never coincide. - S07 · premise_audit · G1, G2, S06, work — Normalization relies on the complete fibre partition. - S06 · premise_audit · G1, G2, S05, work — Equal middle entries do not make the full laws equal. - S05 · premise_audit · G1, G2, S04, work — Entries are ordered by 0,1/4,1/2. - S04 · premise_audit · G1, G2, S03, work — Using only the01 mass 3/16 would omit10. - S03 · premise_audit · G1, G2, S02, work — This is a statistic probability, not a parameter probability. - S02 · premise_audit · G1, G2, S01, work — Each sample belongs to exactly one fibre. - S01 · premise_audit · G1, G2, work — 01 and 10 belong to one fibre. ## Error controls and negative controls Complete fibresList{00},{01,10},{11} before summing masses. ParameterwiseKeep pushforwards separate rather than averaging laws. - P_(1/4)(U=1/4)=3/16. → reject — Both01 and 10 contribute, giving 3/8. - The two laws are identical. → reject — Their U=0 masses are 9/16 and 1/16. - Only observed 01 is needed for the sampling distribution. → reject — All carrier masses are required for normalization. ## Result and limitations The sampling laws of U are(9/16,3/8,1/16) and(1/16,3/8,9/16). ## Verification and source binding 3 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 34dc1cd85c3efadbcfd415dbe36f253fdad355a17c78ddeef279fa0cbb2bf808 - original source SHA-256: e67f4ec52577c1384b1c87cc1e0aa76a24df5697a005983130df8ae74bd5704c - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-sampling-distribution-01.json)