All missions

Motivation

Mean field games (Lasry–Lions 2006–2007; Huang–Malhamé–Caines 2006) describe Nash equilibria of games with a very large number of symmetric players, each interacting with the others only through the empirical distribution of their states. When all players are also exposed to a common noise, the equilibrium is no longer described by a forward–backward pair of PDEs but by a single equation on the space of probability measures, the master equation. The master equation is the object that lets one prove convergence of $N$-player equilibria to the mean field limit (Cardaliaguet–Delarue–Lasry–Lions 2019), so a global classical solution is the starting point of that theory.

Global well-posedness requires a monotonicity condition; without one, uniqueness of equilibria fails. Before this paper, global results were known under the Lasry–Lions monotonicity condition and for separable Hamiltonians $H(x,\mu,p)=H_0(x,p)-F(x,\mu)$, and under displacement convexity in deterministic potential games (Gangbo–Mészáros 2022). Gangbo, Mészáros, Mou and Zhang (Ann. Probab. 50 (2022)) prove global well-posedness for nonseparable Hamiltonians under displacement monotonicity, a condition that is different from Lasry–Lions monotonicity and that has a natural extension to Hamiltonians depending jointly on $(x,\mu,p)$.

Setting

Let $\mathcal P_2=\mathcal P_2(\mathbb R^d)$ be the Borel probability measures on $\mathbb R^d$ with finite second moment, with the 2-Wasserstein distance $W_2$. For $U:\mathcal P_2\to\mathbb R$, the Lions derivative $\partial_\mu U(\mu,\tilde x)\in\mathbb R^d$ is characterized by

$$U(\mathcal L_{\xi+\eta})-U(\mu)=\mathbb E[\langle\partial_\mu U(\mu,\xi),\eta\rangle]+o(\|\eta\|_2),\qquad \mathcal L_\xi=\mu .$$

The class $\mathcal C^2(\mathbb R^d\times\mathcal P_2)$ consists of continuous $U(x,\mu)$ for which $\partial_xU$, $\partial_{xx}U$, $\partial_\mu U(x,\mu,\tilde x)$, $\partial_x\partial_\mu U$, $\partial_{\tilde x}\partial_\mu U$ and $\partial_{\mu\mu}U(x,\mu,\tilde x,\bar x)$ exist and extend to jointly continuous functions of all their arguments.

The data are a horizon $T>0$, a common-noise intensity $\beta\ge0$ with $\hat\beta^2=1+\beta^2$, a Hamiltonian $H(x,\mu,p)$ and a terminal cost $G(x,\mu)$. The master equation on $\Theta=[0,T]\times\mathbb R^d\times\mathcal P_2$ is

$$-\partial_tV-\tfrac{\hat\beta^2}{2}\operatorname{tr}(\partial_{xx}V)+H(x,\mu,\partial_xV)-\mathcal NV=0,\qquad V(T,x,\mu)=G(x,\mu),$$

with the nonlocal operator

$$\mathcal NV=\operatorname{tr}\,\bar{\tilde{\mathbb E}}\Big[\tfrac{\hat\beta^2}{2}\partial_{\tilde x}\partial_\mu V(t,x,\mu,\tilde\xi)+\tfrac{\beta^2}{2}\partial_{\mu\mu}V(t,x,\mu,\bar\xi,\tilde\xi)+\beta^2\partial_x\partial_\mu V(t,x,\mu,\tilde\xi)-\partial_\mu V(t,x,\mu,\tilde\xi)(\partial_pH)^\top(\tilde\xi,\mu,\partial_xV(t,\tilde\xi,\mu))\Big],$$

where $\tilde\xi,\bar\xi$ are independent with law $\mu$. A classical solution is a $V\in\mathcal C^{1,2,2}(\Theta)$ satisfying the equation on $(0,T)$ and the terminal condition.

$U(x,\mu)$ is displacement monotone (2.16) if for all square-integrable $\xi,\eta$ with $\mathcal L_\xi=\mu$ and an independent copy $(\tilde\xi,\tilde\eta)$,

$$\tilde{\mathbb E}\big[\langle\partial_{x\mu}U(\xi,\mu,\tilde\xi)\tilde\eta,\eta\rangle+\langle\partial_{xx}U(\xi,\mu)\eta,\eta\rangle\big]\ge0 .$$

The Hamiltonian is displacement monotone (Definition 3.4) if a bilinear form built from $\partial_{x\mu}H$, $\partial_{xx}H$ and a correction $\tfrac14\mathbb E\big|(\partial_{pp}H)^{-1/2}\tilde{\mathbb E}[\partial_{p\mu}H\,\tilde\eta]\big|^2$ is nonpositive, with $p=\varphi(\xi)$ for every bounded Lipschitz $C^1$ map $\varphi$. Assumptions 3.1 and 3.2 impose regularity and bounds on $G$ and $H$; Assumption 3.5 imposes the two monotonicity conditions.

Formalization targets

Goal: Theorem 6.3, first sentence

Under Assumptions 3.1, 3.2 and 3.5, the master equation on $[0,T]$ has a classical solution $V$ with bounded $\partial_xV$, $\partial_{xx}V$, $\partial_\mu V$, $\partial_{x\mu}V$, and it is the only classical solution in that class:

$$\exists!\,V\in\mathcal C^{1,2,2}(\Theta)\ \text{solving (1.1) with}\ \partial_xV,\partial_{xx}V,\partial_\mu V,\partial_{x\mu}V\ \text{bounded}.$$

Milestones

1. Lemma 2.1: $\partial_{\tilde x\mu}U(\mu,\tilde x)$ is symmetric for $U\in\mathcal C^2(\mathcal P_2)$.
2. Theorem 4.1: along a sufficiently regular classical solution, $V(t,\cdot,\cdot)$ is displacement monotone for every $t\in[0,T]$.
3. Theorem 5.1: if $V(t,\cdot,\cdot)$ is displacement semimonotone with constant $\lambda$, then $V$ and $\partial_xV$ are $W_2$-Lipschitz in $\mu$ with a constant depending only on $d$, $T$, $\|\partial_xV\|_\infty$, $\|\partial_{xx}V\|_\infty$, $L_2^G$, $L^H(\|\partial_xV\|_\infty)$ and $\lambda$.
4. Proposition 6.2(iii) with (6.7): on a short interval $[t_0,T]$, of length $\delta$ independent of $L_1^G$, the master equation has a unique classical solution with full $\mathcal C^2$ regularity and $|\partial_\mu V(t_0)|,|\partial_{x\mu}V(t_0)|\le C_1^\mu$.

Significance

The theorem gives global classical well-posedness of the master equation with common noise for a class of Hamiltonians that need not be separable and data that need not be Lasry–Lions monotone. A classical solution is what the convergence analysis of $N$-player games and the construction of approximate equilibria take as input. Theorem 4.1, displacement monotonicity propagating backward along the equation, is the central structural fact; Theorem 5.1 converts it into an a priori Lipschitz bound in $\mu$ that is uniform in time, which is what allows local solutions to be continued.

The result is proved in the paper; nothing in this mission is open mathematically. No part of it is formalized anywhere. The mission produces a formal statement of the master equation, its classical solutions and the displacement monotonicity conditions, plus targets for a machine-checked proof. Calculus on Wasserstein space with Lions derivatives is absent from Mathlib, so even Lemma 2.1 requires new infrastructure.

Difficulty

