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
Choquet’s capacitability theorem
8.2
Monotone class theorem
8.3
Debut Theorem
8.4
Hitting times
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
▶
10.1
Rings and semi-rings of sets
10.2
Simple processes and elementary predictable sets
10.3
Elementary stochastic integral
11
Modifications with cadlag paths
▶
11.1
Cadlag modifications of martingales
11.2
Cadlag modifications of (local) martingales
12
Doob-Meyer Theorem
▶
12.1
Komlòs Lemma
12.2
Doob decomposition in discrete time
12.3
Doob-Meyer decomposition
12.4
Local version of the Doob-Meyer decomposition
13
Stochastic integral
▶
13.1
Measure associated with a process
13.2
Quasi-martingales
13.3
Square integrable martingales
13.4
Local martingales
13.5
Stochastic integral
13.6
Itô formula
Bibliography
▶
Part 1 Bibliography
Part 2 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
Choquet’s capacitability theorem
8.2
Monotone class theorem
8.3
Debut Theorem
8.4
Hitting times
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
10.1
Rings and semi-rings of sets
10.2
Simple processes and elementary predictable sets
10.3
Elementary stochastic integral
11
Modifications with cadlag paths
11.1
Cadlag modifications of martingales
11.2
Cadlag modifications of (local) martingales
12
Doob-Meyer Theorem
12.1
Komlòs Lemma
12.2
Doob decomposition in discrete time
12.3
Doob-Meyer decomposition
12.4
Local version of the Doob-Meyer decomposition
13
Stochastic integral
13.1
Measure associated with a process
13.2
Quasi-martingales
13.3
Square integrable martingales
13.4
Local martingales
13.5
Stochastic integral
13.6
Itô formula
Bibliography
Part 1 Bibliography
Part 2 Bibliography