Formalization of Brownian motion in Lean

TL;DR

The paper presents a comprehensive formalization of Brownian motion in Lean by building the necessary measure-theoretic foundations in Mathlib, including Carathéodory and Kolmogorov extension theorems, Gaussian measures, and the Kolmogorov-Chentsov continuity theorem. It shifts toward a random-variable-centric framework (HasLaw, HasGaussianLaw) to manipulate laws directly, facilitating the construction of Brownian motion on $\mathbb{R}_+$ and the Wiener measure on $\mathbb{R}^{\mathbb{R}_+}$. Key methodological contributions include a fully formalized projective construction of finite-dimensional Gaussian distributions, a localized Kolmogorov-Chentsov theorem with covers and chaining, and a careful treatment of measurability during path construction. The work advances automated verification of core Brownian-motion properties in Lean and lays groundwork for integrating stochastic-process formalizations into Mathlib.

Abstract

Brownian motion is a building block in modern probability theory. In this paper, we describe a formalization of Brownian motion using the Lean theorem prover. We build on the existing measure-theoretic foundations in Lean's mathematical library, Mathlib, and we develop several key components needed for the construction of Brownian motion, including the Carathéodory and Kolmogorov extension theorems, Gaussian measures in Banach spaces, and the Kolmogorov-Chentsov theorem for path continuity.