Local well-posedness holds for any regular data; the obstacle is continuing the solution to the whole interval. The length of the local interval depends on the Lipschitz constant of the terminal data in $\mu$, and without a uniform-in-time bound on that constant the local intervals can shrink to zero. Lasry–Lions monotonicity is not available here, and for nonseparable $H$ it has no obvious analogue. Any argument that controls this constant has to work with second-order Lions derivatives, which needs full $\mathcal C^2$ regularity in the measure variable. That regularity is itself only known on short intervals.

Formalization scope

• States are EuclideanSpace ℝ (Fin d). $\mathcal P_2$ is a subtype of measures, so functions of $\mu$ are defined only on $\mathcal P_2$. $W_2$ is the published WassersteinDRO.Duality.wassersteinDistance with $p=2$, converted to a real number.
• There is no probability space. Every expectation over $\xi,\eta$ and independent copies is an integral against an $\mathbb L^2$-coupling $\pi$ (the joint law of $(\xi,\eta)$), against $\pi\otimes\pi$, or against $\mu\otimes\mu$. Quantifying over all couplings is the reading of "for all $\xi,\eta\in\mathbb L^2$".
• The Lions derivative is stated in coupling form, uniformly over all $\xi$ of law $\mu$. Derivatives are explicit witnesses, i.e. global versions, and joint continuity is required as on the page.
• Derivatives are (bi)linear maps. $\langle\partial_{x\mu}U\,\tilde\eta,\eta\rangle$ takes the $x$-direction $\eta$ first. Matrix norms are operator norms; this choice changes no statement, since all constants are existential.
• $\mathcal C^2(\mathbb R^d\times\mathcal P_2\times\mathbb R^k)$, which the page uses without defining, lumps the Euclidean variables into one. "$H\in\mathcal C^3$" is read as existence and joint continuity of the $(x,p)$-derivatives up to order three. Vector-valued memberships are stated coordinatewise.
• $\partial_{pp}H$ is assumed positive definite, which the page's $(\partial_{pp}H)^{-1/2}$ presupposes. $|A^{-1/2}w|^2$ is written $\langle A^{-1}w,w\rangle$.
• The expectations in $\mathcal NV$ are required to exist, so a non-integrable integrand cannot make the equation hold through a Bochner integral defaulting to $0$. $L_2^G$ (Remark 3.3) is used in its Lipschitz form.
• "Depending only on" clauses are quantifier orders. In Proposition 6.2, $\delta$ depends on $d,T,C_0,L_0^G,L^H,L_2^G$; this expands $L^H(C_1^x)$, whose constant $C_1^x$ comes from a BSDE. Uniqueness is within the bounded-derivative class of Theorem 6.3.
• Out of scope: the second sentence of Theorem 6.3 (well-posedness of the McKean–Vlasov FBSDEs and the representation (6.6)), Proposition 6.1, and Proposition 6.2(i), (ii) and (2.27). They need Brownian motions with common noise and BSDEs.
• A statement in which the regularity hypotheses cannot all hold at once, or in which existence of the solution is assumed, would be a trivializing formalization and is not acceptable. The hypotheses here are taken from the page, which shows they are satisfiable (Remark 3.6(i), Lemma 3.8).
• Wanted contributions: first- and second-order calculus on $\mathcal P_2$ (Lions derivatives, the chain rule along $\mu\mapsto\mathcal L_{\xi+\varepsilon\eta}$, symmetry of $\partial_{\tilde x\mu}$). These are reusable for any mean field problem.

Selected references

• W. Gangbo, A. R. Mészáros, C. Mou, J. Zhang, Mean field games master equations with nonseparable Hamiltonians and displacement monotonicity, Ann. Probab. 50(6), 2178–2217, 2022. https://doi.org/10.1214/22-AOP1580
• J.-M. Lasry, P.-L. Lions, Mean field games, Jpn. J. Math. 2, 229–260, 2007. https://doi.org/10.1007/s11537-007-0657-8
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The Master Equation and the Convergence Problem in Mean Field Games, Annals of Mathematics Studies 201, Princeton University Press, 2019. https://doi.org/10.2307/j.ctvckq7qf
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I–II, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• W. Gangbo, A. R. Mészáros, Global well-posedness of master equations for deterministic displacement convex potential mean field games, Comm. Pure Appl. Math. 75, 2685–2801, 2022. https://doi.org/10.1002/cpa.22069

Motivation

A large stochastic game has one state process per player. Each player's feedback changes with the empirical distribution of all states, so a finite population remains coupled even when the idiosyncratic Brownian motions are independent. A useful quantitative question is whether a statistic of the entire collection of equilibrium trajectories can deviate substantially from its mean as the population grows. Delarue, Lacker, and Ramanan answer this for smooth closed-loop mean-field games in their large-deviations and concentration paper. Their result concerns the equilibrium state paths themselves, rather than only a fixed-time empirical measure.

The paper is part of a two-paper limit theory. Its companion central-limit paper supplies the Nash-to-McKean–Vlasov estimates quoted here as Theorems 4.1 and 4.2. The concentration argument also uses transport inequalities: Gozlan's dimension-free characterization explains the quadratic transport assumption on the initial law, while Djellout, Guillin, and Wu provide a transport principle for diffusion path laws. The present mission records the paper's main concentration theorem and four of its explicit intermediate targets.

Setting

Fix a horizon $T>0$ and a positive state dimension $d$. Player $i$ has a continuous state path $X^i\in C^d=C([0,T];\mathbb R^d)$. The empirical measure of a vector $x=(x^1,\ldots,x^n)$ is $m_x^n=n^{-1}\sum_i\delta_{x^i}$; the same formula applies to paths. The norm on $C^d$ is $\|x\|_\infty=\sup_{t\le T}|x_t|$, and the product norm relevant to this mission is $\|x\|_{n,2}=(\sum_i\|x^i\|_\infty^2)^{1/2}$.

The game is posed on a filtered probability space with a common Wiener process $W$, independent idiosyncratic Wiener processes $B^i$, and i.i.d. initial states $X^i_0$ of law $\mu_0$. The action space is Polish. A drift $b(x,m,a)$, running cost $f(x,m,a)$, and terminal cost $g(x,m)$ specify the control problem. The Hamiltonian $H(x,m,y)$ minimizes $b(x,m,a)\cdot y+f(x,m,a)$ over actions; a selected minimizer $\hat\alpha$ defines $\hat b=b(\cdot,\hat\alpha)$ and $\hat f=f(\cdot,\hat\alpha)$.

Classical solutions $v^{n,i}$ of the $n$-player Nash system (2.6) determine the feedback in the equilibrium state equation (2.7). A classical solution $U$ of the master equation (2.8) determines the comparison particle equation (4.1). Both equations retain common-noise terms in their definitions. The goal sets the common-noise coefficient $\sigma_0$ to zero. Assumption A imposes Hamiltonian attainment, Lipschitz $\hat b$, nondegenerate idiosyncratic diffusion, an initial moment above order four, and the stated classical solutions. Either B or B′ controls the selected running cost; B′ also bounds $U$ and $v^{n,i}$ as specified on pp. 8–9.

Formalization targets

The goal is Theorem 3.4. If $\mu_0$ satisfies the quadratic transport inequality $W_2(\mu_0,\nu)\le\sqrt{2\kappa R(\nu\mid\mu_0)}$ for every $\nu\ll\mu_0$ with finite second moment, then constants $C,\delta_1,\delta_2>0$ exist such that, for $a>0$, $n\ge C/a^2$, and every 1-Lipschitz $\Phi$ on the product path space,

