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 be a standard Brownian motion Brownian motion. Then on one measurable event of probability one the normalizing function being taken for so that .
Facts & Assumptions
Given: AC, a standard Brownian motion , rationals , and the geometric sequence .
The increments of over disjoint intervals are independent with laws for interval length ; the path is continuous on a probability-one event. Brownian motion
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 one has for , where . Law of the Brownian maximum
Mills bounds: for , ; for , ; and is decreasing in . Two-sided Mills bounds for the standard normal tail Standard normal and normal laws The standard normal density has total mass one
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
If is a standard Brownian motion then so is : the covariance characterisation exhibits the increments of as independent stationary Gaussian increments, and continuity is preserved. Brownian covariance is equivalent to independent stationary normal increments
The rationals are dense in . The rationals embed densely in the reals
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
For with put and ; by [F2] and [F3], for a constant , because ; since the probabilities are summable. For example, grouping in bounds the upper series by a constant times , which is geometric. Set the finitely many early events with to the empty event.
For the lower bound fix , put and , so that by [F1] the are independent with law ; let with , and note .
By [F4] and [step 1.1] there is a probability-one event on which fails for all sufficiently large ; on that event, for every with large, choosing with gives and hence ; therefore almost surely.
For large the probability of satisfies , with , by the lower Mills bound of [F3]; since , for sufficiently large this is at least with . In each block , the sum of these lower bounds is at least a positive constant times ; 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 to be empty.
Intersecting the events of [step 2.1] over the countably many pairs of rationals and using [F6] to choose, for every , rationals with , we obtain almost surely.
By [F5] the process is again a standard Brownian motion, so [step 3.1] applies to it and gives almost surely.
By [F4] and [step 2.2] the events occur infinitely often almost surely; on the event of [step 4.1] intersected with this one, for infinitely many one has .
Since and as , for every there are rational and with ; hence [step 5.1] gives almost surely for every rational , and intersecting over the countably many yields almost surely.
Combining [step 3.1] and [step 6.1] gives almost surely; applying this conclusion to the standard Brownian motion of [F5], whose limit superior is the negative of the limit inferior of , gives almost surely.
The boundary and degeneracy cases are covered: the normalizer is positive precisely for , and the statement is asymptotic as ; the geometric sequences are indexed from , with only finitely many terms below ; the parameters over which probability-one events are intersected may be restricted to rational and rational , a countable family. The auxiliary value need not be rational and creates no additional event: once is fixed it is a deterministic threshold in the same block events . 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].
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 and a subcritical exponent ; here gives exponent one, whose remaining 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
- Brownian motion
- Brownian covariance is equivalent to independent stationary normal increments
- Law of the Brownian maximum
- Two-sided Mills bounds for the standard normal tail
- Standard normal and normal laws
- The standard normal density has total mass one
- First Borel-Cantelli lemma for events
- Second Borel-Cantelli lemma under pairwise independence
- The rationals embed densely in the reals
- The Axiom of Choice
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
- Rick Durrett, Probability: Theory and Examples, fifth edition, Theorem 8.5.1 (standard reference, not scraped)