Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Brownian law of the iterated logarithm at infinity

Statement

Let B be a standard Brownian motion Brownian motion. Then on one measurable event of probability one lim suptBt2tloglogt=1,lim inftBt2tloglogt=1 the normalizing function being taken for t>e so that loglogt>0.

Facts & Assumptions

Given: AC, a standard Brownian motion B, rationals α>1, β>1 and the geometric sequence tn=αn.

[F1]

The increments of B over disjoint intervals are independent with laws N(0,h) for interval length h; the path is continuous on a probability-one event. Brownian motion

[F2]

Use the everywhere-continuous zero-start representative fixed in the maximum-law theorem (zero the path outside a measurable full event of continuity and zero start). It equals the original Brownian motion at all times on that event, so the final path conclusion transfers back. Law of the maximum: with MT=sup0sTBs one has P(MT>x)=2Φ(x/T) for x>0, where Φ(z)=zφ(y)dy. Law of the Brownian maximum

[F3]

Mills bounds: for z>0, Φ(z)φ(z)/z; for z>1, (z1z3)φ(z)Φ(z); and φ(z)=(2π)1/2ez2/2 is decreasing in z. Two-sided Mills bounds for the standard normal tail Standard normal and normal laws The standard normal density has total mass one

[F4]

First Borel-Cantelli: summable probabilities give almost surely finitely many occurrences; second Borel-Cantelli: independent events with divergent probability sum occur infinitely often almost surely. First Borel-Cantelli lemma for events Second Borel-Cantelli lemma under pairwise independence

[F5]

If X is a standard Brownian motion then so is X: the covariance characterisation exhibits the increments of X as independent stationary Gaussian increments, and continuity is preserved. Brownian covariance is equivalent to independent stationary normal increments

[F6]

The rationals are dense in R. The rationals embed densely in the reals

[F7]

AC is inherited from the Brownian, normal-law and maximum-law interfaces. Both cited Borel–Cantelli statements are choice-free; no choice assumption is added to them. The Axiom of Choice

Proof

technique · direct
1.1

For n with tn>e put Un:={Mtn>2βtnloglogtn} and zn:=2βloglogtn; by [F2] and [F3], P(Un)=2Φ(zn)2φ(zn)/znCα,βnβ(logn)1/2 for a constant Cα,β, because φ(zn)=(2π)1/2(logtn)β=(2π)1/2(nlogα)β; since β>1 the probabilities are summable. For example, grouping n in [2j,2j+1) bounds the upper series by a constant times j2j(1β), which is geometric. Set the finitely many early events with tne to the empty event.

givenF1F2F3
1.2

For the lower bound fix α>1, put β:=α/(α1)>1 and Dn:=Btn+1Btn, so that by [F1] the Dn are independent with law N(0,tn+1tn)=N(0,tn+1/β); let En:={Dn>γ2tn+1loglogtn+1} with γ:=1/β, and note γ2β=1.

givenF1
2.1

By [F4] and [step 1.1] there is a probability-one event on which Un fails for all sufficiently large n; on that event, for every ttN with N large, choosing n with tnt<tn+1 gives MtMtn+12βtn+1loglogtn+1 and hence Mt2tloglogtβαloglog(αt)loglogtαβ; therefore lim suptBt2tloglogtαβ almost surely.

step 1.1F1F4
2.2

For large n the probability of En satisfies P(En)=Φ(γ2βloglogtn+1)12zn1φ(zn)=122π12loglogtn+1logtn+1, with zn=2loglogtn+1, by the lower Mills bound of [F3]; since logtn+1=(n+1)logα, for sufficiently large n this is at least cα/((n+1)log(n+1)) with cα>0. In each block 2jn+1<2j+1, the sum of these lower bounds is at least a positive constant times 1/j+1; hence the series diverges (grouping that latter series into square blocks already gives a fixed positive contribution per block). Define the finitely many early events with tn+1e to be empty.

step 1.2F3
3.1

Intersecting the events of [step 2.1] over the countably many pairs of rationals α,β(1,2) and using [F6] to choose, for every ε>0, rationals with αβ1+ε, we obtain lim suptBt2tloglogt1 almost surely.

step 2.1F6
4.1

By [F5] the process B is again a standard Brownian motion, so [step 3.1] applies to it and gives lim inftBt2tloglogt1 almost surely.

step 3.1F5
5.1

By [F4] and [step 2.2] the events En occur infinitely often almost surely; on the event of [step 4.1] intersected with this one, for infinitely many n one has Btn+1=Btn+Dn(1+ε)2tnloglogtn+γ2tn+1loglogtn+1=2tn+1loglogtn+1(γ(1+ε)α1/2(1+o(1))).

step 4.1step 1.2step 2.2F1F4
6.1

Since γ=11/α1 and α1/20 as α, for every δ>0 there are rational α>1 and ε>0 with γ(1+ε)α1/21δ; hence [step 5.1] gives lim suptBt2tloglogt1δ almost surely for every rational δ>0, and intersecting over the countably many δ yields lim sup1 almost surely.

step 5.1F7
7.1

Combining [step 3.1] and [step 6.1] gives lim suptBt2tloglogt=1 almost surely; applying this conclusion to the standard Brownian motion B of [F5], whose limit superior is the negative of the limit inferior of B, gives lim inftBt2tloglogt=1 almost surely.

step 3.1step 6.1F5
8.1

The boundary and degeneracy cases are covered: the normalizer is positive precisely for t>e, and the statement is asymptotic as t; the geometric sequences are indexed from n=0, with only finitely many terms below e; the parameters over which probability-one events are intersected may be restricted to rational α,β>1 and rational δ>0, a countable family. The auxiliary value γ=11/α need not be rational and creates no additional event: once α is fixed it is a deterministic threshold in the same block events En. The upper and lower bounds are established using the first Borel-Cantelli lemma for the upper bound and the second for the lower bound; AC enters only through [F7].

step 3.1step 6.1step 7.1F7given

Source notes

This follows the geometric-block architecture of Durrett, Theorem 8.5.1 (printed pp.416–418), with an explicit critical-threshold variant. Durrett's lower bound uses threshold coefficient 1/β and a subcritical exponent 1/β; here γ=1/β gives exponent one, whose remaining 1/logn factor still makes the probability series divergent, as proved in step 2.2. The upper bound, interpolation, independent-block lower bound and sign symmetry follow the same route. The threshold γ need not be rational: it is determined by the rational parameter α.

Depends on

Used by

Dependency tree · two levels

53 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