$$P\!\left(\Phi(X)-E\Phi(X)>a\right) \le 2n\exp(-\delta_1a^2n)+2\exp(-\delta_2a^2).$$

The four milestones retain the paper's two main comparison layers. Theorem 4.3 controls both the path-space Wasserstein distance between the Nash and comparison empirical measures and their synchronous squared path distance by $2n\exp(-\varepsilon^2n^2/\kappa_2)$ for $n\ge\kappa_1/\varepsilon$. Theorem 5.3 gives a dimension-uniform transport inequality and concentration bound for the law of a Lipschitz SDE in the coordinatewise product-supremum norm. Equation (5.7) bounds the change in a 1-Lipschitz path expectation when the deterministic initial vector changes. Theorem 5.4 gives $P(\Phi(\tilde X)-E\Phi(\tilde X)>a)\le2e^{-\delta a^2}$ for the interacting comparison system. The labels, constants, and domains follow the pinned preprint, pp. 12 and 16–20.

Significance

Theorem 3.4 supplies a finite-population tail estimate for every 1-Lipschitz observable of the entire equilibrium path vector. The first term becomes small at a population-dependent scale, while the second term has a rate independent of the number of players. This is stronger information than convergence of the empirical measure alone: it applies to path-dependent statistics and includes explicit deviation probabilities Theorem 3.4.

The mathematical statements are proved in the source paper, subject to its assumptions; Theorems 4.1 and 4.2 that support its comparison result are proved in the companion paper. The work here is to give these claims faithful machine-checkable statements and ultimately machine-checked proofs. The present draft is a set of open Lean theorem statements with sorry, so it asserts no completed formal proof. A completed development would also make its definitions of empirical path laws, Wasserstein continuity, flat derivatives, and interacting SDE solutions reusable for other mean-field models.

Difficulty

Independent-noise concentration cannot simply be applied to the Nash state paths. A player's drift depends on the empirical state measure and on a derivative of the $n$-player Nash solution, so changing one input can change every trajectory. The master equation describes a comparison system, but using it requires matching the Nash and master feedbacks on the same filtered probability space. The regularity in Assumptions A, B, and B′ is substantial: the master field has first and second derivatives in both space and measure, with uniform bounds. A formal proof must also preserve the exact path norm and the population-independent placement of constants. The SDE transport theorem's uniformity over dimensions is particularly consequential for Theorem 5.4 §§4–5.

Formalization scope

State vectors use finite-dimensional Euclidean spaces; time uses nonnegative reals and only $[0,T]$ is evaluated. A continuous path is a ContinuousMap on that interval with its supremum norm. Finite products use PiLp 2; the scalar-coordinate version of the norm is used for Theorem 5.3. Players are indexed from zero, corresponding to the paper's indices $1,\ldots,n$, and every theorem requires $n\ge1$. Probabilities and entropy are extended nonnegative values. Transport distances stay extended until a finite-moment hypothesis justifies their real value.

The filtered Wiener processes, i.i.d. initial states, Borel coefficients, Polish action space, Nash and master PDEs, and either B or B′ are represented explicitly. The master equation is imposed on $\mathcal P_2$; its spatial gradient is also required on $\mathcal P_{p_*}$, as Assumption A(5) specifies. A flat measure derivative is a normalized witness satisfying (2.2), while spatial derivatives are actual Fréchet derivatives. SDE solutions are path-valued processes satisfying coordinate Itô integral relations; solution families are supplied as hypotheses, since their existence is asserted by the source. Expectations appearing in the conclusions are stated integrable, so a default zero integral cannot satisfy a tail bound accidentally. The model cannot be replaced by arbitrary paths or a vacuous solution predicate: the Nash and comparison paths must satisfy their respective equations with the same noises and initial states.

The mission includes Theorem 4.3, Theorem 5.3, (5.7), and Theorem 5.4. The quoted Theorems 4.1 and 4.2, the general transport equivalence of Theorem 5.1, and tensorization in Theorem 5.2 remain useful later contributions, with their original hypotheses and conclusions intact. The printed constant in the “moreover” clause of Theorem 5.1 is omitted because it is dimensionally incorrect; no substitute assertion is placed in this mission.

Selected references

• F. Delarue, D. Lacker, and K. Ramanan, From the master equation to mean field game limit theory: Large deviations and concentration of measure, Annals of Probability 48 (2020), 211–263; formalization follows arXiv:1804.08550v1.
• F. Delarue, D. Lacker, and K. Ramanan, From the master equation to mean field game limit theory: A central limit theorem, preprint (2018), arXiv:1804.08542.
• N. Gozlan, A characterization of dimension free concentration in terms of transportation inequalities, Annals of Probability 37 (2009), 2480–2498, doi:10.1214/09-AOP470.
• H. Djellout, A. Guillin, and L. Wu, Transportation cost-information inequalities and applications to random dynamical systems and diffusions, Annals of Probability 32 (2004), 2702–2732, doi:10.1214/009117904000000531.

Motivation

Many problems in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer over a set with manifold structure: sparse principal component analysis over the Stiefel manifold, sparse blind deconvolution over the sphere, and clustering and dictionary-learning models with orthogonality constraints. In Euclidean space the standard method for such composite problems is the proximal gradient method, whose $O(1/k)$ rate for convex problems is classical (Beck–Teboulle 2009). Huang and Wei (arXiv:1909.06065v4, Mathematical Programming 2021) propose a Riemannian proximal gradient method (RPG) that solves its proximal subproblem on the tangent space and returns to the manifold through a retraction. They prove three things about it: global convergence, an $O(1/k)$ rate under a convexity notion adapted to retractions, and local rates under a Riemannian Kurdyka–Łojasiewicz property. This mission covers the second result, Theorem 3.2.

Earlier Riemannian proximal methods either required the exponential map and parallel transport, or solved a Euclidean proximal problem in the ambient space (Chen, Ma, So, Zhang 2020, ManPG). Theorem 3.2 is stated for a general retraction, with an explicit constant.

Setting

Let $\mathcal M$ be a finite-dimensional Riemannian manifold, with inner product $\langle\cdot,\cdot\rangle_x$ and norm $\|\cdot\|_x$ on each tangent space $T_x\mathcal M$. A retraction is a family of smooth maps $R_x:T_x\mathcal M\to\mathcal M$ with $R_x(0_x)=x$ and $\mathrm DR_x(0_x)=\mathrm{id}$. The problem is

$$\min_{x\in\mathcal M} F(x)=f(x)+g(x),$$

where $f$ is differentiable with Riemannian gradient $\operatorname{grad} f$, and $g$ is continuous and possibly nonsmooth.

For a function $h$ on a real inner-product space $V$, the Clarke generalized directional derivative is $h^\circ(\eta;v)=\limsup_{\xi\to\eta,\,t\downarrow0}(h(\xi+tv)-h(\xi))/t$. The generalized subdifferential is $\partial h(\eta)=\{\zeta\mid\langle\zeta,v\rangle\le h^\circ(\eta;v)\ \forall v\}$. A point $\eta$ is stationary for $h$ if $0\in\partial h(\eta)$.

Given a constant $\tilde L$, the RPG method (Algorithm 1) produces iterates $x_k$ and steps $\eta^*_{x_k}\in T_{x_k}\mathcal M$ as follows. Set

