Pipeline-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.

✓ 2 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 2 also cleared it.

Discrete test supermartingales and Ville

1 · Prerequisites

2 · Summary

This page proves a finite-horizon maximal bound for a nonnegative discrete-time test supermartingale, then passes to the infinite-horizon crossing and supremum bounds by continuity from below and approximation with lower thresholds. The argument uses bounded optional sampling and explicitly carries the Axiom of Choice required by the current conditional-expectation and optional-sampling suppliers. It applies under each law in the null family and controls threshold rejection at arbitrary stopping times. It makes no continuous-time claim. The supremum event and the finite crossing event are kept distinct when a path approaches a threshold without attaining it.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Finite-horizon crossing bound for a nonnegative test supermartingale

Statement

Assume AC. Let $P_{0}$ be a family of probability laws and let $M = (M_{t})_{t \in N_{0}}$ be a nonnegative test supermartingale for $P_{0}$ . For every $P \in P_{0}$ , every $a > 0$ , and every $N \in N_{0}$ , $P ⁣ (\max_{0 \leq t \leq N} M_{t} \geq a) \leq \frac{E_{P} M_{0}}{a} \leq \frac{1}{a} .$

Facts & Assumptions

Given: Assume AC. Let $P_{0}$ be a null family and let $M = (M_{t})_{t \geq 0}$ be a nonnegative test supermartingale for that family. Fix $P \in P_{0}$ , $a > 0$ , and a finite horizon $N \in N_{0}$ .

[F1]

Nonnegative test supermartingales: under every null law, $M$ is adapted and integrable, is nonnegative almost surely at every time, is a supermartingale, and satisfies $E_{P} M_{0} \leq 1$ .

[F2]

First hitting time of an adapted process is a stopping time: for an adapted process and a Borel set $B$ , its first time in $B$ is a stopping time.

[F3]

Discrete stopping time: a discrete stopping time is a map into $N_{0} \cup {\infty}$ whose events ${τ \leq n}$ belong to $F_{n}$ ; it is bounded when it is bounded almost surely by a deterministic integer.

[F4]

Optional sampling for bounded stopping times: for bounded stopping times $σ \leq τ$ , optional sampling for a supermartingale gives $E_{P} M_{τ} \leq E_{P} M_{σ}$ .

[F5]

Linearity, monotonicity, and the modulus bound for expectation and The expectation of an indicator is the probability of the event: expectation is monotone, and $E_{P} [1_{A}] = P (A)$ for measurable $A$ .

[A1]

AC is assumed by the test-supermartingale definition and the bounded optional-sampling theorem (The Axiom of Choice); it is used only through those suppliers.

Proof

1.1givenF1F2F3A1choose

Define $τ_{a} = \inf {t \geq 0 : M_{t} \geq a}$ , with $\inf \emptyset = \infty$ , and $A_{N} = {τ_{a} \leq N} = {\max_{0 \leq t \leq N} M_{t} \geq a}$ . By [F1], $M$ is adapted; applying [F2] with the Borel set $[a, \infty)$ makes $τ_{a}$ a stopping time. Thus $τ_{a} \land N$ and the constant time $0$ are bounded stopping times, with $0 \leq τ_{a} \land N$ .

2.1F1F4A1step 1.1

Apply [F4] to $0 \leq τ_{a} \land N$ to get $E_{P} M_{τ_{a} \land N} \leq E_{P} M_{0} \leq 1$ .

2.2F1step 1.1

On $A_{N}$ , $τ_{a} \land N = τ_{a}$ and $M_{τ_{a}} \geq a$ ; on $A_{N}^{c}$ , $τ_{a} \land N = N$ and $M_{N} \geq 0$ almost surely by [F1]. Hence $M_{τ_{a} \land N} \geq a 1_{A_{N}}$ almost surely.

3.1F5step 2.1step 2.2algebra∎

By [F5] and step 2.1, $a P (A_{N}) = E_{P} [a 1_{A_{N}}] \leq E_{P} M_{τ_{a} \land N} \leq E_{P} M_{0} \leq 1$ . Dividing by $a > 0$ proves both bounds.

Remarks

The finite-horizon event is exactly the first-crossing event by time $N$ . No assumption that an infinite-horizon supremum is attained is used here.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Discrete Ville inequality and anytime threshold validity

Statement

