CorollaryStatement: 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 zero

Statement

Let $B$ be a standard Brownian motion Brownian motion. Then almost surely ${lim sup}_{t ↓ 0} \frac{B_{t}}{\sqrt{2 t \log \log (1 / t)}} = 1, {lim inf}_{t ↓ 0} \frac{B_{t}}{\sqrt{2 t \log \log (1 / t)}} = - 1,$ the normalizer being taken for $0 < t < e^{- 1}$ so that $\log \log (1 / t) > 0$ .

Facts & Assumptions

Given: AC and a standard Brownian motion $B$ .

[F1]

Almost surely ${lim sup}_{s \to \infty} Y_{s} / \sqrt{2 s \log \log s} = 1$ and the corresponding limit inferior is $- 1$ for every standard Brownian motion $Y$ . Brownian law of the iterated logarithm at infinity

[F2]

Time inversion: the process $Y_{0} = 0$ , $Y_{s} : = s B_{1 / s}$ for $s > 0$ , is again a standard Brownian motion, with continuity at $s = 0$ part of the conclusion. Brownian time inversion

[F3]

AC is the ambient assumption of the Brownian interfaces. The Axiom of Choice

Proof

technique · direct

1.1

Let $Y$ be the time-inverted process of [F2]; by [F1] applied to $Y$ there is a probability-one event on which ${lim sup}_{s \to \infty} Y_{s} / \sqrt{2 s \log \log s} = 1$ and ${lim inf}_{s \to \infty} Y_{s} / \sqrt{2 s \log \log s} = - 1$ .

givenF1F2

2.1

On that event, substituting $s = 1 / t$ with $t ↓ 0$ and using $Y_{1 / t} = B_{t} / t$ gives $\frac{Y_{1 / t}}{\sqrt{2 t^{- 1} \log \log (1 / t)}} = \frac{B_{t} / t}{\sqrt{2 t^{- 1} \log \log (1 / t)}} = \frac{B_{t}}{\sqrt{2 t \log \log (1 / t)}}$ , so ${lim sup}_{t ↓ 0} \frac{B_{t}}{\sqrt{2 t \log \log (1 / t)}} = 1$ and ${lim inf}_{t ↓ 0} \frac{B_{t}}{\sqrt{2 t \log \log (1 / t)}} = - 1$ almost surely.

step 1.1F2

3.1

The cases are covered: the substitution $t \mapsto 1 / t$ is a bijection of $(0, \infty)$ onto itself, so $t ↓ 0$ corresponds to $s ↑ \infty$ ; the normalizer is positive exactly for $0 < t < e^{- 1}$ ; the endpoint $t = 0$ is not evaluated, continuity at zero being part of [F2]; and AC enters only through [F3].

step 2.1F2F3given∎

Source notes

Time inversion converts the law of the iterated logarithm at infinity, Theorem 8.5.1 of Durrett, into the corresponding statement at zero, with the normalizing factor transforming exactly as displayed.

Depends on

Used by

The critical Hölder boundary at zero Corollary
LIL rules out a square-root-time bound Example
The Brownian p-variation threshold Example

Dependency tree · two levels

26 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

Rick Durrett, Probability: Theory and Examples, fifth edition, Theorem 8.5.1 with Brownian time inversion (standard reference, not scraped)