TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-14 (gpt-6.1-sol)

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.

Valid p-values yield level tests for nonempty disjoint alternatives

Statement

Let $p$ be a valid p-value for a nonempty null hypothesis $Θ_{0}$ in a statistical experiment. For every $α \in [0, 1]$ , the deterministic test with rejection function $φ_{α} (x) = 1_{{p (x) \leq α}}$ satisfies $P_{θ} (p (X) \leq α) = E_{θ} [φ_{α} (X)] \leq α (θ \in Θ_{0}) .$ Consequently, whenever a nonempty alternative hypothesis $Θ_{1} \subseteq Θ ∖ Θ_{0}$ is specified, this test has size at most $α$ and hence level $α$ in the sense of Test size and power.

Facts & Assumptions

Given: An experiment, a valid p-value statistic $p : X \to [0, 1]$ for $Θ_{0} \neq \emptyset$ , and $α \in [0, 1]$ . The pointwise bound does not require an alternative hypothesis.

[F1]

Valid p-values: validity means $P_{θ} ({x : p (x) \leq u}) \leq u$ for every $θ \in Θ_{0}$ and $u \in [0, 1]$ .

[F2]

A measurable function between measurable spaces: a statistic is measurable when inverse images of Borel sets are measurable.

[F3]

Every measurable rejection function defines a randomized test: every measurable $φ : X \to [0, 1]$ defines a binary randomized test with rejection function $φ$ .

[F4]

The expectation of an indicator is the probability of the event: the expectation of an event indicator under $P_{θ}$ equals the probability of that event.

[F5]

Test size and power: when a nonempty alternative disjoint from $Θ_{0}$ is specified, size is $\sup_{θ \in Θ_{0}} E_{θ} [φ (X)]$ and level $α$ means size at most $α$ .

Proof

technique · direct

1.1givenF2F3construct

Let $A_{α} = {x : p (x) \leq α}$ . This event is measurable because $p$ is a statistic and $[0, α]$ is Borel in $[0, 1]$ . Thus $φ_{α} = 1_{A_{α}}$ is a measurable map into $[0, 1]$ , and [F3] supplies a randomized test with this rejection function. Since $φ_{α}$ takes only the values $0$ and $1$ , that kernel assigns probability one to the corresponding action, so the test is deterministic.

2.1F1F4F5step 1.1algebra∎

For every $θ \in Θ_{0}$ , [F4] and validity [F1] give $E_{θ} [φ_{α} (X)] = P_{θ} (A_{α}) \leq α$ , proving the pointwise bound. If a nonempty $Θ_{1} \subseteq Θ ∖ Θ_{0}$ is specified, taking the supremum over the nonempty set $Θ_{0}$ gives size at most $α$ by [F5], and therefore level $α$ .

Depends on

Used by

Dependency tree · two levels

30 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

Karl B. Gregory, USC STAT 713 Lecture 10: Tests of Hypotheses, Size, Power, and p-values, PDF pp. 17–20 (standard reference, not scraped)