Applications of Proof Theory to Limit Theorems and Stochastic Processes

Abstract

This thesis represents a stepping stone in advancing the applications of proof-theoretic tools in
probability theory and the theory of stochastic processes. Its contributions are both founda-
tional and applied.
The applied aspect of this thesis presents quantitative versions of important results in
probability theory. We give quantitative versions of various Strong Laws of Large Numbers,
including the improvement of known bounds from the literature. We provide a quantitative
version of Doob’s seminal martingale convergence theorem, and in doing so, we generalise
bounds on the stochastic fluctuations of martingales, found in the literature, to submartingales
and supermartingales. We present improved stochastic fluctuation bounds in the pointwise
ergodic theorem and bounds on local stability that generalise those found in the applied proof
theory literature. Lastly, we provide a quantitative version of the celebrated Robbins-Siegmund
theorem and various applications in stochastic approximation theory, including rates for a
procedure of Dvoretzky.
The primary foundational contribution of the thesis is the development of abstract frame-
works for studying the quantitative aspects of probability theory, with a particular focus on
stochastic convergence. This includes introducing a formal system for reasoning about prob-
ability theory and a corresponding metatheorem guaranteeing the extractability of uniform
quantitative data for a large class of results. Lastly, the thesis presents various proof-theoretic
transfer principles that allow for the transformation of quantitative data from deterministic
results to their probabilistic analogue.
We conclude this thesis with a discussion on the current work in progress, both foundational
and applied, in proof mining in probability theory. We also present some open problems and
conjectures, paving the way for future research and development in this exciting field.

Date of Award	7 May 2025
Original language	English
Awarding Institution	University of Bath
Supervisor	Thomas Powell (Supervisor) & Guy McCusker (Supervisor)