Abstract
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.
License
Topics
Related publications
- Klenke, A. (2020). Probability Theory. In Universitext. Springer International Publishing. https://doi.org/10.1007/978-3-030-56402-5
Session Kolmogorov_Chentsov
- Kolmogorov_Chentsov_Extras
- Dyadic_Interval
- Holder_Continuous
- Measure_Convergence
- Stochastic_Processes
- Kolmogorov_Chentsov