Formalization of a Brownian motion and of stochastic integrals in Lean
1
Brownian motion
▶
1
Characteristic function and covariance
▶
1.1
Characteristic functions
1.2
Covariance
2
Stochastic processes
3
Gaussian distributions
▶
3.1
Gaussian measures
3.2
Gaussian processes
4
Projective family of the Brownian motion
▶
4.1
Kolmogorov extension theorem
4.2
Projective family of Gaussian measures
5
Kolmogorov-Chentsov Theorem
▶
5.1
Covers and covering numbers
5.2
Chaining
5.3
Chaining for stochastic processes under Kolmogorov conditions
5.4
Kolmogorov-Chentsov Theorem
6
Brownian motion
▶
6.1
Stochastic process with continuous paths
6.2
Wiener measure on the continuous functions
2
Stochastic integral
▼
7
Filtrations, processes and martingales
▶
7.1
Local martingales
8
Doob-Meyer Theorem
▶
8.1
Doob decomposition in discrete time
8.2
Cadlag modifications of (local) martingales
8.3
Komlòs Lemma
8.4
Doob-Meyer decomposition
8.5
Local version of the Doob-Meyer decomposition
9
Stochastic integral
▶
9.1
Total variation and Lebesgue-Stieltjes integral
9.2
Doob’s Lp inequality
9.3
Square integrable martingales
9.4
Local martingales
9.5
Stochastic integral
9.6
Itô formula
10
Bibliography
Dependency graph
Bibliography