TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Coverage from pivot inversion and exact calibration

Statement

Let $E = ((X, A), (P_{θ})_{θ \in Θ})$ be an experiment with nonempty $Θ$ . Let $q_{θ} : X \to S$ be a pivot with common law $ν$ , and let $B \in S$ . Define $C (x) : = {θ \in Θ : q_{θ} (x) \in B}$ If $ν (B) \geq 1 - α$ , then $C$ is a confidence set with coverage at least $1 - α$ . If $ν (B) = 1 - α$ , its coverage is exactly $1 - α$ for every parameter value. For an interval $B = [a, b]$ in $R$ , exactness requires calibration of the actual probability $ν ([a, b])$ ; quantile labels alone do not remove endpoint atoms.

Facts & Assumptions

Given: A nonempty parameter set $Θ$ , a statistical experiment, $0 \leq α \leq 1$ , a pivot $q_{θ}$ with common law $ν$ , and a measurable acceptance set $B$ with $ν (B) \geq 1 - α$ .

[F1]

Pivotal quantities: each section $q_{θ}$ is measurable and has pushforward law $ν$ , independent of $θ$ .

[F2]

Confidence sets and coverage: a set-valued procedure is measurable when every parameter-membership section is measurable, and coverage is the probability of that section under the corresponding $P_{θ}$ .

Proof

1.1givenF1F2

For each $η \in Θ$ , the membership section of $C$ is ${x : η \in C (x)} = q_{η}^{- 1} (B)$ . It is in $A$ because $q_{η}$ is measurable and $B \in S$ . Thus $C$ is a confidence-set procedure by [F2].

2.1givenF1F2step 1.1algebra∎

For every $θ \in Θ$ , $P_{θ} {θ \in C (X)} = P_{θ} (q_{θ}^{- 1} (B)) = ν (B) \geq 1 - α$ . Equality holds for every $θ$ when $ν (B) = 1 - α$ ; measurability was established in step 1.1.

Depends on

Used by

Exact selective tests and confidence sets from the pivot Corollary
A discrete pivot can give conservative coverage Example
Exact unknown-variance normal t interval Example
Known-variance normal mean interval Example
Uniform maximum pivot interval Example
Exact confidence and prediction intervals in Gaussian regression Theorem

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Anna Mikusheva, MIT 14.381, Lecture 11: Confidence Sets, §2, PDF pp. 2–3 (standard reference, not scraped)
Karl B. Gregory, USC STAT 713, Lecture 14: Confidence Intervals and Sets, slides 6 and 9, PDF pp. 6 and 14 (standard reference, not scraped)