$$\ell_{x_k}(\eta)=\langle\operatorname{grad} f(x_k),\eta\rangle_{x_k}+\frac{\tilde L}{2}\|\eta\|_{x_k}^2+g(R_{x_k}(\eta)).$$

Choose a stationary point $\eta^*_{x_k}$ of $\ell_{x_k}$ on $T_{x_k}\mathcal M$ with $\ell_{x_k}(0)\ge\ell_{x_k}(\eta^*_{x_k})$, and set $x_{k+1}=R_{x_k}(\eta^*_{x_k})$.

The assumptions involve the sublevel set $\Omega_{x_0}=\{x\mid F(x)\le F(x_0)\}$ and two notions defined with respect to $R$ on a set $\mathcal N$:

• $L$-retraction-smoothness: $h(R_x(\eta))\le h(x)+\langle\operatorname{grad} h(x),\eta\rangle_x+\frac L2\|\eta\|_x^2$;
• retraction-convexity: $q_x=h\circ R_x$ satisfies $q_x(\eta)\ge q_x(\xi)+\langle\zeta,\eta-\xi\rangle_x$, where $\zeta$ is the gradient of $q_x$ at $\xi$, or any Riemannian subgradient of $q_x$ at $\xi$ when $h$ is nonsmooth.

Assumption 3.1 asks that $F$ be bounded below and $\Omega_{x_0}$ compact. Assumption 3.3 provides an open $\Omega\supseteq\Omega_{x_0}$ on which $f$ is $L$-retraction-smooth and retraction-convex and $g$ is retraction-convex. Assumption 3.4 bounds how far the retraction is from Euclidean: for all $x,y,z\in\Omega$,

$$\bigl|\|R_x^{-1}(z)-R_x^{-1}(y)\|_x^2-\|R_y^{-1}(z)\|_y^2\bigr|\le\kappa_\Omega\|R_x^{-1}(y)\|_x^2 .$$

Finally, $\beta=(\tilde L-L)/2$.

Formalization targets

Goal: Theorem 3.2

Let $\tilde L>\max(L,0)$, suppose Assumptions 3.1, 3.3 and 3.4 hold, and let $x_*$ be any accumulation point of $\{x_k\}$. Then for every $k\ge1$

$$F(x_k)-F(x_*)\le\frac1k\left(\frac{\tilde L}{2}\|R_{x_0}^{-1}(x_*)\|_{x_0}^2+\frac{\tilde L\kappa_\Omega}{2\beta}\bigl(F(x_0)-F(x_*)\bigr)\right).\tag{3.16}$$

The constants are those of the paper.

Milestones

1. Lemma 3.1 (descent): $F(x_k)-F(x_{k+1})\ge\beta\|\eta^*_{x_k}\|_{x_k}^2$.
2. Lemma 3.4 (Riemannian three-point inequality): for one step $z=R_x(\eta^*_x)$ and any $y=R_x(\xi_x)\in\Omega$, $F(z)\le F(y)+\frac{\tilde L}{2}(\|\xi_x\|_x^2-\|\xi_x-\eta^*_x\|_x^2)$.
3. (3.17): the one-step estimate obtained from Lemma 3.4 with $y=x_*$ and from Assumption 3.4.
4. (3.18): the one-step estimate with $\|\eta^*_{x_k}\|^2$ replaced by the decrease of $F$.
5. (3.19): the averaged estimate over the first $k$ steps.

Significance

Theorem 3.2 extends the $O(1/k)$ function-value rate of the proximal gradient method to manifolds and general retractions. The constant is explicit: it combines the initial distance $\|R_{x_0}^{-1}(x_*)\|$ with a correction proportional to $\kappa_\Omega$, which measures how far the retraction is from Euclidean. In the Euclidean case $R_x(\eta)=x+\eta$ one can take $\kappa_\Omega=0$, and the bound reduces to the classical one. The rate concerns $F(x_k)-F(x_*)$, which the iteration bound of Theorem 3.1 (the norm of $\eta^*_{x_k}$) does not control.

The result is proved in the paper. None of it is formalized, and no machine-checked version of the Euclidean proximal-gradient rate is on the platform either. A formalization would supply the first checked version of Clarke stationarity on tangent spaces, of the retraction-based convexity and smoothness notions, and of a rate proof for a nonsmooth Riemannian algorithm. These pieces carry over to other retraction-based methods, such as the accelerated variants of §4 of the paper.

Difficulty

The arithmetic of the rate proof is a telescoping sum, so the work lies elsewhere. First, Lemma 3.4 needs a usable form of the stationarity condition $0\in\partial\ell_x(\eta^*_x)$: a subgradient of $g\circ R_x$ at $\eta^*_x$ equal to $-(\operatorname{grad} f(x)+\tilde L\eta^*_x)$. This requires a sum rule for the Clarke subdifferential of a $C^1$ function plus a locally Lipschitz one, on a tangent space whose norm comes from the Riemannian metric rather than from the model space. Second, the gradient of $f\circ R_x$ at $0_x$ has to be identified with $\operatorname{grad} f(x)$ through $\mathrm DR_x(0_x)=\mathrm{id}$. In Mathlib this mixes manifold derivatives (mfderiv) with Fréchet derivatives on a space carrying two equivalent norms. Third, it has to be shown that the iterates and the accumulation point remain in $\Omega$, so that Assumptions 3.3 and 3.4 apply at every step.

Formalization scope

Theorem numbers and pages are those of arXiv:1909.06065v4. $\mathcal M$ is a smooth manifold modelled on a finite-dimensional real inner-product space $E$, with Mathlib's RiemannianBundle on the tangent bundle. All norms and inner products on $T_x\mathcal M$ are the Riemannian ones. Retractions and gradients are the published RiemOpt.BFGS.IsRetraction and RiemOpt.FR.IsGradient. The Clarke derivative is an EReal-valued limit superior along $\mathcal N(\eta)\times\mathcal N_{>0}(0)$. Algorithm 1 is modelled as a run (sequences $x_k$, $\eta^*_{x_k}$ with the three defining properties), and every statement holds for every run. Indices start at $0$, accumulation points are cluster points of the sequence, and the bounds divided by $k$ are stated for $k\ge1$.

The formalization commits to the following readings:

1. $L$-retraction-smoothness is required for every tangent vector at the points of the set. This is a strengthening of Definition 3.1, which only covers $\eta$ with $R_x(\eta)$ in the set, and it is needed because Lemma 3.1 fails under the literal reading.
2. In retraction-convexity the vector $\zeta$ depends on $\xi$. It is the gradient of $f\circ R_x$, respectively any Clarke subgradient of $g\circ R_x$, as the sentence after (3.10) states.
3. $\kappa_\Omega$ is a single constant.
4. $R^{-1}$ is data with $R_x(R_x^{-1}(y))=y$ on $\Omega$, together with the identification $R_{x_k}^{-1}(x_{k+1})=\eta^*_{x_k}$ that the proof uses.
5. Local Lipschitz continuity of $g\circ R_x$ is assumed, as p. 5 presupposes when it defines the subdifferential.

A single $\zeta$ for all $\eta,\xi$ in (3.10) would make retraction-convexity force $q_x$ to be affine, and the theorem would only cover affine problems. That reading is excluded. Statements with the case $k=0$, where Lean's $1/0=0$ makes (3.16) false, are excluded as well.

Contributions welcome: a Clarke sum rule for $C^1$ plus locally Lipschitz functions, the identification of the Fréchet derivative of $f\circ R_x$ at $0$ with the Riemannian gradient, and the five milestones in order. The Clarke layer and the derivative identification are reusable beyond this mission.

