Alphabeta Math
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.

Empirical-Bernstein confidence sequence under adaptive sampling

Statement

Assume the Axiom of Choice. Let (Ω,F,(Ft)t∈N0,P) be a discrete filtered probability space, let a≤b be real numbers, and put c=b−a. Let (Xt)t≥1 be real with Xt measurable with respect to Ft and P(a≤Xt≤b)=1 for every t. Let (X^t)t≥1 be real with X^t measurable with respect to Ft−1 and P(a≤X^t≤b)=1 for every t. Fix δ∈(0,1) and write α=δ/2. For c>0, let uα,c be any Borel one-sided sub-exponential uniform boundary with crossing probability α at scale c. Choose any versions mt=E[Xt∣Ft−1] and define Xˉt=1t∑i=1tXi,μt=1t∑i=1tmi,Vt=∑i=1t(Xi−X^i)2. Let Ct be the interval returned at time t by the empirical-Bernstein interval-update algorithm, using uα,c when c>0. Then P ⁣(μt∈Ct for every t≥1)≥1−δ. The probability statement is independent of the chosen conditional-expectation versions. No common conditional mean is assumed. If there is a fixed real μ such that E[Xi∣Fi−1]=μ almost surely for every i, then μt=μ simultaneously almost surely and the same intervals cover this fixed mean.

For c>0, the finite-mixture formula also supplies a valid boundary: choose an integer J≥1, numbers 0<λj<1/c, and weights wj>0 with ∑j=1Jwj=1. For every v≥0, the unique nonnegative solution s=uα,c(v) of ∑j=1Jwjexp⁡ ⁣(λjs−ψE,c(λj)v)=1α defines a Borel one-sided sub-exponential uniform boundary with crossing probability α at scale c.

Facts & Assumptions

Given: Assume AC. The objects, hypotheses, conventions, error levels, versions, boundary, and interval process in the Statement.

[F1]

Filtration and filtered probability space: (Ft) is an increasing filtration on one probability space, indexed from time zero.

[F2]

Adapted and integrable stochastic process: each Xt is an adapted real random variable; the almost-sure boundedness makes it integrable at each time.

[F3]

Predictable discrete time process: each forecast X^t is Ft−1-measurable.

[F4]

Conditional expectation given a sigma algebra: a conditional-expectation version is real, integrable, measurable with respect to the conditioning sigma-algebra, and has the defining event integrals.

[F5]

Conditional expectation as an ae class: conditional expectations are unique almost-sure classes of versions; the notation is independent of the chosen representative up to almost-sure equality.

[F6]

Basic algebra and order properties of conditional expectation: conditional expectation is linear, positive, order-preserving, and preserves constants.

[F7]

Taking out what is known: for a bounded measurable factor Z, E[ZX∣G]=ZE[X∣G] almost surely.

[F8]

Tower property of conditional expectation: if H⊆G, then E[E[X∣G]∣H]=E[X∣H] almost surely.

[F9]

Martingale submartingale and supermartingale: an integrable adapted process is a supermartingale when its one-step conditional expectations are at most its current values almost surely.

[F10]

Nonnegative test supermartingales: under a null law, a test supermartingale is adapted, integrable, nonnegative, supermartingale, and has initial expectation at most one.

[F11]

Mixtures of null test supermartingales: a product-measurable mixture of null test supermartingales is again a null test supermartingale.

[F12]

Ville's inequality for nonnegative test supermartingales: if M is a nonnegative test supermartingale, then P(sup⁡t≥0Mt≥1/α)≤α.

[F13]

One-sided sub-exponential uniform boundary: a scale-c one-sided sub-exponential boundary bounds the crossing probability of every pair in its stated process class.

[F14]

The exponential is positive, continuous and strictly increasing, has exp⁡(0)=1, and tends to 0 at −∞ and to +∞ at +∞. The exponential function is strictly increasing The exponential tends to +∞ at +∞ and to 0 at −∞ The exponential is positive and satisfies exp⁡(−x)=1/exp⁡(x)

[F15]
[F16]

Strictly between any two real numbers lies a rational. The rationals embed densely in the reals

[F17]

On (0,∞), log⁡′(x)=1/x and log⁡x=∫1xdt/t, so log⁡1=0. Derivatives obey the sum, product and chain rules, differentiability implies continuity, and the mean value theorem compares endpoint differences with interior derivatives. The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t Sum, product, quotient, and chain rules from difference quotients The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a)

[F19]

The open right rays (r,∞), r∈R, generate the real Borel sigma-algebra. Seven generating families for the Borel sigma-algebra on the real line

[L1]

Confidence sequence for a time-varying target: an adapted target process has a confidence sequence when its random intervals are measurable and cover the target at all integer times with the stated probability.

[L2]

Empirical-Bernstein confidence-sequence interval update: when c>0, the algorithm updates Xˉt and Vt from the observed data and returns the closed interval centered at Xˉt with radius uα,c(Vt)/t; when c=0, it returns [a,a].

[A1]

The Axiom of Choice: AC is assumed for conditional-expectation existence and for the cited supermartingale and Ville interfaces.

Proof

technique · direct
1.1givenF4F5F6A1L2choosealgebra

If c=0, then Xt=X^t=a almost surely for every t. By [F6], each mt=a almost surely, so μt=a simultaneously almost surely and the algorithm's singleton Ct=[a,a] covers it. If c>0, boundedness gives Xt∈L1(P); choose the versions in the Statement using [A1]. Any two versions agree almost surely by [F5], and the countable union of their exceptional null sets is null, so the all-times coverage probability does not depend on those choices.

1.2givenF13algebra

