Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

The likelihood-ratio rule is a measurable test of exact size

Statement

In the setup of Likelihood-ratio tests with boundary randomization, for every α∈[0,1] the candidate rejection function φα∗ is measurable into [0,1], defines a randomized test, and has size exactly α for the simple null P0.

Facts & Assumptions

Given: The common-dominator two-law experiment, specified density representatives p0,p1, and α∈[0,1]. The proof uses only these fixed representatives.

[F1]

Likelihood-ratio tests with boundary randomization and Likelihood densities: p0,p1 are finite, nonnegative measurable densities; the candidate is 1U at α=0 and 1U+1A+γ1B at α>0, where U={p0=0<p1}, A={p0>0,R>c}, and B={p0>0,R=c}; in the latter case c≥0, 0≤γ≤1, and P0(R>c)+γP0(R=c)=α.

[F2]

The common-support likelihood ratio is measurable: R is finite, nonnegative, and measurable.

[F3]

A measurable function between measurable spaces: preimages of Borel sets under p0,p1,R are measurable.

[F4]

Closure properties of measurable functions used by the integral: finite sums and real scalar multiples of measurable functions are measurable.

[F5]

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

[F7]

Nonnegative simple measurable functions, The integral of a nonnegative simple function, and The nonnegative integral agrees with the simple integral on simple functions: the integral of a finite-valued nonnegative simple function is the sum of its values times the measures of their disjoint level sets.

[F8]

Measures are monotone: a measurable subset of a measurable P0-null set is P0-null.

[F9]

Expectation of a nonnegative or integrable random variable and Probability measures and probability spaces: EP0 is integration under the probability measure P0.

[F10]

Test size and power: for the simple null {0}, size is the expectation of the rejection function under P0.

Proof

technique · direct
1.1F1F2F3F4

The sets U,A,B in [F1] are measurable by [F2] and [F3]. For α>0 they are pairwise disjoint, so [F4] makes φα∗=1U+1A+γ1B measurable; for α=0, [F4] makes 1U measurable.

1.2F1F6F7F8algebra

Let N={p0=0}. By [F1], [F6], and the zero-function case of [F7], P0(N)=∫Np0 dμ=0, since p0 vanishes on N. Thus P0(U)=0 by [F8].

2.1F1F5step 1.1algebra

The disjointness and 0≤γ≤1 show that every value of φα∗ lies in [0,1]. Hence [F5] makes it a randomized test.

2.2F1F7F9F10step 1.2

If α=0, [F1] gives φ0∗=1U. The simple integral identity [F7] and [F9] give EP0[φ0∗]=P0(U)=0, so [F10] makes its size 0=α.

3.1F1F7F9F10step 1.2algebra∎

Suppose α>0. Since R=0 on N and c≥0, A={R>c}. Also B={R=c} when c>0; when c=0, the two sets differ only by N. Step 1.2 makes that difference P0-null. The three disjoint indicator terms in [F1] therefore have expectation P0(R>c)+γP0(R=c)=α by [F7], [F9], and the threshold equation in [F1]. By [F10], the test has size α.

Depends on

Used by

Dependency tree · two levels

49 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