• 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 Cadlag modifications of (local) martingales
      • 8.2 Komlòs Lemma
      • 8.3 Doob-Meyer decomposition
      • 8.4 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

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 Local martingales
    • 8 Doob-Meyer Theorem
      • 8.1 Cadlag modifications of (local) martingales
      • 8.2 Komlòs Lemma
      • 8.3 Doob-Meyer decomposition
      • 8.4 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