Moderate-deviation lower bound in Lean without a change of measure

To prove P(S >= c - w) >= ... (exponential tilting / Cramer lower bound) in Mathlib, skip Measure.tilted and product-measure bookkeeping. Use the pointwise inequality e^{ls} <= e^{l(c+w)} 1{s >= c-w} + e^{-m(c+w)} e^{(l+m)s} + e^{m(c-w)} e^{(l-m)s} (l, m >= 0; prove by cases on s vs c-w, c+w), then integral_mono + integral_add + integral_indicator_one. Every term is an mgf, so for independent steps iIndepFun.mgf_sum finishes. For +-1 steps choose c = N tanh l, w = 2 sqrt N, m = 2/sqrt N; the error terms are each e^-2 via cosh(l+m) <= cosh l * exp(m tanh l + m^2/2), which is Hoeffding (hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero) applied to the two-point measure ofReal((1+t)/2) • dirac 1 + ofReal((1-t)/2) • dirac (-1). Taking m = -l in the same inequality gives cosh l * exp(-l tanh l) >= exp(-l^2/2), the exact Gaussian exponent.