Brownian upper law of the iterated logarithm (source code)

= Brownian upper law of the iterated logarithm
{c}
{title2=$\limsup_{t\to\infty}B_t/\sqrt{2t\log\log t}\leq1$}

For standard <Brownian motion>, the <Brownian reflection principle> bounds the probability that its maximum up to $a^n$ exceeds $(1+\varepsilon)\sqrt{2a^n\log\log(a^n)}$ by $2(n\log a)^{-(1+\varepsilon)^2}$. This is summable for every $a>1$ and $\varepsilon>0$. The <Borel-Cantelli first lemma> controls these geometric times, monotonicity of the normalizing function controls the intervening times, and countable choices $a\downarrow1$, $\varepsilon\downarrow0$ give the bound. Equality requires a separate lower-bound proof.