Abstract
It is an elementary fact from real analysis that any monotone bounded sequence of real numbers converges. It turns out that the monotone convergence theorem can be given an equivalent finitary formulation: roughly that any sufficiently long monotone bounded sequence experiences long regions where the sequence is metastable. This so-called “finite convergence principle” is carefully motivated and discussed by Terence Tao in a 2007 blog post (‘Soft analysis, hard analysis, and the finite convergence principle’), but was already known to proof theorists, where the use of logical methods to both finitize infinitary statements and provide uniform quantitative information for the finitary versions plays a central role in the so-called proof mining program. The goal of my talk is to discuss how methods from proof mining can be applied to the theory of stochastic processes, an area of mathematics hitherto unexplored from this perspective. I will begin by discussing the simple monotone convergence principle, and will then focus on how everything I mentioned above can be generalised to the analogous result in the stochastic setting: Doob’s martingale convergence theorems. This then sets the groundwork for new applications of proof theory in stochastic optimization, and I will give a high level overview of some recent work in this direction, joint with Morenikeji Neri and Nicholas Pischke.
Talk Details
Speaker: Thomas Powell (University of Bath, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 15:15
Key Topics
- Proof mining program
- Monotone convergence theorem
- Finite convergence principle
- Metastability
- Stochastic processes
- Doob’s martingale convergence theorems
- Stochastic optimization
- Quantitative analysis
- Finitization of infinitary statements
Collaborators
- Morenikeji Neri
- Nicholas Pischke
Related Work
- Terence Tao’s ‘Soft analysis, hard analysis, and the finite convergence principle’ (2007)
- Proof mining methodology
- Martingale theory