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

The common-support likelihood ratio is measurable

Statement

Let $p_{0}, p_{1} : X \to [0, \infty)$ be finite-valued measurable functions on a measurable space $(X, A)$ . Define $R (x) = {\begin{cases} p_{1} (x) / p_{0} (x), & p_{0} (x) > 0, \\ 0, & p_{0} (x) = 0. \end{cases}$ Then $R$ is finite-valued, nonnegative, and measurable.

Facts & Assumptions

Given: Finite-valued nonnegative measurable functions $p_{0}, p_{1}$ .

[F1]

Likelihood densities: the selected density representatives are finite-valued, nonnegative, and measurable.

[F2]

A measurable function between measurable spaces: inverse images of Borel sets under a measurable function are measurable.

[F3]

Threshold characterisations of real-valued and extended-real-valued measurability: a real-valued function is measurable if all of its strict superlevel sets are measurable.

[F4]

Arithmetic and lattice operations preserve measurability whenever they are defined: the product of two finite real-valued measurable functions is measurable.

Proof

technique · direct

1.1F1F2F3given

Define $h (x) = 1 / p_{0} (x)$ when $p_{0} (x) > 0$ and $h (x) = 0$ when $p_{0} (x) = 0$ . It is finite and nonnegative. For $t < 0$ , ${h > t} = X$ ; for $t = 0$ , ${h > t} = {p_{0} > 0}$ ; for $t > 0$ , ${h > t} = {0 < p_{0} < 1 / t}$ . Each set is measurable by [F1] and [F2], so [F3] makes $h$ measurable.

2.1F1F4step 1.1algebra∎

By [F1] and step 1.1, $p_{1} h$ is a finite nonnegative measurable function by [F4]. On ${p_{0} > 0}$ it equals $p_{1} / p_{0}$ , and on ${p_{0} = 0}$ it is zero. Hence $R = p_{1} h$ and has all the asserted properties.

Depends on

Used by

Dependency tree · two levels

21 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

George Deligiannidis, SB2.1 Foundations of Statistical Inference, Chapter 13, §13.1.2, PDF p. 77 (standard reference, not scraped)
Anna Mikusheva, MIT 14.381 Lecture 9: Uniformly Most Powerful Tests, PDF pp. 2–3 (standard reference, not scraped)