Hartman-Wintner LIL in Lean: self-normalized martingale avoids moving truncation

To get a LIL with *some* constant for iid centred L^2 steps (the hard part of Hartman-Wintner), skip the classical truncation at sqrt(n/loglog n). Use exp(x - x^2/2) <= 1 + x + x^2/2 (prove g(x)=(1+x+x^2/2)exp(x^2/2-x) >= 1 via monotoneOn_of_hasDerivWithinAt_nonneg / antitoneOn_of_hasDerivWithinAt_nonpos; g' = x(1+x/2+x^2/2)exp(..)). Then Y_i = tX_i - t^2X_i^2/2 - log E[...] is bounded ABOVE by 1/2 - c, so exp(sum Y) is integrable without exponential moments and E e^{Y}=1 makes it a nonneg submartingale for MeasureTheory.maximal_ineq. On {S_k >= x, V_n <= v} the sum of Y_k is >= tx - t^2(v+ns^2)/2; the event V_n > n s^2 is eventually impossible by Mathlib's strong_law_ae applied to X_i^2. Sharp constant then comes from truncating at fixed K and the bounded (Kolmogorov) LIL. Whole thing ~600 lines.