Assume AC. Let $P_{0}$ be a family of probability laws and let $M = (M_{t})_{t \in N_{0}}$ be a nonnegative test supermartingale for $P_{0}$ . For every $P \in P_{0}$ and $α \in (0, 1)$ , define $τ_{α} = \inf {t \geq 0 : M_{t} \geq 1 / α}, \inf \emptyset = \infty .$ Then $P ⁣ (\sup_{t \geq 0} M_{t} \geq \frac{1}{α}) \leq α, P (τ_{α} < \infty) \leq α .$ Moreover, for every discrete stopping time $σ$ , $P (σ < \infty, M_{σ} \geq 1 / α) \leq α,$ where the event involving $M_{σ}$ is restricted to ${σ < \infty}$ .

Facts & Assumptions

Given: Assume AC. Let $P_{0}$ be a null family, let $M$ be a nonnegative test supermartingale for it, and fix $P \in P_{0}$ and $α \in (0, 1)$ .

[F1]

Finite-horizon crossing bound for a nonnegative test supermartingale: for every $a > 0$ and finite $N$ , $P (\max_{0 \leq t \leq N} M_{t} \geq a) \leq 1 / a$ .

[F2]

Continuity from below for measures: if measurable events $A_{N}$ increase, then $P (⋃_{N} A_{N}) = \lim_{N} P (A_{N})$ .

[F3]

Nonnegative test supermartingales: under every null law, $M$ is adapted, integrable, nonnegative almost surely at every time, a supermartingale, and has $E_{P} M_{0} \leq 1$ .

[F4]

Discrete stopping time: for each $n$ , ${σ \leq n} \in F_{n}$ ; a stopping time takes values in $N_{0} \cup {\infty}$ .

[A1]

AC is the axiom used in [F1] through the test-supermartingale definition and bounded optional sampling (The Axiom of Choice).

Proof

1.1givenF1F3A1choose

For any $γ \in (0, 1)$ , set $τ_{γ} = \inf {t \geq 0 : M_{t} \geq 1 / γ}$ and $A_{N} = {τ_{γ} \leq N} = {\max_{0 \leq t \leq N} M_{t} \geq 1 / γ}$ . The events $A_{N}$ increase and their union is ${τ_{γ} < \infty} = {\exists t \geq 0 : M_{t} \geq 1 / γ}$ .

2.1F1F2step 1.1

By [F1], $P (A_{N}) \leq γ$ for each $N$ ; [F2] gives $P (τ_{γ} < \infty) = \lim_{N} P (A_{N}) \leq γ$ .

3.1givenF3step 2.1choosealgebra

Put $γ_{n} = α + (1 - α) / (n + 1)$ for $n \geq 1$ . Then $γ_{n} ↓ α$ and $1 / γ_{n} < 1 / α$ . The countable-supremum event $H = {\sup_{t \geq 0} M_{t} \geq 1 / α}$ equals $⋂_{n \geq 1} {τ_{γ_{n}} < \infty}$ : if the supremum is at least $1 / α$ , each strictly lower threshold $1 / γ_{n}$ is exceeded by some process value; conversely, crossing every such threshold forces the supremum to be at least their limit $1 / α$ . Thus $H$ is measurable and, by step 2.1, $P (H) \leq γ_{n}$ for every $n$ .

4.1step 2.1step 3.1algebra

Letting $n \to \infty$ in step 3.1 gives $P (H) \leq α$ . Taking $γ = α$ in step 2.1 also gives $P (τ_{α} < \infty) \leq α$ .

5.1F3F4step 4.1algebra∎

For a discrete stopping time $σ$ , ${σ < \infty, M_{σ} \geq 1 / α} = ⋃_{t \geq 0} ({σ = t} \cap {M_{t} \geq 1 / α}) \subseteq {τ_{α} < \infty}$ . The event is measurable by [F3]–[F4], and step 4.1 bounds its probability by $α$ .

Remarks

The all-time crossing event ${τ_{α} < \infty}$ and the supremum event ${\sup_{t} M_{t} \geq 1 / α}$ are not identified here. The proof uses lower thresholds for the supremum event because a supremum need not be attained.

5 · Examples, counterexamples and false statements

None yet.

Discrete test supermartingales and Ville

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Finite-horizon crossing bound for a nonnegative test supermartingale

Statement

Facts & Assumptions

Proof

Remarks

Discrete Ville inequality and anytime threshold validity

Statement

Facts & Assumptions

Proof

Remarks

5 · Examples, counterexamples and false statements

Sources