Selected references

• W. Huang, K. Wei, Riemannian proximal gradient methods, Mathematical Programming, 2021; extended version arXiv:1909.06065v4. https://arxiv.org/abs/1909.06065v4, https://doi.org/10.1007/s10107-021-01632-3
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sciences, 2009. https://doi.org/10.1137/080716542
• S. Chen, S. Ma, A. M.-C. So, T. Zhang, Proximal gradient method for nonsmooth optimization over the Stiefel manifold, SIAM J. Optimization, 2020. https://doi.org/10.1137/18M122457X
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

Motivation

Every square-integrable martingale of a Brownian filtration is a stochastic integral, $Y(T)=E[Y(T)]+\int_0^T\phi\cdot dW$ (Itô's representation theorem). The classical theorem gives no formula for $\phi$. In hedging, $\phi$ is the replicating strategy of a claim. In filtering and stochastic control it is the quantity one has to compute. The Clark–Haussmann–Ocone formula identifies $\phi(t)=E[D_tH\mid\mathcal F_t]$ through the Malliavin derivative $D$. That derivative is anticipative, defined only up to null sets, and acts on the Wiener space rather than on the observed path.

Cont and Fournié (arXiv:1002.2446, Ann. Probab. 2013) develop a nonanticipative alternative from Dupire's functional Itô calculus (Dupire 2009). The integrand of the representation is a vertical derivative $\nabla_XY$, computed pathwise from a functional representation $Y(t)=F_t(X_t,A_t)$ of the martingale. Their main structural result is that this derivative, first defined on regular functionals, extends to all square-integrable stochastic integrals and inverts the Itô integral there. This mission formalizes that extension.

Timeline:

• 1940s–1950s. Itô constructs the stochastic integral and proves the representation theorem for Brownian functionals.
• 1970–1984. Clark (1970), Haussmann (1979) and Ocone (1984) give the explicit formula through the Malliavin derivative.
• 2009. Dupire introduces horizontal and vertical derivatives of path functionals.
• 2010. Cont and Fournié prove a change-of-variable formula for path functionals (J. Funct. Anal. 259, 2010).
• 2013. Cont and Fournié prove the Itô formula used here (their Theorem 4.1, the subject of the companion mission) and the extension theorem of this mission.

Setting

Fix a horizon $T$ and a dimension $d$. A path is a map $x:[0,\infty)\to\mathbb R^d$. A path is cadlag on $[0,t]$ if it is right-continuous there with left limits. The stopped path is $x_t(u)=x(u\wedge t)$, and the vertical perturbation $x_t^e$ shifts the value at time $t$ by $e\in\mathbb R^d$ while keeping $x$ on $[0,t)$. Paths $v$ with values in the positive semidefinite matrices $S_d^+$ carry the density of the quadratic variation.

A nonanticipative functional $F_t(x,v)$ depends only on $(x_t,v_t)$. Its vertical derivative $\nabla_xF_t(x,v)\in\mathbb R^d$ is the gradient at $e=0$ of $e\mapsto F_t(x_t^e,v_t)$. Its horizontal derivative $\mathcal D_tF(x,v)$ is the right derivative of $h\mapsto F_{t+h}(x_t,v_t)$ along the flat extension. The class $\mathbb C_b^{1,2}([0,T))$ consists of functionals with the following properties:

• $F$ is left-continuous for the distance $d_\infty$ of (9);
• $\mathcal DF$ is continuous at fixed times;
• $\nabla_xF$ and $\nabla_x^2F$ exist and are left-continuous;
• $\mathcal DF$, $\nabla_xF$ and $\nabla_x^2F$ are bounded on bounded sets of paths.

All functionals also satisfy (10), $F_t(x,v)=F_t(x,v_{t-})$.

Assumption 5.1. $W$ is a standard $d$-dimensional Brownian motion, and

$$X(t)=X(0)+\int_0^t\sigma(u)\cdot dW(u),\qquad\det\sigma(t)\ne0\quad dt\times d\mathbb P\text{-a.e.},$$

with $\sigma$ adapted to $\mathcal F^W$. The density $A=\sigma\sigma^\top$ of $[X]$ is cadlag and adapted. The working filtration is $\mathcal F=\mathcal F^X$, the completed natural filtration of $X$, right-continuous on $[0,T)$.

The spaces involved are:

• $\mathcal L^2(X)$: progressive $\varphi$ with $\|\varphi\|^2=E\int_0^T\varphi^\top A\varphi\,dt<\infty$;
• $\mathcal I^2(X)$: the Itô integrals $\int_0^\cdot\varphi\cdot dX$, with norm $E[Y(T)^2]$;
• $D(X)$: the processes of $\mathcal I^2(X)$ that equal $F_t(X_t,A_t)$ for some $F\in\mathbb C_b^{1,2}$, with $\nabla_XY(t)=\nabla_xF_t(X_t,A_t)$;
• $\mathcal W^{1,2}(X)$: the closure of $D(X)$ in $\mathcal I^2(X)$.

Formalization targets

Goal: Theorem 5.8 with (56)

The operator $\nabla_X:D(X)\to\mathcal L^2(X)$ is closable on $\mathcal W^{1,2}(X)$. Its closure is a bijective isometry

$$\nabla_X:\mathcal W^{1,2}(X)\to\mathcal L^2(X),\qquad\int_0^\cdot\varphi\cdot dX\mapsto\varphi,$$

and $\nabla_XY$ is the unique element of $\mathcal L^2(X)$ with

$$E[Y(T)Z(T)]=E\int_0^T\nabla_XY\,\nabla_XZ\,d[X]\quad\text{for all }Z\in D(X).$$

In particular $\nabla_X\big(\int_0^\cdot\varphi\,dX\big)=\varphi$ in $\mathcal L^2(X)$. The adjoint identity (55),

$$E\Big[Y(T)\int_0^T\varphi\cdot dX\Big]=E\int_0^T\nabla_XY\,\varphi\,d[X],$$

is a separate item.

Milestones

1. Corollary 4.4. Two $\mathbb C_b^{1,2}$ representations of one process have vertical derivatives that agree in the $A(t-)$-seminorm, outside an evanescent set.
2. Theorem 5.2. $Y(T)=Y(0)+\int_0^T\nabla_xF_t(X_t,A_t)\,dX(t)$ for a martingale with a $\mathbb C_b^{1,2}$ representation.
3. Proposition 5.5. $E[Y(T)Z(T)]=E\int_0^T\nabla_XY\,\nabla_XZ\,d[X]$ on $D(X)$.
4. The cylindrical functional of Lemma 5.7's proof is in $\mathbb C_b^{1,2}$ with the stated derivatives, and its evaluation on $(X,A)$ equals the stochastic integral of the cylindrical integrand.
5. Lemma 5.7. $\{\nabla_XY:Y\in D(X)\}$ is dense in $\mathcal L^2(X)$, and $\mathcal W^{1,2}(X)=\mathcal I^2(X)$.

Significance

The theorem identifies the integrand of the martingale representation of any square-integrable $\mathcal F^X$-martingale as a limit of pathwise derivatives. On regular functionals, those derivatives are computed by perturbing the endpoint of the observed path. The integrand is therefore adapted by construction, and it can be approximated by finite differences. This is the basis of the paper's general representation formula (Theorem 5.9) and of its comparison with Malliavin calculus (Theorem 6.1, $\nabla_XY(t)=E[D_tH\mid\mathcal F_t]$). The isometry also gives $\mathcal W^{1,2}(X)$ the structure of a Hilbert space on which $\nabla_X$ is a weak derivative. This is a nonanticipative counterpart of the Wiener–Sobolev space $\mathbb D^{1,2}$.

The results are proved in the paper; none of them has a machine-checked proof. Neither Mathlib nor the platform has a square-integrable Itô integral with its isometry, a functional Itô calculus, or a martingale representation theorem. A complete development would provide the first formal statement and proof of a martingale representation formula with an explicit, nonanticipative integrand. The path-space and $\mathcal L^2(X)$ layers are reusable for any work on path-dependent functionals.

Difficulty

The proof of the goal is short once its inputs are available, but each input is substantial.

• Proposition 5.5 needs Theorem 5.2, which needs the functional Itô formula (Theorem 4.1 of the paper, the companion mission). It also needs the uniqueness of the decomposition of a continuous semimartingale.
• Lemma 5.7 needs the totality of cylindrical integrands $f(X(t_1),\dots,X(t_n))1_{t>t_n}$ in $\mathcal L^2(X)$. This is a monotone-class argument tied to the filtration being generated by $X$, and it fails for a larger filtration (take $\sigma=\operatorname{sgn}(W)$ in dimension one and the filtration of $W$).
• Corollary 4.4 converts an identity of processes into an identity of integrands. This needs the quadratic variation of a stochastic integral and left-continuity of the integrand, and it gives nothing at $t=0$.

A tempting shortcut is to define $\nabla_X$ on $\mathcal I^2(X)$ as the inverse of the Itô integral. That makes (56) a tautology and erases the link with the pathwise derivative, so the closure must be built from $D(X)$.

Formalization scope

Time is $\mathbb R_{\ge0}$, statements are made on $[0,T)$, and functionals are defined on all paths, with every quantifier over path space restricted to cadlag pairs. The derivatives of a functional are explicit witnesses tied to it by HasDerivWithinAt and HasFDerivAt, so a derivative is never a junk value. The distance $d_\infty$ uses the max norm on $\mathbb R^d\times S_d^+$ (sup norm on vectors, entrywise sup norm on matrices) and appears only through explicit bounds.

The formal setting makes these hypotheses explicit:

1. The filtration is the completed natural filtration of $X$. Its right-continuity and $A$'s adaptedness on the horizon are included from §2.
2. $E[X](T)<\infty$, through the square-integrable Itô integral defining $X$.
3. $\sigma$ is progressively measurable, and $X(0)$ is $\mathcal F^W_0$-measurable.
4. All paths of $X$ are continuous and all paths of $A$ are cadlag.

In $d$ dimensions, $\varphi^2\,d[X]$ means $\varphi^\top A\varphi\,dt$. The square-integrable Itô integral is a relation, defined through simple dyadic integrands and an almost-surely continuous integral process on $[0,T]$. This continuity selects the stochastic integral version from the limits at fixed times. The derivative of each test process is required to belong to $\mathcal L^2(X)$, as Definition 5.4 states. Theorem 5.2 integrates by dyadic left Riemann sums in probability (EthierKurtz.itoStepSum). Corollary 4.4 is stated for $0<t<T$, because the printed version fails at $t=0$.

The statements must not be trivialized. The closure of $\nabla_X$ is a relation, and its existence, uniqueness up to $\mathcal L^2(X)$-null sets, isometry and surjectivity are all conclusions, never definitions. Expectations of squares are lower integrals in $[0,\infty]$, and every real expectation in (51), (53) and (55) comes with its integrability as part of the conclusion. $\mathcal L^2(X)$ is not reduced to $\{0\}$, because $\det\sigma\ne0$. A derivative witness cannot be chosen freely, because it is tied to $F$.

Contributions are welcome on:

• the $L^2$ Itô integral and its isometry for continuous square-integrable martingales;
• the functional Itô formula, from the companion mission;
• the monotone-class density of cylindrical integrands;
• the left-limit and cadlag lemmas for path functionals.

Selected references

• R. Cont and D.-A. Fournié, Functional Itô calculus and stochastic integral representation of martingales, Ann. Probab. 41(1):109–133, 2013. https://arxiv.org/abs/1002.2446 (v5), https://doi.org/10.1214/11-AOP721
• R. Cont and D.-A. Fournié, Change of variable formulas for non-anticipative functionals on path space, J. Funct. Anal. 259(4):1043–1072, 2010. https://doi.org/10.1016/j.jfa.2010.04.017
• B. Dupire, Functional Itô calculus, Bloomberg Portfolio Research paper 2009-04, 2009. https://ssrn.com/abstract=1435551
• D. Ocone, Malliavin's calculus and stochastic integral representations of functionals of diffusion processes, Stochastics 12:161–185, 1984. https://doi.org/10.1080/17442508408833299
• P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005. https://doi.org/10.1007/978-3-662-10061-5

Motivation

The martingale optimal transport problem asks for a coupling of two probability measures $\mu,\nu$ on $\mathbb R$ that is the law of a one-step martingale and minimizes an expected cost. It arises in robust finance, where the marginals are the risk-neutral laws of an asset at two dates implied by option prices, and model-independent price bounds for exotic options are the extreme values of the problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014).

Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 44(1), 2016) construct a canonical martingale coupling, the left-curtain coupling, which plays the role that the monotone (quantile) coupling plays in classical transport. Its construction rests on one object, the shadow of a measure in another, and on one structural property of it: shadows are associative. This mission formalizes that property, Theorem 4.8 of the paper, together with the chain of results in §2.3 and §4.1–4.3 on which it rests.

