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
Basic definitions
7.2
Right-continuous filtrations
7.3
Predictable processes
7.4
Uniformly integrable
7.5
Optional sampling
7.6
Martingale convergence
7.7
Doob’s Lp inequality
8
Debut Theorem
▶
8.1
Corollaries
9
Local martingales
▶
9.1
Local properties
9.2
Locally Cadlag
9.3
Local martingales
9.4
Doob-Meyer class
10
Simple processes and elementary integrals
11
Modifications with cadlag paths
▶
11.1
Preliminaries
11.2
Cadlag modifications of martingales
11.3
Cadlag modifications of (local) martingales
12
Doob-Meyer Theorem
▶
12.1
Doob decomposition in discrete time
12.2
Komlòs Lemma
12.3
Doob-Meyer decomposition
12.4
Local version of the Doob-Meyer decomposition
13
Stochastic integral
▶
13.1
Total variation and Lebesgue-Stieltjes integral
13.2
Square integrable martingales
13.3
Local martingales
13.4
Stochastic integral
13.5
Itô formula
14
Bibliography
Dependency graph
Formalization of a Brownian motion and of stochastic integrals in Lean
Rémy Degenne Peter Pfaffelhuber
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
Basic definitions
7.2
Right-continuous filtrations
7.3
Predictable processes
7.4
Uniformly integrable
7.5
Optional sampling
7.6
Martingale convergence
7.7
Doob’s Lp inequality
8
Debut Theorem
8.1
Corollaries
9
Local martingales
9.1
Local properties
9.2
Locally Cadlag
9.3
Local martingales
9.4
Doob-Meyer class
10
Simple processes and elementary integrals
11
Modifications with cadlag paths
11.1
Preliminaries
11.2
Cadlag modifications of martingales
11.3
Cadlag modifications of (local) martingales
12
Doob-Meyer Theorem
12.1
Doob decomposition in discrete time
12.2
Komlòs Lemma
12.3
Doob-Meyer decomposition
12.4
Local version of the Doob-Meyer decomposition
13
Stochastic integral
13.1
Total variation and Lebesgue-Stieltjes integral
13.2
Square integrable martingales
13.3
Local martingales
13.4
Stochastic integral
13.5
Itô formula
14
Bibliography