TheoremStatement: Literature-sourcedProof: 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.

Iid drift conditions imply almost-sure test termination

Statement

Assume AC. Let $(X_{i})_{i \geq 1}$ be IID under each of two probability measures $P_{j}$ , with one-coordinate law $Q_{j}$ , and suppose $Q_{0}$ and $Q_{1}$ are equivalent. Choose a finite strictly positive representative $λ = d Q_{1} / d Q_{0}$ and set $Z = \log λ$ . If $E_{Q_{0}} ∣ Z ∣, E_{Q_{1}} ∣ Z ∣ < \infty, E_{Q_{0}} Z < 0 < E_{Q_{1}} Z,$ then for every $α, β \in (0, 1)$ the algorithm Sequential likelihood-ratio test, with $F_{0} = {\emptyset, Ω}$ and $F_{t} = σ (X_{1}, \dots, X_{t})$ , satisfies $P_{0} (τ < \infty) = P_{1} (τ < \infty) = 1.$

Facts & Assumptions

Given: Assume AC. Under $P_{j}$ , the observations $X_{i}$ are IID with common law $Q_{j}$ , the one-observation laws are equivalent, and the log likelihood increment $Z = \log (d Q_{1} / d Q_{0}) (X_{1})$ is integrable under both laws with strictly negative $Q_{0}$ mean and strictly positive $Q_{1}$ mean. The algorithm uses fixed $α, β \in (0, 1)$ .

[A1]

The Axiom of Choice: AC states that every family of nonempty sets has a choice function and is assumed by the local Radon–Nikodym convention.

[F1]

Identical distribution and IID families: IID means mutual independence together with a common one-coordinate law.

[F2]

Measurable coordinatewise functions preserve independence: applying the same measurable real function to IID observations preserves independence; the resulting variables have the common pushforward law.

[F3]

Kolmogorov iid l1 strong law: for IID integrable real variables, their sample mean converges almost surely to the expectation.

[F4]

Law or distribution of a random element: $Q_{j}$ is the pushforward law of one observation under $P_{j}$ .

[F5]

Likelihood ratio as a Radon–Nikodym derivative and Likelihood-ratio change of measure: an absolutely continuous probability law has a nonnegative RN density, finite almost surely; its integral over a set is the probability of that set under the changed law.

[F6]

Finite-sample likelihood ratio for iid observations: under IID observations, the finite-time density process is $L_{t} = \prod_{i = 1}^{t} λ (X_{i})$ .

[F7]

Sequential likelihood-ratio test: the procedure stops upon crossing $1 / α$ above or $β$ below, and otherwise continues.

[F8]

Continuous functions on Euclidean spaces are Borel measurable: under countable choice, a continuous map from $R^{n}$ to $R^{m}$ is Borel measurable for $n, m \geq 1$ . This corollary does not itself cover $\log : (0, \infty) \to R$ ; step 1.1 verifies measurability on that subspace directly.

[F9]

Composition with a Borel measurable outer map preserves measurability: composing a measurable map with a Borel map gives a measurable map.

[F10]

Change of variables for expectation: if $X_{i}$ has law $Q_{j}$ and $Z$ is measurable, then $E_{P_{j}} ∣ Z (X_{i}) ∣ = E_{Q_{j}} ∣ Z ∣$ and, when these are finite, $E_{P_{j}} Z (X_{i}) = E_{Q_{j}} Z$ .

Proof

1.1A1F4F5F8F9givenconstruct