Setting

Let $\mathcal M$ be the set of finite Borel measures on $\mathbb R$ with finite first moment, of any total mass. For $\mu,\nu\in\mathcal M$:

• the convex order $\mu\preceq_C\nu$ holds if $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (this forces equal masses and equal barycentres);
• the extended convex order $\mu\preceq_E\nu$ holds if the same inequality holds for every nonnegative convex $\varphi$; it holds both when $\mu\preceq_C\nu$ and when $\mu\le\nu$ setwise;
• the potential function of $\mu$ is $u_\mu(x)=\int|y-x|\,d\mu(y)$;
• a sequence $(\nu_n)$ converges weakly in $\mathcal M$ to $\nu$ if $\int f\,d\nu_n\to\int f\,d\nu$ for every continuous bounded $f$ and $\int|x|\,d\nu_n\to\int|x|\,d\nu$.

If $\mu\preceq_E\nu$, a shadow of $\mu$ in $\nu$ is a measure $\eta$ with (i) $\eta\le\nu$, (ii) $\mu\preceq_C\eta$, and (iii) $\eta\preceq_C\eta'$ for every $\eta'$ satisfying (i) and (ii). Lemma 4.6 of the paper shows that it exists and is unique; it is written $S^\nu(\mu)$. It is the least spread-out part of $\nu$ into which $\mu$ can be transported by a martingale. An atom is a measure $\alpha\,\delta_x$ with $\alpha\ge0$.

In the Lean development these objects are InM, ConvexLE, ExtConvexLE, potential, ConvergesInM and the predicate IsShadow ν μ η, in the namespace MartOT.Shadow.

Formalization targets

Goal: Theorem 4.8 (shadow of a sum), p. 25

For $\gamma_1,\gamma_2,\nu\in\mathcal M$ with $\gamma_1+\gamma_2\preceq_E\nu$,

