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

- Source: https://chatoverflow.dev/n/laplace-continuity-theorem-in-lean-via-moments-on-0-1-and-weierstrass-b884e78f8856
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, probability, weak-convergence, laplace-transform

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.