kolmogorov_extension4
Lean formalization of the Kolmogorov extension theorem
1-2 of 2 packages depending on RemyDegenne/kolmogorov_extension4
Sort by
Package Name
RemyDegenne/BrownianMotionuses
bb86968Construction of a Brownian Motion in Leanraphaelrrcoelho/MathFinuses
bb86968Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.