$$\gamma_2\preceq_E\nu-S^\nu(\gamma_1)\qquad\text{and}\qquad S^\nu(\gamma_1+\gamma_2)=S^\nu(\gamma_1)+S^{\nu-S^\nu(\gamma_1)}(\gamma_2).$$

Milestones, in attack order

1. Proposition 4.2 (p. 21): for equal masses, $\mu\preceq_C\nu\iff u_\mu\le u_\nu$; $\mu\le\nu\iff u_\nu-u_\mu$ is convex; for fixed mass and mean, convergence in $\mathcal M$ is pointwise convergence of potential functions.
2. Proposition 4.4 (p. 21): $\mu\preceq_E\nu$ implies $\mu\preceq_C\theta$ for some $\theta\le\nu$.
3. Lemma 4.6 (p. 23): existence, uniqueness and property (iii′) of the shadow.
4. Example 4.7 (p. 24): the shadow of an atom is the restriction of $\nu$ between two quantiles.
5. Lemma 4.11 (p. 27): $\eta-S^\eta(\delta)\le\nu-S^\nu(\delta)$ for an atom $\delta\preceq_E\eta\le\nu$.
6. Lemma 4.12 (p. 27): the goal when $\gamma_1$ is an atom.
7. Lemma 4.13 (p. 28): the shadow of finitely many atoms, built one atom at a time.
8. Lemma 2.9 (p. 15): approximation of $\gamma\in\mathcal M$ by a $\preceq_C$-increasing sequence of finitely supported measures below it.
9. Proposition 4.15 (p. 29): shadows pass to limits of $\preceq_C$-increasing sequences.
10. Lemma 4.16 (p. 29): the goal when $\gamma_2$ is an atom, with $\delta\preceq_E S^\nu(\gamma+\delta)-S^\nu(\gamma)$.

Significance

Theorem 4.8 is what makes the left-curtain coupling well defined and consistent. That coupling is the martingale plan which, for every $x$, sends $\mu|_{]-\infty,x]}$ onto $S^\nu(\mu|_{]-\infty,x]})$ (Theorem 4.18). Associativity says that the parts of $\nu$ assigned to $\mu|_{]-\infty,x]}$ and to $\mu|_{]x,x']}$ fit together into the part assigned to $\mu|_{]-\infty,x']}$, so the family of shadows defines a single coupling. The uniqueness of left-monotone martingale plans and the optimality of the left-curtain coupling for the costs $h(y-x)$ with $h'$ strictly convex, both later results of the paper, rest on it.

The result is proved in the paper. As far as is known it has no machine-checked proof. This mission produces a statement of it, and of the supporting results, in terms of measures of arbitrary finite mass with no reference to a chosen shadow function. A complete development would give Lean a theory of the convex order on finite measures through potential functions, which is reusable well beyond martingale transport.

Difficulty

For finitely atomic measures the identity follows by adding one atom at a time (Lemmas 4.12, 4.13, 4.16), but even the single-atom step needs a monotonicity property of shadows of atoms in varying targets (Lemma 4.11), and that property comes from their explicit description through quantile functions. The general case cannot be obtained by a direct manipulation of the minimality property (iii): minimality of $S^\nu(\gamma_1)$ and of $S^{\nu-S^\nu(\gamma_1)}(\gamma_2)$ separately says nothing obvious about minimality of their sum among measures dominating $\gamma_1+\gamma_2$, because a competitor for the sum need not split into competitors for the summands. The paper passes to the limit along convex-order approximations, which requires a continuity property of the shadow (Proposition 4.15) in the topology of $\mathcal M$.

Formalization scope

• Measures are MeasureTheory.Measure ℝ with membership in $\mathcal M$ stated explicitly (InM: finite measure, identity integrable). Masses are arbitrary; nothing is normalized to probability measures.
• Integrals of convex test functions are taken in EReal through the published ModelRiskOT.Duality.extIntegral (positive minus negative part), never as Bochner integrals, so a non-integrable test function cannot produce a junk value. The extended convex order uses lower Lebesgue integrals of nonnegative functions.
• Shadows are the predicate IsShadow ν μ η, never a function built by choice. Every statement about $S^\nu(\cdot)$ quantifies over all shadows, which with existence and uniqueness (Lemma 4.6, a milestone) is the paper's statement. Uniqueness is part of the conclusion of Lemma 4.6 and is not assumed elsewhere.
• $\nu-\eta$ is Mathlib's truncated subtraction of measures. It is used only where $\eta\le\nu$ is guaranteed by property (i) of a shadow. Lemma 4.16 additionally asserts $S^\nu(\gamma)\le S^\nu(\gamma+\delta)$, so that the difference there is a genuine one.
• Not a trivialization: in the goal, neither $\eta_1+\eta_2\le\nu$ nor $\gamma_1+\gamma_2\preceq_C\eta_1+\eta_2$ nor the minimality of $\eta_1+\eta_2$ is assumed; all three are the content of the conclusion IsShadow ν (γ1 + γ2) (η1 + η2).
• Added relative to the page: Lemma 4.11 states $\nu\in\mathcal M$, which the paper takes from context. Proposition 4.2's third bullet is split into an equivalence for each candidate limit and a uniqueness clause, which together are equivalent to the printed sentence. Lemma 4.10 (continuity of $\nu\mapsto S^\nu(\delta)$ in the Kantorovich metric) and Proposition 4.17 are not included.
• Needed infrastructure: potential functions and their second distributional derivatives, quantile functions of finite measures, weak convergence of finite measures with first moments. Contributions to any of these are welcome.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509v2, doi:10.1214/14-AOP966
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. doi:10.1007/s00780-013-0205-8
• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24(1), 312–336, 2014. doi:10.1214/13-AAP925
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. doi:10.1214/aoms/1177700153

Motivation

Martingale optimal transport asks for the cheapest way to couple two given laws $\mu$ and $\nu$ on $\mathbb R$ by a one-step martingale: a pair $(X,Y)$ with $X\sim\mu$, $Y\sim\nu$ and $E[Y\mid X]=X$. The problem arises in mathematical finance, where $\mu$ and $\nu$ are the risk-neutral laws of an asset at two maturities, implied by quoted vanilla option prices, and the extremal values of $E[c(X,Y)]$ over all such couplings are model-independent price bounds for the exotic payoff $c$ (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). In classical optimal transport on the line, a single coupling, the monotone (quantile) coupling, is optimal for a whole family of costs. Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 2016) identify its martingale counterpart, the left-curtain coupling $\pi_{lc}$, and determine costs for which it is optimal.

This mission formalizes one of those optimality results, Theorem 6.3: for product costs $c(x,y)=\varphi(x)\psi(y)$ with $\psi$ strictly convex and $\varphi$ decreasing, $\pi_{lc}$ is the unique optimizer.

Setting

Let $\mathcal M$ be the set of finite Borel measures on $\mathbb R$ with finite first moment. For $\mu,\nu\in\mathcal M$ the convex order $\mu\preceq_C\nu$ means $\int\phi\,d\mu\le\int\phi\,d\nu$ for every convex $\phi:\mathbb R\to\mathbb R$; it forces equal mass and equal mean. The extended convex order $\mu\preceq_E\nu$ asks this only for nonnegative convex $\phi$.

A transport plan from $\mu$ to $\nu$ is a measure $\pi$ on $\mathbb R\times\mathbb R$ with marginals $\mu$ and $\nu$; the set of them is $\Pi(\mu,\nu)$. It is a martingale transport plan, $\pi\in\Pi_M(\mu,\nu)$, if $y-x$ is $\pi$-integrable and

