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.

✓ 3 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. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Empirical-Bernstein confidence sequences under adaptive sampling — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Repeated fixed-level tests do not give an all-times bound

Example

Let $U_{1}, U_{2}, \dots$ be independent random variables, each uniform on $[0, 1]$ , let $F_{t} = σ (U_{1}, \dots, U_{t})$ , and at every time $t \geq 1$ test the same null by rejecting when $U_{t} \leq α$ , for a fixed $α \in (0, 1)$ . Each single-time test has rejection probability $α$ , but for every integer $n \geq 2$ , the probability of at least one rejection by time $n$ is $1 - (1 - α)^{n} > α$ . Marginal level $α$ at each time therefore does not give the same $α$ bound for the event of ever rejecting.

Facts & Assumptions

Given: The probability space carries the independent $[0, 1]$ -uniform random variables in the Example.

[A1]

The variables $U_{1}, U_{2}, \dots$ are mutually independent and each satisfies $P (U_{t} \leq x) = x$ for $0 \leq x \leq 1$ .

Verification

1.1givenA1

For every $t \geq 1$ , [A1] gives $P (U_{t} \leq α) = α$ , so the test at that fixed time has level $α$ .

1.2givenA1algebra

Independence in [A1] gives $P (U_{t} > α for all 1 \leq t \leq n) = \prod_{t = 1}^{n} P (U_{t} > α) = (1 - α)^{n}$ . Taking the complement, $P (\exists t \leq n : U_{t} \leq α) = 1 - (1 - α)^{n}$ .

2.1givenA1step 1.2algebra∎

For $n \geq 2$ , $1 - (1 - α)^{n} = α + (1 - α) (1 - (1 - α)^{n - 1}) > α$ , since both factors in the added term are positive. Thus the pointwise error bounds do not supply the same bound for all tests through time $n$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A predictable linear forecast and its empirical residual process

Example

Assume AC, fix $δ \in (0, 1)$ , and choose a Borel one-sided sub-exponential uniform boundary $u_{δ / 2, 1}$ with crossing probability $δ / 2$ at scale $1$ . Let $X_{1}, X_{2}, \dots$ be independent Bernoulli random variables with success probability $1 / 4$ , set $X_{0} = 0$ , and let $F_{0} = {\emptyset, Ω}$ and $F_{t} = σ (X_{1}, \dots, X_{t})$ . Use the predictable linear forecast ${\hat{X}}_{t} = 1 / 4 + (1 / 2) X_{t - 1}$ . Then ${\hat{X}}_{t} \in [0, 1]$ and $E [X_{t} ∣ F_{t - 1}] = 1 / 4$ almost surely. On the path $(X_{1}, X_{2}, X_{3}, X_{4}) = (1, 0, 0, 1)$ , which has probability $9 / 256$ , the algorithm has ${\overset{ˉ}{X}}_{4} = 1 / 2$ , $V_{4} = 7 / 4$ , and returns $C_{4} = [\frac{1}{2} - \frac{u_{δ / 2, 1} (7 / 4)}{4}, \frac{1}{2} + \frac{u_{δ / 2, 1} (7 / 4)}{4}] .$ The forecast is predictable and differs from the conditional mean when $X_{t - 1} = 1$ ; the full interval sequence still covers its target sequence with probability at least $1 - δ$ .

Example references

The one-sided boundary input and its crossing guarantee

The streaming interval update

The all-times coverage theorem

Facts & Assumptions

Given: Assume AC. The Bernoulli stream, filtration, forecast, error level, boundary, algorithm, and target sequence in the Example.

[F1]

Conditional expectation given a sigma algebra: a conditional-expectation version is measurable and has the defining event integrals.

[F2]

Conditional expectation is unique almost surely: conditional-expectation versions with the same input and conditioning sigma-algebra agree almost surely.

[F3]

Empirical-Bernstein confidence-sequence interval update: at time $t$ , the output is centered at ${\overset{ˉ}{X}}_{t}$ with radius $u_{δ / 2, 1} (V_{t}) / t$ .

[F4]

Empirical-Bernstein confidence sequence under adaptive sampling: for these bounded observations and predictable forecasts, the intervals cover the running average conditional-mean target at all times with probability at least $1 - δ$ .

[A1]

The Axiom of Choice: AC is explicitly assumed here and by the coverage theorem; the definition of a conditional-expectation version imposes no AC assumption.

Verification

1.1givenF1F2

For each $t$ , the atoms of $F_{t - 1}$ are the events $A_{x} = {(X_{1}, \dots, X_{t - 1}) = x}$ , with $A = Ω$ for $t = 1$ . Each atom has positive probability, and independence gives $P (X_{t} = 1, A_{x}) = \frac{1}{4} P (A_{x})$ and $P (X_{t} = 0, A_{x}) = \frac{3}{4} P (A_{x})$ . Thus the constant $1 / 4$ has the defining event integrals on every atom and every union of atoms, so it is a version of $E [X_{t} ∣ F_{t - 1}]$ by [F1]; [F2] identifies it with the chosen conditional-expectation class.

