Exponential Convergence of the Lifted Gradient Flow of the Bass Functional
Danila Litvinov
math.PR
Oct 29, 2026 · v1
q-fin.MF
TL;DR
The main multidimensional exponential convergence theorem is formalized in Lean 4 using Mathlib, with axiom reports limited to standard axioms.
Abstract
We establish multidimensional exponential convergence of the lifted Bass gradient flow in martingale optimal transport. Let $μ\le_{cx}ν$ be an irreducible pair, with compact convex target support, source support strictly inside the target support, and target density bounded above and bounded away from zero almost everywhere on its interior. For every bounded $σ(X)$-measurable initial state, the flow converges exponentially in $L^2$ to the global minimizer with the prescribed mean, and the functional value gap decays exponentially. Both bounds hold at every nonnegative time with the exact initial errors as prefactors. The quantitative step is strong convexity on sets with a common $L^\infty$ bound and a fixed mean. We prove it by interpolating entropic endpoint potentials, using two conditional copies to cancel the unknown potential increment, and obtaining a Hessian lower bound uniform in the regularization parameter. Removing the regularization yields curvature for the original functional; the known qualitative theory supplies a common bound for the orbit. This extends the one-dimensional exponential-convergence result of Backhoff-Veraguas, Pammer, and Schachermayer. The main result is formalized in Lean 4. AI was used in preparing the paper (see Section 8).
Problem
The lifted gradient flow of the Bass functional in martingale optimal transport was known to converge exponentially only in one dimension. Multidimensional exponential convergence to the global minimizer was open.
Approach
The authors prove strong convexity of the functional on sets with a common L-infinity bound and fixed mean. They interpolate entropic endpoint potentials and use two conditional copies to cancel the unknown potential increment, which gives a Hessian lower bound uniform in the regularization parameter. Removing the regularization gives curvature for the original functional, and the known qualitative theory supplies a uniform bound along the orbit. The final statement is formalized in Lean 4 with Mathlib.
Results
For irreducible convex-ordered pairs with compact convex target support and a suitably bounded target density, the flow converges exponentially in L^2. The functional value gap also decays exponentially, at every time, with the exact initial errors as prefactors. The Lean declarations depend only on the standard axioms propext, Classical.choice and Quot.sound.
