Pipeline-generated

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.

Tests, Neyman–Pearson and Valid P-values — Examples

1 · Prerequisites

2 · Summary

The finite examples compute a randomized test at a discrete likelihood-ratio atom and a threshold test for continuous densities. A two-point null law also shows that a measurable statistic taking values in $[0, 1]$ can fail superuniformity and produce an anti-conservative rejection rule.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A measurable [0,1]-valued statistic need not be a valid p-value

Statement refuted

Every measurable statistic $p : X \to [0, 1]$ is a valid p-value for a given null hypothesis.

Facts & Assumptions

Given: A statistical experiment with a nonempty null hypothesis and a disjoint nonempty alternative, and the definition of a valid p-value.

[F1]

Statistical experiments: an experiment supplies a measurable data space and a probability law for each parameter.

[F2]

Valid p-values: a valid p-value must satisfy $P_{θ} (p (X) \leq u) \leq u$ for every null parameter and every $u \in [0, 1]$ .

[F3]

Test size and power: for the simple null $Θ_{0} = {θ_{0}}$ and a nonempty disjoint alternative, size is the rejection probability under $P_{θ_{0}}$ .

[F4]

A measurable function between measurable spaces: a statistic is measurable when all measurable target sets have measurable preimages.

[F5]

The expectation of an indicator is the probability of the event: the expectation of an event indicator is the event's probability.

[F6]

Every measurable rejection function defines a randomized test: every measurable function into $[0, 1]$ defines a binary randomized test.

Counterexample

1.1givenF1F4algebraconstruct

Let $X = {0, 1}$ with the full sigma-algebra, $Θ = {θ_{0}, θ_{1}}$ , $Θ_{0} = {θ_{0}}$ , and $Θ_{1} = {θ_{1}}$ . Set $P_{θ_{0}} ({0}) = P_{θ_{0}} ({1}) = 1 / 2$ and $P_{θ_{1}} ({0}) = 0$ , $P_{θ_{1}} ({1}) = 1$ . These masses define probability measures: they are nonnegative and sum to one, and on the two-point space countable additivity follows because at most two members of a disjoint family are nonempty. Define $p (0) = 0$ and $p (1) = 1$ . It is measurable because every subset of $X$ is measurable.

2.1F2F3F5F6step 1.1algebra∎

At $u = 1 / 4$ , ${x : p (x) \leq u} = {0}$ , so $P_{θ_{0}} (p (X) \leq 1 / 4) = 1 / 2 > 1 / 4$ . Thus $p$ is not valid by [F2]. Thresholding it at $1 / 4$ defines a test by [F6], rejects on ${0}$ , and has size $1 / 2$ by [F3,F5], so it is anti-conservative. The claimed implication is false.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

Randomize at a discrete likelihood-ratio boundary

Example

On $X = {0, 1}$ with its full sigma-algebra and counting measure $μ$ , let the simple null and alternative laws be $P_{0} ({0}) = P_{0} ({1}) = 1 / 2$ and $P_{1} ({0}) = 1 / 4$ , $P_{1} ({1}) = 3 / 4$ . At level $α = 1 / 4$ , the Neyman–Pearson test randomizes with probability $1 / 2$ at $x = 1$ and rejects with probability $0$ at $x = 0$ . Its size is $1 / 4$ and its power is $3 / 8$ .

Verification

Given: The two probability laws above, counting measure $μ$ , and $α = 1 / 4$ . Assume AC for the general Neyman–Pearson comparison.

[A1] The Axiom of Choice: the Neyman–Pearson theorem is used in its AC density-selection branch; the finite example's densities are explicit.

[F1] Counting measure on an arbitrary set: each singleton has $μ$ -measure $1$ .

[F6] Counting measure is a measure and Finite, sigma-finite, and semifinite measures: the counting set function is a measure; a finite measure is sigma-finite.

[F2] Likelihood-ratio tests with boundary randomization and The likelihood-ratio rule is a measurable test of exact size: the candidate is a measurable randomized test of exact size; on ${p_{0} > 0}$ it rejects above its cutoff and randomizes by $γ$ at equality.

[F3] Test size and power: size is null rejection probability and power is alternative rejection probability.

[F4] Expectation of a nonnegative or integrable random variable, Nonnegative simple measurable functions, The integral of a nonnegative simple function, and The nonnegative integral agrees with the simple integral on simple functions: expectation of this finite-valued rejection function is the sum of its values weighted by the point masses.

[F5] Neyman–Pearson lemma with singular alternative mass: no test of size at most $1 / 4$ has larger power than the constructed likelihood-ratio test.

