Stochastic processes are used in probability theory to describe the evolution of random systems over time. The principal mathematical problem is the construction of a probability space for the paths of stochastic processes. The Daniell-Kolmogorov theorem solves this problem: it shows how a family of finite-dimensional distributions defines the distribution of the stochastic process. The construction is generic, i.e., it works for discrete time as well as for continuous time.
Starting from the existing formalizations of measure theory and product probability spaces in Isabelle/HOL, we provide a formal proof of the Daniell-Kolmogorov theorem in Isabelle/HOL. This requires us to formalize concepts from topology, namely polish spaces and regularity of measures on polish spaces.
These results can serve as a foundation to formalize for example discrete-time or continuous-time Markov chains, Markov decision processes, or physical phenomena like Brownian motion.