# Pointwise coverage, averaging and selection [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-confidence-interval-coverage/) 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-finite-confidence-interval-coverage-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Compute pointwise and worst-case coverage of a fixed interval procedure. Frequentist coverage is not an observed-data posterior; selection must be incorporated anew. ## Givens and symbols - work - G1 — Theta={0,1}, Omega={a,b,c}, P0=(1/2,1/4,1/4), P1=(1/4,1/4,1/2). Precommit I(a)=[0,0], I(b)=[0,1], I(c)=[0,0]. - I(x) — precommitted interval procedure - C(θ) — pointwise coverage - A — selection event ## Rules and sources - mko_definition · cited — Supply the complete normalized finite sampling law for every theta. The precommitted procedure I(x)=[L(x),U(x)] is defined at every sample, independent of the unknown theta, and has L(x)≤U(x). Its pointwise coverage is sum_x P_theta(x)*1{L(x)≤theta≤U(x)}; its worst-case coverage is the minimum over the finite theta carrier. An average-only boundary must have distinct pointwise coverages and a target with average≥target>minimum. Posterior probability uses a prior and observed data and is not this coverage. Selection included in the full procedure can be analyzed again; the error is ignoring selection while reusing old coverage. Zero selected mass makes the corresponding conditional coverage undefined. · mko-finite-confidence-interval-coverage - work · prerequisite — C(theta)=sum_x Ptheta(x)1{L(x)≤theta≤U(x)}; worst case is the minimum; positive-mass selection uses the conditional intersection quotient. ## Main derivation S01 · impliesBefore P_0,P_1 After 1/2+1/4+1/4=1,\quad1/4+1/4+1/2=1 Conditions: none Rule: work · Uses: G1, work Leaf basis: work Both complete laws normalize; the interval at each sample is precommitted. S02 · impliesBefore I(a),I(b),I(c) After L(x)\le U(x)\quad\text{for all }x\in\Omega Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work All three closed intervals have ordered endpoints and the procedure is total. S03 · impliesBefore \theta=0:\quad\mathbf1\{0\in I(x)\} After (1,1,1),\quad C(0)=1 Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work Zero belongs to every closed interval, yielding coverage one. S04 · impliesBefore \theta=1:\quad\mathbf1\{1\in I(x)\} After (0,1,0),\quad C(1)=P_1(b)=1/4 Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work One belongs only to the interval at b; use its mass under the second law. S05 · impliesBefore \min_{\theta\in\Theta}C(\theta) After \min(1,1/4)=1/4 Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work Worst-case coverage on the finite parameter set is the minimum, not the average. S06 · impliesBefore \overline C=(C(0)+C(1))/2,\quad q=1/2 After \overline C=5/8\ge1/2>1/4=\min C Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work This explicitly witnesses average-only validity: the average meets the target while worst-case coverage fails. S07 · impliesBefore A=\{a,b\}\text{ selected},\quad\theta=1 After P_1(1\in I(X)\mid A)=\frac{P_1(b)}{P_1(a)+P_1(b)}=1/2 Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work Reporting only at a,b requires recomputed conditional coverage, differing from original1/4. S08 · impliesBefore x_{\rm obs}=b,\quad I(b)=[0,1] After \mathbf1\{\theta\in I(b)\}=1\quad(\theta=0,1) Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work After observing b this fixed interval contains either allowed theta; procedure coverage1/4 is not its posterior. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — A posterior needs a prior and data update; no prior was supplied. - S07 · premise_audit · G1, S06, work — The selection denominator 1/2 is positive; zero selection mass would leave it undefined. - S06 · premise_audit · G1, S05, work — The average is a specified equal-weight summary, not an automatic frequentist guarantee or prior. - S05 · premise_audit · G1, S04, work — Both theta values have been fully computed. - S04 · premise_audit · G1, S03, work — Even coincident numerical masses do not remove the need to use the correct law. - S03 · premise_audit · G1, S02, work — Endpoint equality must be included. - S02 · premise_audit · G1, S01, work — The two singleton intervals[0,0] are valid. - S01 · premise_audit · G1, work — The procedure cannot change with true theta. ## Error controls and negative controls Complete procedureFix intervals at a,b,c before weighting either law. Recompute selectionCompute selection numerators and denominators under the same theta law. - Average5/8 means every theta has coverage≥1/2. → reject — At theta=1 coverage is only 1/4. - After selecting a,b coverage remains1/4. → reject — The recomputed conditional coverage at theta=1 is 1/2. - After b the posterior probability of theta in I(b) is 1/4. → reject — I(b) contains all of Theta, so every valid posterior gives 1; the1/4 is procedural pointwise coverage. ## Result and limitations C(0)=1 and C(1)=1/4, with worst case1/4; average5/8 does not guarantee1/2 for every parameter. ## Verification and source binding 3 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 4107037a3f83077f1cc2a7fa2b5b455a7cdbabb0e3e44d2397157a1118baea32 - original source SHA-256: e02e1138c369c28009b17a65c10da3c0ca5a8b024ccd40f5a3df260cadf99b8b - 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-finite-confidence-interval-coverage-01.json)