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

Mixtures of null test supermartingales

Statement

Assume AC. Let $(Λ, A, π)$ be a probability space and let $P_{0}$ be a family of laws on a common discrete filtered measurable space $(Ω, F, (F_{t})_{t \geq 0})$ . For each $λ \in Λ$ , let $E^{λ} = (E_{t}^{λ})_{t \geq 0}$ be a nonnegative test supermartingale for $P_{0}$ . Suppose that, for every $t$ , the map $(λ, ω) \mapsto E_{t}^{λ} (ω)$ is measurable with respect to $A \otimes F_{t}$ . Before mixing, take its pointwise nonnegative version $E_{t}^{λ, +} (ω) = \max {E_{t}^{λ} (ω), 0}$ , and define ${\overline{E}}_{t} (ω) = \int_{Λ} E_{t}^{λ, +} (ω) π (d λ), {\tilde{E}}_{t} (ω) = {\begin{cases} {\overline{E}}_{t} (ω), & {\overline{E}}_{t} (ω) < \infty, \\ 0, & {\overline{E}}_{t} (ω) = \infty . \end{cases}$ Then $\tilde{E} = ({\tilde{E}}_{t})_{t \geq 0}$ is a nonnegative test supermartingale for $P_{0}$ . The modification on the infinite-integral set makes a real-valued version common to all null laws.

Facts & Assumptions

Given: Assume AC. Let $π$ , $P_{0}$ , and the product-measurable family of component test supermartingales satisfy the Statement. If $P_{0}$ is empty, its lawwise conclusion is vacuous; otherwise fix any $P \in P_{0}$ when checking the test-supermartingale conditions.

[F1]

Nonnegative test supermartingales: under each $P \in P_{0}$ , every component is nonnegative, adapted, integrable, a supermartingale, and has initial expectation at most one.

[F2]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: for a nonnegative product-measurable function, section integrals are measurable and the product integral equals either iterated integral.

[F3]

Optional sampling for bounded stopping times: under AC, bounded stopping of a supermartingale gives a downward expectation inequality; deterministic times are bounded stopping times.

[F4]

Conditional expectation as an ae class: under AC, the conditional-expectation class exists and is represented by conditional-expectation versions.

[F5]

Conditional expectation given a sigma algebra: a conditional-expectation version is measurable and has the same integral as the original variable on every event in the conditioning sigma-algebra.

[A1]

The Axiom of Choice: AC supplies conditional-expectation classes used in the supermartingale and optional-sampling clauses.

Proof

1.1F1F2F3A1

Fix $P \in P_{0}$ and $t \geq 0$ . For every $λ$ , $P (E_{t}^{λ} \geq 0) = 1$ , so $E_{t}^{λ, +} = E_{t}^{λ}$ $P$ -almost surely and has the same expectation. Apply F3 at the deterministic times $0$ and $t$ to get $E_{P} E_{t}^{λ, +} = E_{P} E_{t}^{λ} \leq E_{P} E_{0}^{λ} = E_{P} E_{0}^{λ, +} \leq 1$ . The pointwise nonnegative map $(λ, ω) \mapsto E_{t}^{λ, +} (ω)$ is product-measurable; Tonelli F2 makes ${\overline{E}}_{t}$ $F_{t}$ -measurable and gives $E_{P} {\overline{E}}_{t} = \int_{Λ} E_{P} E_{t}^{λ, +} π (d λ) \leq 1$ . Hence $N_{t} = {{\overline{E}}_{t} = \infty} \in F_{t}$ is null under every $P \in P_{0}$ . The common modification ${\tilde{E}}_{t} = {\overline{E}}_{t}$ off $N_{t}$ and $0$ on $N_{t}$ is finite, adapted, nonnegative and integrable under every null law, with $E_{P} {\tilde{E}}_{0} \leq 1$ .

2.1F1F2F4F5A1step 1.1

Fix $P \in P_{0}$ , $t \geq 1$ , and $A \in F_{t - 1}$ . Since $E_{s}^{λ, +} = E_{s}^{λ}$ $P$ -almost surely for $s = t - 1, t$ , the component supermartingale condition and the event-integral identity F5 give $\int_{A} E_{t}^{λ, +} d P = \int_{A} E_{t}^{λ} d P \leq \int_{A} E_{t - 1}^{λ} d P = \int_{A} E_{t - 1}^{λ, +} d P$ for every $λ$ . Tonelli F2 integrates these inequalities over $π$ ; since $N_{t}$ and $N_{t - 1}$ are $P$ -null, replacing the mixtures by ${\tilde{E}}_{t}$ and ${\tilde{E}}_{t - 1}$ does not change these integrals. Thus $\int_{A} {\tilde{E}}_{t} d P \leq \int_{A} {\tilde{E}}_{t - 1} d P$ .

3.1F4F5A1step 2.1∎

Let $U = E_{P} [{\tilde{E}}_{t} ∣ F_{t - 1}]$ , which exists by F4 and AC A1. For every $A \in F_{t - 1}$ , the event-integral identity F5 and step 2.1 give $\int_{A} (U - {\tilde{E}}_{t - 1}) d P \leq 0$ . Take $A = {U > {\tilde{E}}_{t - 1}}$ . If $P (A) > 0$ , then for some integer $m \geq 1$ the subset where $U - {\tilde{E}}_{t - 1} \geq 1 / m$ has positive measure, making that integral strictly positive, a contradiction. Therefore $U \leq {\tilde{E}}_{t - 1}$ almost surely. As $P$ and $t$ were arbitrary, $\tilde{E}$ is a test supermartingale for $P_{0}$ .

Depends on

Used by

The Gaussian mixture is a sub-Gaussian test supermartingale Theorem

Dependency tree · two levels

25 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

Steven R. Howard, Aaditya Ramdas, Jon McAuliffe and Jasjeet Sekhon, Time-Uniform, Nonparametric, Nonasymptotic Confidence Sequences, Lemma 2 and Appendix A.3 (standard reference, not scraped)
Aaditya Ramdas, Peter Grunwald, Vladimir Vovk and Glenn Shafer, Game-Theoretic Statistics and Safe Anytime-Valid Inference, §§2.3-2.4 (standard reference, not scraped)