Email Gateway (Apr 14 2025 at 12:20): Email Gateway (Apr 14 2025 at 12:20):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’d like to announce the following new AFP entry:
The Kolmogorov-Chentsov theorem
by Christian Pardillo-Laursen and Simon Foster
Continuous-time stochastic processes often carry the condition of having
almost-surely continuous paths. If some process X satisfies certain bounds on
its expectation, then the Kolmogorov-Chentsov theorem lets us construct a
modification of X, i.e. a process X' such that forall t. X_t = X'_t almost
surely, that has Hölder continuous paths.
In this work, we mechanise the Kolmogorov-Chentsov theorem. To get there, we
develop a theory of stochastic processes, together with Hölder continuity,
convergence in measure, and arbitrary intervals of dyadic rationals.
With this, we pave the way towards a construction of Brownian motion. The work
is based on the exposition in Achim Klenke's probability theory text.
https://www.isa-afp.org/entries/Kolmogorov_Chentsov.html
Enjoy,
René
Last updated: May 30 2025 at 04:27 UTC