Local CLT on ℤ in Lean/Mathlib: one DCT with a single e^{-ct²} bound

Gnedenko's local limit theorem (√n P(S_n=k) − gaussian((k−nμ)/√n) → 0 uniformly in k) formalizes in ~550 lines. (1) Fourier inversion on ℤ: P(Y=k) = (2π)⁻¹∫_{-π}^{π} e^{-ikt} charFun t dt, via integral_integral_swap (bounded integrand, Integrable.of_bound) and integral_exp_mul_complex + Complex.exp_eq_exp_iff_exists_int for ∫ e^{imt}=0. (2) Substitute t=x/√n with intervalIntegral.integral_comp_div; the Gaussian side is integral_cexp_quadratic. The error is ≤ (2π)⁻¹∫‖1_{Ioc(-π√n,π√n)} ψ(x/√n)^n − e^{-ax²}‖, independent of k. (3) Skip the textbook three-region estimate: from Taylor (taylorWithinEval_charFun_two_zero + taylor_isLittleO_univ) near 0 and IsCompact.exists_isMaxOn on {δ≤|t|≤π}, get one bound |ψ(t)| ≤ 1−ct² ≤ e^{-ct²} on all of [-π,π]; then |ψ(x/√n)^n| ≤ e^{-cx²} and a single tendsto_integral_filter_of_dominated_convergence finishes. Pointwise limit: tendsto_pow_exp_of_isLittleO_sub_add_div. Aperiodicity as 'law not on a coset of a proper AddSubgroup ℤ' makes |φ(t)|<1 easy: H = {m | e^{itm}=1} is a subgroup, 1∉H since t∉2πℤ.