TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Terminal error bounds for a sequential likelihood-ratio test

Statement

Assume AC. Under the hypotheses of Sequential likelihood-ratio test, the boundary rule $τ$ is a stopping time and, for the specified decisions, $P_{0} (τ < \infty, L_{τ} \geq 1 / α) \leq α, P_{1} (τ < \infty, L_{τ} \leq β) \leq β .$ These bounds concern terminal errors and do not assume that $τ$ is finite almost surely.

Facts & Assumptions

Given: Assume AC. Let $P_{0}, P_{1}$ be probability measures on $(Ω, F)$ with a common discrete filtration $(F_{t})_{t \geq 0}$ , equivalent restrictions at each finite $t$ , and likelihood-ratio density representatives $L_{t} = d (P_{1} ∣_{F_{t}}) / d (P_{0} ∣_{F_{t}})$ . Let $α, β \in (0, 1)$ and let $τ$ and the terminal decisions be as in the algorithm.

[A1]

The Axiom of Choice: AC states that every family of nonempty sets has a choice function; the supplied likelihood-ratio and conditional-expectation constructions use AC.

[F1]

Probability measures and probability spaces: each $P_{j}$ is a probability measure, so $P_{j} (Ω) = 1$ .

[F2]

Sequential likelihood-ratio test: the rule stops at the first $t \geq 1$ with $L_{t} \geq 1 / α$ or $L_{t} \leq β$ , decides $H_{1}$ at the upper boundary and $H_{0}$ at the lower.

[F3]

Likelihood ratio as a Radon–Nikodym derivative: $L_{t}$ is a nonnegative measurable representative of the finite-time Radon–Nikodym density.

[F4]

Likelihood-ratio change of measure: if $P_{1} ∣_{F_{t}} ≪ P_{0} ∣_{F_{t}}$ , then $\int g L_{t} d P_{0} = \int g d P_{1}$ on $F_{t}$ for every nonnegative measurable $g$ .

[F5]

Filtration and filtered probability space and Adapted and integrable stochastic process: $F_{t}$ is increasing, and an adapted process has each $L_{t}$ measurable with respect to $F_{t}$ .

[F6]

Conditional expectation given a sigma algebra: a conditional-expectation version is integrable, measurable with respect to the conditioning sigma-algebra, and has the same integrals on its events.

[F7]

Conditional expectation exists by radon nikodym: under AC, conditional-expectation versions exist for integrable random variables and sub-sigma-algebras.

[F8]

Conditional expectation is unique almost surely: two versions with the same event integrals agree almost surely.

[F9]

Conditional expectation as an ae class and Martingale submartingale and supermartingale: the martingale condition is the almost-sure conditional-expectation identity at each adjacent time.

[F10]

Nonnegative test supermartingales: for a singleton null family, a nonnegative adapted integrable martingale with initial expectation at most one is a test supermartingale.

[F11]

Ville's inequality for nonnegative test supermartingales: for such a process $M_{t}$ and $c \in (0, 1)$ , $P (\sup_{t \geq 0} M_{t} \geq 1 / c) \leq c$ .

[F12]

Discrete stopping time: $τ$ is a stopping time when ${τ \leq n} \in F_{n}$ for each $n \geq 0$ .

Proof

1.1A1F1F2F3F4F5

Each $L_{t}$ is nonnegative by [F3] and $F_{t}$ -measurable by [F2]. Applying [F4] with $g = 1$ gives $E_{P_{0}} L_{t} = P_{1} (Ω) = 1$ for every $t \geq 0$ , so ${L_{t} = \infty}$ is $P_{0}$ -null. Define $M_{t} = L_{t}$ where $L_{t} < \infty$ and $M_{t} = 0$ otherwise. This modification on an $F_{t}$ -measurable null set preserves the density class. Thus $M$ is a real-valued nonnegative adapted process with $E_{P_{0}} M_{t} = 1$ , and each $M_{t}$ has the same density event integrals as $L_{t}$ .

1.2F2F5F12

For $n \geq 1$ , ${τ \leq n} = ⋃_{t = 1}^{n} ({L_{t} \geq 1 / α} \cup {L_{t} \leq β}) \in F_{n}$ , because each $L_{t}$ is $F_{t}$ -measurable and the filtration is increasing; ${τ \leq 0} = \emptyset$ . Hence [F12] makes $τ$ a stopping time.

2.1A1F2F4F6F7F8F9step 1.1

