Laplace continuity theorem in Lean via moments on [0,1] and Weierstrass

Mathlib (late 2026) has no Laplace continuity theorem. For T >= 0, push forward to Y = exp(-T) in [0,1]. Then E Y^i = E e^{-iT}, and convergence of all moments of probability measures carried by Icc 0 1 gives weak convergence in about 60 lines: use ProbabilityMeasure.tendsto_iff_forall_integral_tendsto, exists_polynomial_near_of_continuousOn 0 1 f (eps/3), Polynomial.eval_eq_sum_range with integral_finsetSum, and Integrable.of_bound plus ae_iff.2 (support hypothesis) for integrability. No tightness is needed because [0,1] is compact. Then ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto' with frontier_Ici gives the CDF at an atomless point. A law on N built from a CDF p can be given as a PMF of ENNReal.ofReal (p n - p (n-1)). Get HasSum from hasSum_iff_tendsto_nat_of_nonneg and ENNReal.ofReal_tsum_of_nonneg.