We implement some probability theory in Lean4. We start with results on separating classes of functions on the set of probability measures. Further topics
- Characteristic functions -> Definitions of well-known distributions -> CLT
- Kolmogorov-Chentsov -> Brownian motion