Constructive Probability, Foundations and Numerical Analysis for mathematical finance and machine learning
Claudio Albanese
math.PR
Nov 5, 2026 · v1
TL;DR
A Lean 4/Mathlib Lake project, sorry-free, formalizes the Farkas/orthant alternative behind the fundamental theorem and algebraic lemmas from later chapters.
Abstract
This monograph sets out a constructive theory of stochastic processes in the continuum, in the sense of constructive field theory: the continuum is not postulated but reached as the limit of a sequence of lattice approximations, with the renormalisation the limit requires exhibited rather than assumed, and the limit controlled by estimates that can be checked. The primitive object is not a sigma-algebra but de Finetti's prevision, the price of finitely many gambles at a fixed resolution, which coherence turns into a conditional expectation. The theorem at the centre of the book, called plainly the fundamental theorem, is at once de Finetti's fundamental theorem of probability, the fundamental theorem of Bayesian statistics, and the one-period fundamental theorem of asset pricing; the financial vocabulary is a convenience only. The applications are two, mathematical finance and machine learning, and they are one mathematics read in opposite directions: an assessment is a price in the one and a prediction in the other, and both are computed by one adjoint recursion, the adjoint of a propagation in the first case and backpropagation in the second. Carried through, the two directions give sharp rates of convergence rather than asymptotic orders: for the moments of Ito diffusions, for the value function of Feynman-Kac semigroups, and for the measure changes of the fundamental theorem, the last as a limit theorem for reweighted generators, under a condition keeping the reweighting well behaved. A measure change is thus calculated, not postulated: a lattice approximation with Farkas' lemma computes it, completeness makes it unique, and the passage to the continuum is earned by the regularity of what is computed. Sixty-seven Python scripts regenerate every numerical table, and much of the finite-dimensional core of the argument has been verified in Lean 4.
Problem
The monograph builds a constructive theory of stochastic processes and mathematical finance from de Finetti's prevision rather than sigma-algebras, reaching the continuum through lattice approximations with explicit convergence estimates. The aim is a formulation in which every statement concerns finite objects, so that it can be machine-checked.
Approach
The central fundamental theorem, covering coherence, Bayesian statistics and one-period asset pricing, is proved through a finite-dimensional orthant alternative (Farkas' lemma) and then applied site-by-site on lattices to construct pricing measures. Sixty-seven Python scripts regenerate the numerical tables. A small Lean 4 project built on Mathlib, with modules Cert.Farkas, Cert.Basic, Cert.Phi1, Cert.Antiderivative and Cert.Abelian, formalizes the finite-dimensional core. It obtains the certificate through Mathlib's geometric separation route.
Results
The monograph derives sharp convergence rates for moments of Ito diffusions, Feynman-Kac value functions and measure changes. The Lean development builds with lake build, contains no sorry, and uses only the standard axioms. The analytic estimates of Chapter 5 are not formalized.