2.1givenstep 1.1algebra

The forecast ${\hat{X}}_{t}$ is a function of $X_{t - 1}$ , hence $F_{t - 1}$ -measurable, and its values are $1 / 4$ or $3 / 4$ ; when $X_{t - 1} = 1$ it equals $3 / 4$ , not the conditional mean $1 / 4$ . On the specified path, the four squared errors are $9 / 16, 9 / 16, 1 / 16, 9 / 16$ , so $V_{4} = 28 / 16 = 7 / 4$ and ${\overset{ˉ}{X}}_{4} = 2 / 4 = 1 / 2$ . Independence gives the path probability $(1 / 4) (3 / 4) (3 / 4) (1 / 4) = 9 / 256$ .

3.1givenF3F4A1step 1.1algebra∎

By [F3], the algorithm returns the displayed interval at time $4$ . Its hypotheses hold with $a = 0$ , $b = 1$ ; therefore [F4] gives $P (μ_{t} \in C_{t} for every t \geq 1) \geq 1 - δ$ . In particular, using [A1], the interval sequence is a confidence sequence for the adapted target process defined in the Example.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Diagonal scalar bounds miss off-diagonal matrix size

Example

Assume AC and fix $δ \in (0, 1)$ . For each real $r > 0$ , let $A_{t} = A^{(r)} = (\begin{array}{cc} 0 & r \\ r & 0 \end{array})$ for every $t \geq 1$ . Define the Euclidean operator norm by $∥ A ∥_{o p} = \sup_{∥ x ∥_{2} = 1} ∥ A x ∥_{2}$ , where $∥ x ∥_{2} = \sqrt{x_{1}^{2} + x_{2}^{2}}$ . Both diagonal entry streams are identically zero; with scalar bounds $a = b = 0$ and the constant predictable forecasts ${\hat{X}}_{t} = 0$ , the scalar theorem returns $[0, 0]$ for both coordinates at every time, independently of $r$ . Yet $∥ A^{(r)} ∥_{o p} = r$ , which is unbounded across this family. An operator-norm confidence sequence at level $1 - δ$ consists of matrix estimates ${\hat{A}}_{t}$ and almost-surely finite nonnegative radii $R_{t}$ satisfying $P (∥ A_{t} - {\hat{A}}_{t} ∥_{o p} \leq R_{t} for every t) \geq 1 - δ$ . Any rule using only the two diagonal interval streams (and, if randomized, auxiliary randomness whose law is independent of $r$ ) has the same time-one output law for every $r$ . Such a rule cannot have the stated coverage uniformly over this family. A matrix-valued conclusion needs separate assumptions and an argument for the matrix process.

Example references

The scalar theorem's domain and interval guarantee

Facts & Assumptions

Given: Assume AC and fix $δ \in (0, 1)$ . The deterministic symmetric matrix family and any estimation rule restricted to its diagonal interval streams, with auxiliary randomness independent of $r$ , are as in the Example.

[F1]

Empirical-Bernstein confidence sequence under adaptive sampling: with bounded observations and predictable forecasts, the theorem gives simultaneous coverage for the running scalar conditional-mean target.

[F2]

Empirical-Bernstein confidence-sequence interval update: when $a = b$ , the update returns $[a, a]$ at every time.

[F3]

Continuity from above when one set has finite measure: for decreasing measurable sets under a finite measure, their measures converge to the measure of their intersection.

[A1]

The Axiom of Choice: AC is explicitly assumed by the scalar theorem.

Verification

1.1givenF1F2A1

For every $r > 0$ , each diagonal entry of $A^{(r)}$ is the constant zero. With scalar bounds $a = b = 0$ and forecast ${\hat{X}}_{t} = 0$ , each coordinate process satisfies the theorem's hypotheses; [F2] gives the returned interval $[0, 0]$ at every time, independently of $r$ .

1.2givenalgebra

For every vector $x \in R^{2}$ , $(A^{(r)})^{T} A^{(r)} = r^{2} I$ gives $∥ A^{(r)} x ∥_{2}^{2} = r^{2} ∥ x ∥_{2}^{2}$ , hence $∥ A^{(r)} ∥_{o p} = r$ .

2.1givenF3step 1.2algebra∎

Let $({\hat{A}}_{1}, R_{1})$ have the common time-one output law from the Example, with $R_{1}$ finite almost surely. For each integer $n \geq 1$ , the reverse triangle inequality gives $P (∥ A^{(n)} - {\hat{A}}_{1} ∥_{o p} \leq R_{1}) \leq P (∥ {\hat{A}}_{1} ∥_{o p} + R_{1} \geq n)$ . The events on the right decrease to the null event where a finite random variable is infinite; [F3] makes their probabilities tend to zero. Since $1 - δ > 0$ , some $n$ has time-one coverage probability below $1 - δ$ , and the all-times event is contained in the time-one event. Thus no such rule gives uniform coverage over the family.