[F7] Probability measures and probability spaces: a measure with total mass $1$ is a probability measure.

[F8] A measurable function between measurable spaces: every real-valued function on the two-point space with its full sigma-algebra is measurable.

1.1givenF1F6F7algebra

By [F1] and [F6], $μ$ is a measure with $μ (X) = 2$ , so it is finite and hence sigma-finite. Each displayed law has nonnegative masses summing to $1$ , and any disjoint family of subsets of ${0, 1}$ has at most two nonempty members, so each law is countably additive. Thus $P_{0}, P_{1}$ are probability measures by [F7].

2.1F2F4F8step 1.1algebra

Define $p_{0} (0) = p_{0} (1) = 1 / 2$ , $p_{1} (0) = 1 / 4$ , and $p_{1} (1) = 3 / 4$ . They are finite, nonnegative, and measurable by [F8]. For every $A \subseteq X$ , the simple-integral formula in [F4] gives $\int_{A} p_{i} d μ = \sum_{x \in A} p_{i} (x) = P_{i} (A)$ , so these are density representatives and $P_{i} ≪ μ$ . Hence $R (0) = 1 / 2$ and $R (1) = 3 / 2$ . With $c = 3 / 2$ , $P_{0} (R > c) = 0$ and $P_{0} (R = c) = 1 / 2$ , so the boundary equation gives $γ = (1 / 4) / (1 / 2) = 1 / 2$ . The test has $φ^{*} (1) = 1 / 2$ and $φ^{*} (0) = 0$ .

3.1F3F4step 2.1algebra

Using [F4], its size is $E_{P_{0}} φ^{*} = (1 / 2) (1 / 2) + (1 / 2) (0) = 1 / 4$ , and its power is $E_{P_{1}} φ^{*} = (3 / 4) (1 / 2) + (1 / 4) (0) = 3 / 8$ . Thus it uses the boundary atom to attain the requested size.

4.1A1F5step 3.1∎

The Neyman–Pearson lemma [F5] makes this test most powerful among all tests whose size is at most $1 / 4$ .

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A continuous likelihood-ratio test

Example

On $[0, 1]$ with restricted Lebesgue measure, let $P_{0}$ have density $p_{0} (x) = 1$ and let $P_{1}$ have density $p_{1} (x) = 2 x$ . At level $α = 1 / 4$ , the likelihood-ratio test rejects for $x > 3 / 4$ , has size $1 / 4$ , and has power $7 / 16$ .

Verification

Given: The interval data space $([0, 1], A)$ , where $A$ is the trace of the Lebesgue sigma-algebra, restricted Lebesgue measure $μ$ , the densities $p_{0} (x) = 1$ and $p_{1} (x) = 2 x$ , and $α = 1 / 4$ .

[F0] Statistical experiments: an experiment consists of a data measurable space, a parameter set, and one probability law for each parameter.

[A1] The Axiom of Choice: AC is assumed for the general Neyman–Pearson theorem; the example's density representatives $p_{0} = 1$ and $p_{1} = 2 x$ are explicit.

[A2] The Axiom of Countable Choice ( ${A C}_{ω}$ ): CC is used for the restricted Lebesgue-measure construction and the Riemann-to-Lebesgue equality below.

[F1] Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, and A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included: under CC, restricted Lebesgue measure is a measure; interval mass is length and singleton mass is zero.

[F2] Continuous functions on Euclidean spaces are Borel measurable and A measurable function between measurable spaces: the continuous extension $x \mapsto 2 x$ on $R$ is Borel measurable, so its restriction to $[0, 1]$ is measurable for the trace sigma-algebra $A$ .

[F3] The measure with density $f$ relative to $μ$ and Integrating against a density agrees with integrating the product: $A \mapsto \int_{A} 2 x d μ$ is a measure and integrates nonnegative $g$ as $\int g (x) 2 x d μ (x)$ .

[F4] A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: the continuous function $2 x$ is Riemann integrable on every compact subinterval.

[F5] Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions, For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , and The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ : the bounded Riemann-integrable function has the same Darboux integral, and each lower sum is at most it while each upper sum is at least it.

[F6] Finite sums and finite products, by recursion, Laws of finite sums and finite products, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, and The principle of mathematical induction: finite sums obey their recursion, naturals are interpreted in $R$ , and induction holds.

[F7] For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ : for each $ε > 0$ a positive natural $N$ can be chosen with $1 / N < ε$ .

