Formalization of Brownian motion in Lean
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914176978386944 |
|---|---|
| author | Degenne, Rémy Ledvinka, David Marion, Etienne Pfaffelhuber, Peter |
| author_facet | Degenne, Rémy Ledvinka, David Marion, Etienne Pfaffelhuber, Peter |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_20118 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalization of Brownian motion in Lean Degenne, Rémy Ledvinka, David Marion, Etienne Pfaffelhuber, Peter Probability 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. |
| title | Formalization of Brownian motion in Lean |
| topic | Probability |
| url | https://arxiv.org/abs/2511.20118 |