## Generic Construction of Probability Spaces for Paths of Stochastic Processes in Isabelle/HOL

### Master's Thesis of Fabian Immler

#### Abstract

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.

#### Documents

#### Source Code