[F8] The measure with density $f$ relative to $μ$ , Integrating against a density agrees with integrating the product, and The expectation of an indicator is the probability of the event: density integrals give the corresponding law masses and rejection probabilities.

[F9] Likelihood-ratio tests with boundary randomization, The likelihood-ratio rule is a measurable test of exact size, and Test size and power: the candidate rejects above its likelihood-ratio cutoff and has the displayed null size.

[F10] Neyman–Pearson lemma with singular alternative mass: no test of size at most $1 / 4$ has greater power than the candidate.

[F11] Finite, sigma-finite, and semifinite measures: a finite measure is sigma-finite by the one-set cover consisting of the whole space.

[F12] A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral: under CC, a bounded Riemann-integrable function is Lebesgue measurable and its Lebesgue and Riemann integrals agree.

[F13] Probability measures and probability spaces: a measure with total mass $1$ is a probability measure.

[F14] Nonnegative simple measurable functions, The integral of a nonnegative simple function, and The nonnegative integral agrees with the simple integral on simple functions: for every measurable $A$ , $\int_{A} 1 d μ = μ (A)$ .

Proof technique: direct.

1.1A2F1F2F3F13given

By [A2] and [F1], Lebesgue measure is a measure and $[0, 1]$ is measurable with measure $1$ . Each event in the trace sigma-algebra $A$ is therefore Lebesgue measurable, and restricting Lebesgue measure to these events preserves countable additivity. Hence $μ$ is a probability measure by [F13]. Define $Q_{1} (A) = \int_{A} 2 x d μ (x)$ . The density is nonnegative and measurable by [F2], so [F3] makes $Q_{1}$ a measure.

1.2F6algebrainduction

Let $S_{N} = \sum_{k < N} k$ . Its recursion is $S_{0} = 0$ and $S_{N + 1} = S_{N} + N$ , so induction [F6] gives $2 S_{N} = N (N - 1)$ for every $N \geq 0$ .

2.1F4F5F6step 1.2algebra

Fix $0 \leq a < b \leq 1$ , put $d = b - a$ , and divide $[a, b]$ into $N \geq 1$ equal intervals of length $d / N$ . Since $2 x$ is increasing, the lower and upper sums are respectively $L_{N} = 2 a d + d^{2} (1 - 1 / N)$ and $U_{N} = 2 a d + d^{2} (1 + 1 / N)$ , by substituting $S_{N} = N (N - 1) / 2$ into the finite sums in [F5].

3.1A2F5F7F12step 2.1algebra

The value $b^{2} - a^{2} = 2 a d + d^{2}$ lies between $L_{N}$ and $U_{N}$ , and their gap is $2 d^{2} / N$ . By [F7] this gap can be made arbitrarily small. The Lebesgue integral equals the Riemann integral by [A2] and [F12], while [F5] bounds that integral between $L_{N}$ and $U_{N}$ for every $N$ . Hence $\int_{[a, b]} 2 x d μ (x) = b^{2} - a^{2}$ .

4.1A2F0F1F3F8F9F11F13F14step 3.1algebra

Step 3.1 with $a = 0, b = 1$ gives $Q_{1} ([0, 1]) = 1$ , so $P_{1} : = Q_{1}$ is a probability measure by [F13]. Set $P_{0} : = μ$ and $p_{0} (x) : = 1$ ; for each $A \in A$ , [F14] gives $\int_{A} p_{0} d μ = μ (A)$ , so $p_{0}$ is a density of $P_{0}$ . By definition of $Q_{1}$ , $p_{1} (x) : = 2 x$ is a density of $P_{1}$ . Thus they define the experiment [F0], and their likelihood ratio is $R (x) = 2 x$ . The common measure $μ$ is finite and hence sigma-finite by [F11]. With $c = 3 / 2$ and $γ = 0$ , $P_{0} (R > c) = μ ((3 / 4, 1]) = 1 / 4$ and $P_{0} (R = c) = μ ({3 / 4}) = 0$ by [F1]. Thus [F9] gives the rejection region $x > 3 / 4$ and size $1 / 4$ .

4.2A2F1F3F8step 3.1algebra

The power is $P_{1} ((3 / 4, 1]) = \int_{[3 / 4, 1]} 2 x d μ (x) = 1 - (3 / 4)^{2} = 7 / 16$ by [F1], [F3], and step 3.1; the singleton boundary has zero measure.

5.1A1F10step 4.1step 4.2∎

Under AC [A1], the Neyman–Pearson lemma [F10] says no test with size at most $1 / 4$ has larger power.