ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Binomial upper confidence limit by lower-tail test inversion

Example

Let the observation space be ${0, \dots, n}$ with its full power set, $n \geq 1$ , $p \in [0, 1]$ , $0 < α < 1$ , and let $X$ have mass $P_{p} (X = j) = (\binom{n}{j}) p^{j} (1 - p)^{n - j}$ , $j = 0, \dots, n$ , with $0^{0} = 1$ . Define $F_{p} (k) = \sum_{j = 0}^{k} (\binom{n}{j}) p^{j} (1 - p)^{n - j}$ . For $k < n$ , let $U_{k} \in (0, 1)$ be the unique solution of $F_{U_{k}} (k) = α$ , and set $U_{n} = 1$ . Then $C (X) = [0, U_{X}]$ is the confidence set obtained by inverting the lower-tail tests that reject $p = p_{0}$ when $F_{p_{0}} (X) < α$ . Its coverage is at least $1 - α$ ; discreteness can make it conservative.

Facts & Assumptions

Given: The finite binomial model, $n \geq 1$ , $p \in [0, 1]$ , and $0 < α < 1$ .

[F1]

The binomial theorem over an arbitrary commutative ring: the binomial expansion holds for real $p$ and $1 - p$ .

[F2]

Confidence sets and coverage: coverage is the probability that the true parameter belongs to the confidence set.

[F3]

Coverage from test inversion: inverting measurable point-null acceptance events of probability at least $1 - α$ gives coverage at least $1 - α$ .

[F4]

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ : $(\binom{n}{j})$ counts the $j$ -element subsets of an $n$ -element set.

[F5]

Sigma-algebras: a sigma-algebra is an algebra of subsets closed under countable unions.

[F6]

Probability measures and probability spaces: a probability measure is a measure of total mass one on a measurable space.

[F7]

Statistical experiments: an experiment fixes a measurable observation space and a probability law for each parameter.

[F8]

Test size and power: a test has level $α$ when its size, the supremum of its rejection probabilities over the null, is at most $α$ .

[F9]

On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed: a continuous function on an interval with strictly negative derivative at every interior point is strictly decreasing on that interval.

[F10]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ : a continuous real function on a closed interval takes every value between its endpoint values.

Verification

1.1givenF1F5F6F7algebra

The full power set of ${0, \dots, n}$ is an algebra closed under countable unions, hence a sigma-algebra by [F5]. The binomial theorem [F1] gives $\sum_{j = 0}^{n} (\binom{n}{j}) p^{j} (1 - p)^{n - j} = (p + 1 - p)^{n} = 1$ ; all terms are nonnegative for $p \in [0, 1]$ , so [F6] makes the displayed masses a probability measure, including $p = 0, 1$ . These laws form an experiment as in [F7].

1.2givenF4F9F10algebra

For $k < n$ , count pairs consisting of a $j$ -element subset of an $n$ -element set and a distinguished element inside it. Counting in the two orders gives $j (\binom{n}{j}) = n (\binom{n - 1}{j - 1})$ for $1 \leq j \leq k$ . Counting instead a distinguished element outside the subset gives $(n - j) (\binom{n}{j}) = n (\binom{n - 1}{j})$ for $0 \leq j \leq k$ , by [F4]. The first identity is not used at $j = 0$ : in differentiating $p^{j}$ , that boundary term is zero, so the first derivative sum starts at $j = 1$ , while the second identity includes $j = 0$ . Since $F_{p} (k)$ is a polynomial, it is continuous on $[0, 1]$ , and for $0 < p < 1$ termwise differentiation and the two identities give $\frac{d}{d p} F_{p} (k) = \sum_{j = 1}^{k} j (\binom{n}{j}) p^{j - 1} (1 - p)^{n - j} - \sum_{j = 0}^{k} (n - j) (\binom{n}{j}) p^{j} (1 - p)^{n - j - 1} = - n (\binom{n - 1}{k}) p^{k} (1 - p)^{n - k - 1} < 0.$ When $k = 0$ , the first sum is empty and the $j = 0$ term of the second sum gives the same formula. By [F9], $F_{p} (k)$ is strictly decreasing on $[0, 1]$ . Also $F_{0} (k) = 1$ and $F_{1} (k) = 0$ because $k < n$ . Applying [F10] to this continuous polynomial on $[0, 1]$ gives a point $U_{k} \in (0, 1)$ with $F_{U_{k}} (k) = α$ ; strict decrease makes it unique.

2.1givenF8step 1.1algebra

For each fixed candidate $p_{0}$ , $F_{p_{0}} (k)$ is nondecreasing in integer $k$ . Let $k_{0}$ be the least $k \in {0, \dots, n}$ with $F_{p_{0}} (k) \geq α$ , which exists because $F_{p_{0}} (n) = 1$ . The deterministic test function is $φ_{p_{0}} (x) = 1_{{F_{p_{0}} (x) < α}}$ ; it is measurable on this finite space. Its rejection event is ${X < k_{0}}$ , whose probability is $0$ if $k_{0} = 0$ , and otherwise is $F_{p_{0}} (k_{0} - 1) < α$ . The null is ${p_{0}}$ , and the alternative $[0, 1] ∖ {p_{0}}$ is nonempty; by [F8] the test size equals this rejection probability and is at most $α$ .

3.1givenF2F3step 1.2step 2.1algebra∎

For an observed $x < n$ , strict decrease of $F_{p} (x)$ in $p$ makes ${p_{0} : F_{p_{0}} (x) \geq α} = [0, U_{x}]$ ; for $x = n$ , the set is $[0, 1] = [0, U_{n}]$ . Thus $C (X)$ is precisely the inversion of those acceptance events. The level calculation in step 2.1 and [F3] imply its coverage is at least $1 - α$ , in the sense of [F2].

Remarks

The finite binomial size calculation uses the current Test size and power interface, and Coverage from test inversion supplies the stated coverage implication.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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 p. 1 (standard reference, not scraped)
Karl B. Gregory, USC STAT 713, Lecture 14: Confidence Intervals and Sets, slide 12, PDF p. 20 (standard reference, not scraped)