This file proves the law of the iterated logarithm for Brownian motion, which provides sharp asymptotics for the limsup of B_t as t tends to infinity.

The main theorem is IsBrownianReal.ae_limsup_div_sqrt_log_log_eq_one, which proves that if $B_t$ is a Brownian motion, it holds almost surely that $\limsup_{t → ∞} \frac{B_t}{\sqrt{2 \log \log t}} = 1$.

theorem ProbabilityTheory.IsBrownianReal.reflection {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (hX : IsBrownianReal X P) {t : NNReal} {c : ℝ} (ht : 0 < t) (hc : 0 ≤ c) : P.real {ω : Ω | ↑c ≤ ⨆ (s : NNReal), ⨆ (_ : s ≤ t), ↑(X s ω)} = 2 * P.real {ω : Ω | c ≤ X t ω}

theorem ProbabilityTheory.IsStandardGaussian.tail {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : HasLaw X (gaussianReal 0 1) P) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => P.real {ω : Ω | x ≤ X ω}) fun (x : ℝ) => 1 / x * Real.exp (-1 / 2 * x ^ 2)

theorem ProbabilityTheory.IsBrownianReal.ae_limsup_div_sqrt_log_log_eq_one {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (hX : IsBrownianReal X P) : ∀ᵐ (ω : Ω) ∂P, Filter.limsup (fun (t : NNReal) => ↑(X t ω) / ↑√(2 * ↑t * Real.log (Real.log ↑t))) Filter.atTop = 1

Law of the iterated logarithm for Brownian motion.