For x>−1 define r(x)=(x−log⁡(1+x))/x2 when x≠0 and r(0)=1/2. Direct integration gives r(x)=∫01t/(1+tx) dt. The integrand decreases in x for every t>0, so r is decreasing on (−1,∞). If c>0, 0<λ<1/c, and ∣ξ∣≤c, then x=λξ≥−λc>−1, whence λξ−log⁡(1+λξ)=(λξ)2r(λξ)≤(λξ)2r(−λc)=ψE,c(λ)ξ2. Exponentiating yields exp⁡(λξ−ψE,c(λ)ξ2)≤1+λξ; the same holds at λ=0 by equality.

1.3givenF10F11F12F13F14F15F16F17F18F19A1algebra

Fix any one-sided sub-exponential pair at scale c>0 and any finite mixture parameters from the Statement. For each j, its defining condition [F13] supplies a dominating nonnegative test supermartingale Lλj. For x=cλj∈(0,1), define h(t)=−log⁡(1−t)−t on t<1. By [F17], h(0)=0 and the chain and sum rules give h′(t)=1/(1−t)−1=t/(1−t). The function is continuous on [0,x] and differentiable on (0,x) by [F17]. The mean value theorem [F17] gives h(x)−h(0)=xh′(θ)≥0 for some 0<θ<x<1. Since c2>0, ψE,c(λj)=h(x)/c2≥0. For each fixed v≥0, gv(s)=∑jwjeλjs−ψE,c(λj)v is continuous by [F14] and [F18]. Every term is strictly increasing in s, since wj>0 and λj>0, so [F14] makes the sum strictly increasing. As s→−∞, each affine exponent tends to −∞, so [F14] makes every term tend to zero; the finite sum tends to zero. As s→∞, its first term tends to infinity by [F14] and every other term is positive, so the sum tends to infinity. Also gv(0)=∑jwje−ψE,c(λj)v≤∑jwj=1<1/α. The two limits give finite s−<0<s+ with gv(s−)<1/α<gv(s+); the intermediate value theorem [F15] on [s−,s+] gives a root between them, and strict increase makes it unique and positive. Write this root as uα,c(v). For each real r≤0, {v≥0:uα,c(v)<r} is empty. For r>0, strict increase and the root equation give {v≥0:uα,c(v)<r}=⋃q∈Q0<q<r{v≥0:gv(q)>1/α}. Indeed, if uα,c(v)<r, [F16] supplies a rational q strictly between the positive root and r; conversely, gv(q)>1/α implies q>uα,c(v). For fixed q, gv(q)=∑jwjeλjq−ψE,c(λj)v is continuous in v by [F14] and [F18], so each set in the union is open relative to [0,∞) and the union is open. To apply [F19] directly, if r≥0, strict increase gives {v≥0:uα,c(v)>r}={v≥0:gv(r)<1/α}, which is also relatively open by [F14] and [F18]; if r<0, this inverse image is all of [0,∞). Thus the inverse images of every open right ray are Borel. The real sets whose inverse images are Borel form a sigma-algebra, so [F19] implies that uα,c is Borel. There are finitely many indices j and countably many integer times, so the almost-sure domination inequalities for all Lλj hold simultaneously outside one null set. The finite mixture Lt=∑jwjLtλj is a test supermartingale by [F11]; finite support makes its product measurability immediate. If St≥uα,c(Vt), then Lt≥gVt(St)≥1/α. Ville's inequality [F12] bounds this crossing event by α, so the root is a boundary as in [F13].

2.1F1F2F3F4F6F7F8A1step 1.2

On the increasing filtration [F1], for t≥1 put Yt=Xt−mt, ηt=X^t−mt, and ξt=Yt−ηt=Xt−X^t. By [F6], a≤mt≤b almost surely, so ∣ηt∣≤c; by [F8], E[Yt∣Ft−1]=0. Also [F3] and [F4] make ηt bounded and Ft−1-measurable, and ∣ξt∣≤c. Apply step 1.2 to ξt and multiply by eληt. Taking conditional expectations, using [F6] and the bounded-factor identity [F7], gives E[eλYt−ψE,c(λ)ξt2∣Ft−1]≤eληt(1−ληt)≤1, since 1−z≤e−z for z=ληt<1.

3.1F2F3F9F10A1F13step 2.1

For each 0≤λ<1/c, define M0λ=1 and Mtλ=exp⁡ ⁣(λ∑i=1tYi−ψE,c(λ)Vt). This process is nonnegative and adapted. At each fixed t, its exponent is bounded because ∣Yi∣≤c and 0≤Vt≤c2t, so it is integrable. The one-step inequality in step 2.1, multiplied by the bounded Ft−1-measurable Mt−1λ, proves the supermartingale condition. Thus [F9], [F10], and [A1] make Mλ a nonnegative test supermartingale with initial expectation one, so Ltλ=Mtλ verifies the domination condition in [F13]. Replacing every Yi,ηi by −Yi,−ηi gives the same conclusion for the pair (−St,Vt), where St=∑i=1tYi.

4.1givenF1F2F3F4F13L1L2step 1.1step 3.1algebra∎

For the supplied boundary, [F13] and step 3.1 show that the crossing probability is at most α for both (St,Vt) and (−St,Vt). Outside their union, ∣St∣<uα,c(Vt) for every t. Since St=t(Xˉt−μt), this is exactly μt∈Ct for every interval returned by [L2], with probability at least 1−2α=1−δ. By [F1] and [F4], each mi is Fi−1-measurable, so μt is Ft-measurable; Xˉt,Vt are also Ft-measurable by [F2] and [F3], and composition with the Borel boundary makes the interval endpoints measurable. Thus [L1] applies. If all mi=μ almost surely for one fixed μ, their countable intersection has probability one and then μt=μ for all t, proving the fixed-mean clause.

Depends on

Used by

Dependency tree · two levels

102 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