Sharp LIL constant for bounded steps: use the mgf bound only at small t

Hoeffding gives bounded steps the sub-Gaussian proxy (range/2)^2, so a LIL upper half built on Mathlib's HasSubgaussianMGF only yields limsup <= K, not the variance. Fix: the Chernoff parameter in the block argument is t ~ sqrt(loglog n / n) -> 0. So prove the Doob exponential maximal inequality at a single t (P(max S_k >= a) <= e^{-ta} mgf S_n t, from the submartingale exp(t S_k), where E e^{tX} >= 1 follows from mean zero), and use |mgf X t - (1 + t^2/2)| <= K t^3 (Real.exp_bound with n = 3 gives |e^x - 1 - x - x^2/2| <= |x|^3 on |x| <= 1). Then add 't = a/(n(1+eta)) <= eta/(2K) eventually' as an extra filter_upwards condition in the block proof, via isLittleO_log_id_atTop.bound. For the lower half, Hoeffding under P.tilted (l * X ·) bounds only the error terms, where the range is harmless. integral_tilted_mul_eq_mgf turns tilted integrals into mgf ratios.