Let $r$ be any nonnegative RN representative of $Q_{1}$ with respect to $Q_{0}$ . Since $\int r d Q_{0} = 1$ , the set where $r = \infty$ is $Q_{0}$ -null and hence $Q_{1}$ -null. On $A = {r = 0}$ the change-of-measure identity [F5] gives $Q_{1} (A) = \int_{A} r d Q_{0} = 0$ ; equivalence $Q_{0} ≪ Q_{1}$ then makes $A$ $Q_{0}$ -null too. Replacing $r$ by $1$ on these common null sets yields a finite strictly positive measurable representative $λ$ of the same density class. Its range lies in $(0, \infty)$ , so it is measurable into that subspace with its Borel sigma-algebra ${B \cap (0, \infty) : B \in B (R)}$ . Although the logarithm is continuous on this subspace, [F8] only covers Euclidean domains. For every open $U \subseteq R$ , $\log^{- 1} (U)$ is open in $(0, \infty)$ and therefore Borel there; since open sets generate $B (R)$ , $\log : (0, \infty) \to R$ is Borel measurable. Thus [F9] makes $Z = \log \circ λ$ real-valued and measurable.

1.2F1F2F3F10given

For each $j$ , the variables $Z_{i} : = Z (X_{i})$ are IID under $P_{j}$ : measurability gives the same pushforward law for all coordinates, and [F2] preserves their independence. The change-of-variables identity [F10] gives $E_{P_{j}} ∣ Z_{i} ∣ = E_{Q_{j}} ∣ Z ∣ < \infty$ and $E_{P_{j}} Z_{i} = μ_{j} : = E_{Q_{j}} Z$ . Thus [F3] gives $t^{- 1} \sum_{i = 1}^{t} Z_{i} \to μ_{j}$ almost surely under $P_{j}$ .

2.1F5F6step 1.1

Put $G_{t} = \prod_{i = 1}^{t} λ (X_{i})$ . By [F6], $G_{t}$ is a version of the finite-time density, so the algorithm's chosen representative $L_{t}$ equals $G_{t}$ $P_{0}$ -almost surely by uniqueness of Radon–Nikodym derivatives. The representative $λ$ is finite and strictly positive $Q_{0}$ -almost surely; equivalence of $Q_{0}, Q_{1}$ gives the same under $Q_{1}$ . Thus $G_{t}$ is finite and strictly positive $P_{0}$ -almost surely, and for $A \in F_{t}$ , $P_{1} (A) = \int_{A} G_{t} d P_{0}$ implies $P_{1} (A) = 0$ exactly when $P_{0} (A) = 0$ . The finite-time restrictions are therefore equivalent, so $L_{t} = G_{t}$ also $P_{1}$ -almost surely. Intersecting these probability-one events over countably many $t$ gives one event under each law on which the equalities hold for every $t$ . Positivity of $λ$ there yields $\log L_{t} = \sum_{i = 1}^{t} Z_{i}$ .

3.1F7step 1.2step 2.1givenalgebra

Under $P_{0}$ , steps 1.2 and 2.1 give $\log L_{t} / t \to μ_{0} < 0$ , hence $\log L_{t} \to - \infty$ . Since $\log β$ is finite, some finite $t$ satisfies $L_{t} \leq β$ , so the lower boundary has been crossed and the algorithm has $τ < \infty$ .

4.1F7step 1.2step 2.1givenalgebra∎

Under $P_{1}$ , steps 1.2 and 2.1 give $\log L_{t} / t \to μ_{1} > 0$ , hence $\log L_{t} \to + \infty$ . Since $\log (1 / α)$ is finite, some finite $t$ satisfies $L_{t} \geq 1 / α$ , so the upper boundary has been crossed and $τ < \infty$ . This proves almost-sure termination under both laws, without a claim about $E_{P_{j}} τ$ .

Source notes

Wolpert §1.2, PDF p. 4, writes the iid log likelihood as a sum of iid increments. Durrett Theorem 2.4.1, printed pp. 76–78, proves the L1 strong law by truncation. The local proof uses the actual published Kolmogorov iid L1 strong-law supplier; no finite-variance strengthening is assumed.

Depends on

Used by

Exact Bernoulli crossings in a sequential likelihood-ratio test Example

Dependency tree · two levels

58 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

Robert L. Wolpert, Introduction to Martingales, STA 711 course notes, §1.2, PDF p. 4 (standard reference, not scraped)
Rick Durrett, Probability: Theory and Examples, 5th ed., §2.4, Theorem 2.4.1 and proof, printed pp. 76–78 (standard reference, not scraped)