feat: law of the iterated logarithm

[jvanwinden]

This PR adds a proof of the law of the iterated logarithm for Brownian motion, stating that

$\limsup_{t \to \infty} \frac{B_t}{\sqrt{2 \log \log t}} = 1$ almost surely.

The statement is given by IsBrownian.ae_limsup_div_sqrt_log_log_eq_one, and only uses the assumption IsBrownian X P. The proof is the one from Kallenberg.

There are however two sorry-ful lemmas, namely IsBrownian.reflection and IsStandardGaussian.tail.
The latter can be formalized right now, but the former relies on the strong Markov property for Brownian motion, which might benefit from being proved in higher generality (for example, for Feller processes).

[RemyDegenne]

Could you merge the master branch into yours and then run lake exe mk_all --module to add your new file to the imports of the BrownianMotion.lean file?

[jvanwinden]

Thanks for the review @RemyDegenne! It's my first time proving a 'nontrivial' (for some definition of nontrivial) theorem in lean, so any feedback is much appreciated.