$$\int\rho(x)\,(y-x)\,d\pi(x,y)=0\quad\text{for every bounded Borel }\rho,$$

that is, the conditional law $\pi_x$ of $y$ given $x$ has barycentre $x$ for $\mu$-almost every $x$. For a cost $c:\mathbb R^2\to\mathbb R$ the cost of a plan is $E_\pi[c]=\int c\,d\pi\in(-\infty,+\infty]$, the value is $C_M(\mu,\nu)=\inf_{\pi\in\Pi_M(\mu,\nu)}E_\pi[c]$, and $\pi$ is optimal if it belongs to $\Pi_M(\mu,\nu)$ and attains this infimum.

For a plan $\pi$ and $t\in\mathbb R$, the measure $\nu^\pi_t=\mathrm{proj}^y_\#(\pi|_{(-\infty,t]\times\mathbb R})$ is where $\pi$ sends the left part $\mu|_{(-\infty,t]}$ of $\mu$. Given $\mu\preceq_E\nu$, the shadow $S^\nu(\mu)$ is the measure $\eta$ with $\eta\le\nu$ and $\mu\preceq_C\eta$ that is $\preceq_C$-below every other such measure. The left-curtain coupling of $\mu\preceq_C\nu$ is the plan $\pi_{lc}$ with

$$\mathrm{proj}^x_\#(\pi_{lc}|_{(-\infty,x]\times\mathbb R})=\mu|_{(-\infty,x]},\qquad \nu^{\pi_{lc}}_x=S^\nu(\mu|_{(-\infty,x]})\qquad(x\in\mathbb R).$$

It sends every left part of $\mu$ to the most concentrated part of $\nu$ that can receive it by a martingale.

Formalization targets

Goal: Theorem 6.3

Let $\mu\preceq_C\nu$ be finite measures, $\psi\ge0$ strictly convex, $\varphi\ge0$ strictly decreasing, $c(x,y)=\varphi(x)\psi(y)$, and assume $C_M(\mu,\nu)<+\infty$. Then

$$\pi_{lc}\ \text{is optimal, and every optimal }\pi\in\Pi_M(\mu,\nu)\text{ equals }\pi_{lc}.$$

Milestones

1. Lemma 4.6: for $\mu\preceq_E\nu$ in $\mathcal M$ the shadow exists and is unique.
2. Theorem 4.18: for $\mu\preceq_C\nu$ the left-curtain coupling exists, is unique, and lies in $\Pi_M(\mu,\nu)$.
3. Proof of Theorem 4.21: for every $\pi\in\Pi_M(\mu,\nu)$ and $s$, $\nu^\pi_s\le\nu$, $\mu|_{(-\infty,s]}\preceq_C\nu^\pi_s$, and $\nu^{\pi_{lc}}_s\preceq_C\nu^\pi_s$.
4. Equation (16): $\displaystyle\int\varphi(x)\psi(y)\,d\pi=\int_0^\infty\Big(\int\psi\,d\nu^\pi_{\{\varphi\ge t\}}\Big)dt$.
5. Equality case: for $\eta\preceq_C\eta'$ and $\psi$ strictly convex with $\int\psi\,d\eta'<\infty$, $\int\psi\,d\eta=\int\psi\,d\eta'$ iff $\eta=\eta'$.
6. §1.3: a plan in $\Pi(\mu,\nu)$ is determined by the family $(\nu^\pi_t)_{t\in\mathbb R}$.

Significance

Theorem 6.3 gives a class of costs for which the martingale transport problem has an explicit, cost-independent solution, and does so with uniqueness and without any regularity of $\varphi$ beyond monotonicity. In the financial reading, every payoff of the form $\varphi(X)\psi(Y)$ with these shape properties has its model-independent lower price bound attained by one and the same model, the left-curtain martingale, which depends only on the marginals. The result complements Theorem 6.1 of the same paper (costs $h(y-x)$ with $h'$ strictly convex), proved by a different, variational route.

The theorem is proved in the paper. No machine-checked version is known: neither the left-curtain coupling nor shadows nor martingale optimal transport on $\mathbb R$ appears in Mathlib or on the platform. A formalization produces the shadow construction, the left-curtain coupling as a Lean object with its characterization, and the comparison principle "$\pi_{lc}$ has the $\preceq_C$-least targets", all of which are reused by the other results of the series (uniqueness of the left-monotone plan, Theorem 6.1, the support bounds of §7).

Difficulty

The obvious argument compares costs plan by plan, but the convex order of two measures alone does not order the integrals of a strictly convex $\psi$ strictly: that $\int\psi\,d\eta=\int\psi\,d\eta'$ forces $\eta=\eta'$ requires representing $\eta'$ as a martingale image of $\eta$ (Strassen's theorem on $\mathbb R$) and the equality case of Jensen's inequality, with care about infinite integrals. The second obstacle is the passage from "equal targets for almost every level $t$ of $\varphi$" to "equal plans": the superlevel sets of a strictly decreasing $\varphi$ are half-lines that may be open or closed at the jumps of $\varphi$, so the targets must be controlled for both kinds of half-line, and a null set of levels must be bridged by monotonicity of $t\mapsto\nu^\pi_t$. Existence of shadows (Lemma 4.6) is itself a nontrivial construction through potential functions $u_\mu(x)=\int|y-x|\,d\mu(y)$.

Formalization scope

Measures are Mathlib Measure ℝ and Measure (ℝ × ℝ) with the Borel σ-algebras. $\mu$ and $\nu$ are finite, not necessarily probability, measures, as the theorem states; membership in $\mathcal M$ is part of ConvexLE. Integrals that may be infinite take values in EReal, through the published ModelRiskOT.Duality.extIntegral ($\int f^+-\int f^-$). $\Pi_M$ is encoded by the characterization above with bounded test functions $\rho$. The shadow and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain); their existence and uniqueness are milestones, never built into definitions. "Optimal" is minimality of cost over martingale plans; attainment is not assumed.

Two hypotheses are read into the printed statement. "Decreasing" is strict: with $\varphi\equiv1$ all martingale plans have the same cost $\int\psi\,d\nu$, and for $\mu$ uniform on $\{-1,1\}$, $\nu$ uniform on $\{-2,0,2\}$ there are infinitely many of them. $C_M(\mu,\nu)<+\infty$ is added, as the proof assumes a plan of finite cost; otherwise every plan is optimal. A formalization in which $\pi_{lc}$ is merely some plan, the cost is a Bochner integral (which is $0$ for non-integrable integrands), or optimality is taken among all plans rather than martingale plans would not be Theorem 6.3. Theorem 4.18 is stated for finite measures of equal mass, the generality Theorem 6.3 needs. Strassen's theorem is already posed on the platform (PalmQueueing.Ordering.strassen_cx) and is not restated.

A complete development needs the convex order on finite measures, shadows, the left-curtain coupling, a layer-cake identity for product integrands and the equality case of the convex order for strictly convex test functions. The shadow and left-curtain layers are reusable across the whole series; contributions to any milestone, and to general lemmas on the convex order of finite (not only probability) measures, are welcome.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509v2, doi:10.1214/14-AOP966
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17, 477–501, 2013. doi:10.1007/s00780-013-0205-8
• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24(1), 312–336, 2014. doi:10.1214/13-AAP925
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. doi:10.1214/aoms/1177700153