Fix $t \geq 1$ and $A \in F_{t - 1}$ . Since $A \in F_{t}$ , [F4] applied to the density representatives $M_{t}$ and $M_{t - 1}$ gives $E_{P_{0}} [1_{A} M_{t}] = P_{1} (A) = E_{P_{0}} [1_{A} M_{t - 1}]$ . By [F7], choose a version $Y_{t}$ of $E_{P_{0}} [M_{t} ∣ F_{t - 1}]$ . Its defining event-integral identities [F6] show that $Y_{t}$ and $M_{t - 1}$ are versions of that conditional expectation; [F8] makes them equal almost surely. Thus $M$ is a nonnegative $P_{0}$ -martingale by [F9].

2.2A1F2F3F4F5step 1.1

For each $t \geq 0$ , step 1.1 and equivalence of the restrictions give $P_{0} (L_{t} = \infty) = P_{1} (L_{t} = \infty) = 0$ . Moreover, [F4] gives $P_{1} (L_{t} = 0) = \int_{{L_{t} = 0}} L_{t} d P_{0} = 0$ , so equivalence gives $P_{0} (L_{t} = 0) = 0$ . Thus $N_{t} = {L_{t} = 0} \cup {L_{t} = \infty} \in F_{t}$ is null under both laws. Define the real nonnegative $R_{t} = 1 / L_{t}$ where $0 < L_{t} < \infty$ and set it to $0$ on $N_{t}$ . It is $F_{t}$ -measurable, and $R_{t} M_{t} = 1$ off $N_{t}$ . Applying [F4] with density $M_{t}$ and $g = 1_{A} R_{t}$ for $A \in F_{t}$ gives $E_{P_{1}} [1_{A} R_{t}] = E_{P_{0}} [1_{A} R_{t} M_{t}] = P_{0} (A)$ , so $R_{t}$ is integrable with mean one.

3.1A1F2F6F7F8F9step 2.2

For $t \geq 1$ and $A \in F_{t - 1}$ , step 2.2 at times $t$ and $t - 1$ gives $E_{P_{1}} [1_{A} R_{t}] = P_{0} (A) = E_{P_{1}} [1_{A} R_{t - 1}]$ . Existence [F7], the defining conditional-expectation identity [F6], and uniqueness [F8] identify $E_{P_{1}} [R_{t} ∣ F_{t - 1}] = R_{t - 1}$ almost surely. Thus $R$ is a nonnegative $P_{1}$ -martingale by [F9].

4.1A1F10F11step 1.1step 2.1step 2.2step 3.1

By steps 1.1 and 2.1, $M$ is a real nonnegative martingale under $P_{0}$ with $E_{P_{0}} M_{0} = 1$ ; by [F10] it is a nonnegative test supermartingale for the singleton null ${P_{0}}$ . By steps 2.2 and 3.1, $R$ is a real nonnegative test supermartingale for ${P_{1}}$ . Applying [F11] gives $P_{0} (\sup_{t \geq 0} M_{t} \geq 1 / α) \leq α$ and $P_{1} (\sup_{t \geq 0} R_{t} \geq 1 / β) \leq β$ .

5.1F2step 1.1step 1.2step 2.2step 4.1algebra∎

The measurable set $N = ⋃_{t \geq 0} N_{t}$ is null under both laws by countable subadditivity. Outside $N$ , simultaneously for every $t$ , $M_{t} = L_{t}$ and $R_{t} = 1 / L_{t}$ . Hence the terminal $H_{1}$ event is contained in $N \cup {\sup_{t \geq 0} M_{t} \geq 1 / α}$ , and the terminal $H_{0}$ event is contained in $N \cup {\sup_{t \geq 0} R_{t} \geq 1 / β}$ . These terminal events are measurable countable unions of ${τ = t}$ intersected with the corresponding boundary events. Since $P_{0} (N) = P_{1} (N) = 0$ , step 4.1 proves both terminal-error inequalities.

Source notes

Wolpert §1.2, PDF p. 4, gives the iid likelihood-ratio process and exact martingale maximal-inequality error control. His commonly quoted Wald boundary formulas and expected sample-size expressions are approximate and are not used here. Howard et al., Lemma 1 and its proof (PDF pp. 15 and 45), prove the nonnegative-supermartingale crossing bound through bounded stopping and a limiting argument. The local proof uses the published Ville supplier and does not apply optional stopping at the possibly unbounded $τ$ .

Depends on

Used by

Exact Bernoulli crossings in a sequential likelihood-ratio test Example

Dependency tree · two levels

45 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 pp. 4–5 (standard reference, not scraped)
Steven R. Howard, Aaditya Ramdas, Jon McAuliffe and Jasjeet Sekhon, Time-uniform Chernoff bounds via nonnegative supermartingales, Probability Surveys 17 (2020), Lemma 1 and proof, PDF pp. 15 and 45 (standard reference, not scraped)