Probability

Motivation

A martingale transport plan between two laws $\mu$ and $\nu$ on $\mathbb R$ is a joint law of a pair $(X,Y)$ with $X\sim\mu$, $Y\sim\nu$ and $E[Y\mid X]=X$. Minimizing or maximizing $E[c(X,Y)]$ over such plans gives the model-independent price bounds of an option with payoff $c(X,Y)$ when the market quotes vanilla options at two maturities, and so fixes the marginal laws $\mu$ and $\nu$ of the asset price. For the forward-starting straddle, with payoff $|Y-X|$, the two bounds are the problems with costs $-|y-x|$ and $|y-x|$.

• 1965: Strassen (doi:10.1214/aoms/1177700153) shows that martingale plans between $\mu$ and $\nu$ exist if and only if $\mu$ and $\nu$ are in convex order.
• 2012: Hobson and Neuberger (doi:10.1111/j.1467-9965.2010.00473.x) identify the optimizer for $-|y-x|$ through a construction of dual maximizers, under conditions on the marginals.
• 2012: Hobson and Klimmek communicate a description of the optimizer for $+|y-x|$ to Beiglböck and Juillet, cited there as private communication (arXiv:1208.1509v2, §7.4 and reference 15).
• 2016: Beiglböck and Juillet (arXiv:1208.1509v2) prove existence, uniqueness and the shape of the optimizer for $|y-x|$ for every continuous starting law, using only the primal problem and their variational lemma.

Setting

$\mu$ and $\nu$ are Borel probability measures on $\mathbb R$ with finite first moments, in convex order: $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (Definition 2.1). $\Pi_M(\mu,\nu)$ is the set of measures $\pi$ on $\mathbb R^2$ with marginals $\mu$ and $\nu$ such that $y-x$ is $\pi$-integrable and

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

which is the paper's characterization (4) of "the disintegration $\pi_x$ has barycentre $x$". For the cost $c(x,y)=|y-x|$ the cost of a plan is $\int|y-x|\,d\pi\in[0,\infty)$, and $\pi$ is optimal if it minimizes this over $\Pi_M(\mu,\nu)$. $\mu$ is continuous if $\mu(\{x\})=0$ for every $x$.

$\mu\wedge\nu$ is the largest measure below both $\mu$ and $\nu$ (Example 2.5); $(\mathrm{Id}\otimes\mathrm{Id})_\#\eta$ is the image of $\eta$ under $x\mapsto(x,x)$, a measure on the diagonal $\Delta=\{(x,x)\}$. For $\Gamma\subseteq\mathbb R^2$, $\Gamma_x=\{y:(x,y)\in\Gamma\}$, and $\operatorname{graph}(T)=\{(x,T(x))\}$.

Formalization targets

Goal: Theorem 7.4 (p. 43)

If $\mu\preceq_C\nu$ and $\mu$ is continuous, there is a unique optimal $\pi_{\mathrm{abs}}\in\Pi_M(\mu,\nu)$ for $c(x,y)=|y-x|$; it is concentrated on a set $\Gamma$ with $|\Gamma_x|\le3$ for every $x$; and

$$\pi_{\mathrm{abs}}=(\mathrm{Id}\otimes\mathrm{Id})_\#(\mu\wedge\nu)+\pi_{\mathrm{go}},\qquad \pi_{\mathrm{go}}\ \text{concentrated on}\ \operatorname{graph}(T_1)\cup\operatorname{graph}(T_2)$$

for some functions $T_1,T_2:\mathbb R\to\mathbb R$.

Milestones, in attack order

1. Attainment of the minimum (§2.1, pp. 10–11).
2. Lemma 1.11, the variational lemma (p. 8).
3. Lemma 7.5, the sign of a three-point cost difference (pp. 43–44).
4. The forbidden configurations (24) on a finitely optimal set (p. 45).
5. The static part: $\pi|_\Delta=(\mathrm{Id}\otimes\mathrm{Id})_\#(\mu\wedge\nu)$ for every optimal $\pi$ (pp. 45–46).
6. Lemma 3.2, accumulation of uncountably many large fibres (p. 19).
7. At most two off-diagonal points per fibre (p. 46).
8. The reduced problem between $\mu-\mu\wedge\nu$ and $\nu-\mu\wedge\nu$ (p. 46).
9. Lemma 5.5, two Borel graphs (p. 35), and Lemma 5.6, uniqueness from at most two points per fibre (p. 36).

Significance

The theorem identifies the lower model-independent bound for the forward-starting straddle: the extremal model keeps the mass that $\mu$ and $\nu$ share in place and splits every other starting point between at most two destinations. With Theorem 7.3 for $-|y-x|$ it settles both bounds for continuous $\mu$ without any dual attainment, which is known to fail in general. The decomposition into a static part $\mu\wedge\nu$ and a part between marginals with $\bar\mu\wedge\bar\nu=0$ is a reduction that applies to other costs vanishing on the diagonal.

The result is proved in the paper; nothing in it has been machine-checked. The mission produces a formal statement of Theorem 7.4 and of each step of its proof, a Lean vocabulary for martingale transport on $\mathbb R$ shared with the other missions of this series, and the general measure-theoretic lemmas (3.2, 5.5, 5.6) that the structure theorems of the paper all use.

Difficulty

Lemma 7.5 and (24) are elementary; the work lies in passing from them to statements about measures. The variational lemma needs Kellerer's duality-type result for finitely optimal sets. The static part requires showing that a positive defect $\kappa=\mu\wedge\nu-\pi(\Delta\text{-projection})$ produces, at $\kappa$-almost every point, a forbidden configuration, which uses the disintegration of the moving part. The cardinality bound requires the accumulation argument of Lemma 3.2, and the forbidden configurations only hold for points that lie strictly inside the range of their own fibre, which the martingale condition supplies only almost everywhere. Uniqueness does not follow from strict convexity of a cost functional, since the problem is linear: it comes from the two-graph structure through Lemma 5.6, and it fails if $\mu$ has atoms (Remark 7.7).

Formalization scope

Measures are Mathlib Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. Costs are integrals in the extended reals through the published ModelRiskOT.Duality.extIntegral; the cost $|y-x|$ is nonnegative and, under finite first moments, finite. Martingale plans are encoded by condition (4), competitors by the same device. $\mu\wedge\nu$ is the infimum in Mathlib's complete lattice of measures, measure subtraction is Mathlib's truncated subtraction, cardinalities of fibres are Set.encard in $\mathbb N\cup\{\infty\}$, and "concentrated on $A$" is $\pi(A^c)=0$. Continuity of $\mu$ is $\mu(\{x\})=0$ for all $x$. As on the page, $\Gamma$, $T_1$ and $T_2$ in the goal carry no measurability requirement.

Two choices differ from a literal reading and are disclosed in the items: (24) carries the hypothesis $y^-<x<y^+$ of Lemma 7.5, which the page invokes and without which (24) is false; and the steps that do not need continuity of $\mu$ (the static part, the reduced problem) are stated without it.

A trivializing formalization is ruled out: $\mu\wedge\nu$ is the lattice infimum of measures, not a product and not a pointwise minimum of set values, and all four conjuncts of the goal (existence, uniqueness, the bound 3, the decomposition) are asserted together.

Reusable beyond this mission: the Setting layer (convex order, $\Pi_M$, competitors), Lemma 3.2, Lemma 5.5 (a Lusin–Novikov consequence) and Lemma 5.6. Proofs of any milestone, and infrastructure on disintegrations of plans on $\mathbb R^2$, 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
• D. Hobson, A. Neuberger, Robust bounds for forward start options, Mathematical Finance 22(1), 31–56, 2012. doi:10.1111/j.1467-9965.2010.00473.x
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. doi:10.1214/aoms/1177700153
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995 (Theorem 18.11). doi:10.1007/978-1-4612-4190-4

Motivation

In classical optimal transport on the real line, one coupling plays a distinguished role: the monotone (Hoeffding–Fréchet) coupling, which sends the $q$-quantile of the first marginal to the $q$-quantile of the second. It is canonical (every initial segment of the first marginal goes as far left as possible) and it is optimal for a whole family of costs at once.

Martingale optimal transport adds the constraint that the coupling be the law of a one-step martingale $(X, Y)$, $\mathbb E[Y\mid X]=X$. The problem arises in robust (model-independent) mathematical finance: prices of vanilla options fix the marginal laws $\mu$ of $X$ and $\nu$ of $Y$, and bounds on the price of an exotic option $c(X,Y)$ that hold under every arbitrage-free model are values of the martingale transport problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). Martingale couplings exist exactly when $\mu$ and $\nu$ are in convex order (Strassen 1965).

Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 44(1), 2016) asked for the martingale counterpart of the monotone coupling, and found it: the left-curtain coupling $\pi_{\mathrm{lc}}$. This mission formalizes its existence and uniqueness (Theorem 1.5), which is the foundation for the paper's later optimality results (Theorems 1.7, 6.1 and 6.3, other missions of this series).

Setting

All measures are Borel measures on $\mathbb R$ or $\mathbb R\times\mathbb R$. $\mathcal M$ is the set of finite measures $\mu$ with $\int|x|\,d\mu<\infty$. For $\mu,\nu\in\mathcal M$:

• Convex order $\mu\preceq_C\nu$: $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (Definition 2.1). It forces equal mass and equal mean. Extended convex order $\mu\preceq_E\nu$: the same inequality for nonnegative convex $\varphi$ only (Definition 4.3); it allows $\mu(\mathbb R)<\nu(\mathbb R)$.
• Martingale transport plans $\Pi_M(\mu,\nu)$: measures $\pi$ on $\mathbb R^2$ with marginals $\mu$ and $\nu$ and $\int\rho(x)(y-x)\,d\pi(x,y)=0$ for every bounded Borel $\rho$, that is, the conditional barycentre of $\pi_x$ is $x$ for $\mu$-a.e. $x$.
• Left-monotone plans (Definition 1.4): $\pi$ is concentrated on a Borel set $\Gamma$ that contains no three points $(x,y^-),(x,y^+),(x',y')$ with $x<x'$ and $y^-<y'<y^+$. Mass leaving a point $x$ to both sides of $y'$ forbids any later point $x'>x$ from sending mass to $y'$.
• Shadow (Lemma 4.6): for $\mu\preceq_E\nu$, $S^\nu(\mu)$ is the measure $\eta\le\nu$ with $\mu\preceq_C\eta$ that is least in the convex order among all such $\eta$: the least spread-out part of $\nu$ into which $\mu$ can be embedded by a martingale.
• Left-curtain coupling (Theorem 4.18): the plan $\pi_{\mathrm{lc}}$ with $\operatorname{proj}^x_\#(\pi_{\mathrm{lc}}|_{]-\infty,x]\times\mathbb R})=\mu|_{]-\infty,x]}$ and $\nu^{\pi_{\mathrm{lc}}}_x:=\operatorname{proj}^y_\#(\pi_{\mathrm{lc}}|_{]-\infty,x]\times\mathbb R})=S^\nu(\mu|_{]-\infty,x]})$ for every $x$.

In Lean these are InM, ConvexLE, ExtConvexLE, IsMartingalePlan, IsLeftMonotone, IsShadow, IsLeftCurtain and targetUpTo in the shared namespace MartOT.Var. The mission's own theorems are in MartOT.Curtain.

Formalization targets

Goal: Theorem 1.5 (p. 6)

For probability measures $\mu\preceq_C\nu$ on $\mathbb R$ with finite first moments,

$$\exists!\,\pi\quad\pi\in\Pi_M(\mu,\nu)\ \text{ and }\ \pi\text{ is left-monotone}.$$

Existence alone, or uniqueness only among left-curtain plans, is not the goal: the statement says that monotonicity alone singles out one martingale coupling.

Milestones

1. Lemma 4.6: shadows exist and are unique, and satisfy (iii′) for the extended order.
2. Monotonicity of shadows (§4.4, p. 31): $\mu\le\mu'\preceq_E\nu$ implies $S^\nu(\mu)\le S^\nu(\mu')$.
3. Theorem 4.18: $\pi_{\mathrm{lc}}$ exists, is unique, is a probability measure and lies in $\Pi_M(\mu,\nu)$.
4. Theorem 1.8: $\nu^{\pi_{\mathrm{lc}}}_t\preceq_C\nu^\pi_t$ for every $t$ and every $\pi\in\Pi_M(\mu,\nu)$.
5. Lemma 1.11 (variational lemma): an optimal plan of finite cost lives on a Borel set on which no finitely supported measure has a cheaper competitor.
6. Proof of Theorem 4.21: $\pi_{\mathrm{lc}}$ is optimal for every cost $c_{s,t}(x,y)=\mathbf 1_{]-\infty,s]}(x)|y-t|$.
7. Theorem 4.21: $\pi_{\mathrm{lc}}$ is left-monotone (the existence half of the goal).
8. Lemma 5.1: end-point behaviour of $\mu\preceq_C\nu$ at $\sup\operatorname{spt}\mu$ and $\inf\operatorname{spt}\mu$.
9. Lemma 5.2: a nonzero signed measure of mass $0$ is detected by a test function $g_{a,b}$ anchored in the support of its positive part.
10. Theorem 5.3: every left-monotone martingale plan is the left-curtain coupling of its marginals (the uniqueness half).

Significance

Theorem 1.5 identifies a canonical martingale coupling defined by a geometric property of its support alone. The paper then shows that $\pi_{\mathrm{lc}}$ is the unique optimizer of the martingale transport problem for costs $h(y-x)$ with $h'$ strictly convex (Theorem 1.7) and that it is characterized by the convex-order minimality of Theorem 1.8. The left-curtain coupling has since been studied and generalized in a series of works (for instance Henry-Labordère and Touzi 2016).

The result is proved in the paper. It has, as far as the platform's catalogue shows, no machine-checked proof: no statement about martingale transport plans, shadows or the left-curtain coupling exists on Prove2Me. A formal development would produce reusable infrastructure: the convex order on finite measures of arbitrary mass, shadows, and the passage between the barycentre characterization (4) of martingale plans and their disintegrations.

Difficulty

Existence is not the hard part in the abstract: a left-monotone plan can be obtained as an optimizer for a suitable cost via the variational lemma. The construction through shadows is more delicate: one must show that the shadows of the initial segments $\mu|_{]-\infty,x]}$ increase with $x$ (this rests on Theorem 4.8, the shadow of a sum) and that the resulting plan satisfies the martingale property.

Uniqueness is the main obstacle. The classical argument for uniqueness of optimal plans (averaging two candidates and using strict convexity) requires a continuous first marginal and does not apply to arbitrary $\mu$ with atoms. The paper's argument is specific to the problem: it compares $\nu^\pi_x$ with the shadow $\nu^{\pi_{\mathrm{lc}}}_x$ through the test functions $g_{u,v}$ and a case analysis at the support end-points, which needs the measure-theoretic Lemmas 5.1 and 5.2.

Formalization scope

• Measures are MeasureTheory.Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. The goal and Theorems 1.8, 4.18, 4.21 take $\mu,\nu$ probability measures (IsProbabilityMeasure) in convex order; Lemma 4.6, the shadow monotonicity, Lemma 5.1 and Theorem 5.3 work in $\mathcal M$, as the paper's Sections 4–5 do.
• Integrals of convex functions and costs are extended-real valued (EReal, through the published ModelRiskOT.Duality.extIntegral), so no Bochner integral of a non-integrable function enters a statement. $\Pi_M$ is encoded by characterization (4) of the paper, not by disintegrations.
• Shadows and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain), never chosen functions: their existence and uniqueness are milestones, not definitions. A formalization that defined $\pi_{\mathrm{lc}}$ by a choice and the left-monotone plan as "the left-curtain plan" would make the goal circular; the goal mentions only $\Pi_M$ and left-monotonicity.
• "$\pi(\Gamma)=1$" is written $\pi(\Gamma^c)=0$; the support of a measure is Mathlib's Measure.support.
• No hypothesis is added to any statement of the page. In Lemma 5.1, $\sup\operatorname{spt}\mu$ is the real supremum of the support under BddAbove; at $\mu=0$ Lean's convention $\sup\emptyset=0$ applies.
• Reading: Theorem 1.8's "minimal" is formalized as "least" (below every member of the family), which is how the paper uses it.
• Strassen's theorem is not restated; it is already posed on the platform as PalmQueueing.Ordering.strassen_cx.

Contributions are welcome at every level: proofs of the milestones, auxiliary lemmas on the convex order of finite measures (potential functions $u_\mu$, equality of mass and mean), and the equivalence between (4) and the disintegration form of the martingale property.

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.1509, 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. arXiv:1106.5929
• 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(2), 423–439, 1965. doi:10.1214/aoms/1177700153
• P. Henry-Labordère, N. Touzi, An explicit martingale version of the one-dimensional Brenier theorem, Finance Stoch. 20(3), 635–668, 2016. arXiv:1302.4854

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks: a stochastic gradient method that keeps an exponential moving average $m_n$ of past gradients and an exponential moving average $v_n$ of their coordinatewise squares, and divides the first by the square root of the second. Its practical success came well before any convergence theory for nonconvex objectives. Reddi, Kale and Kumar (2018) showed that Adam with constant momentum parameters can fail to converge even on convex problems, which made the question of under which parameter schedules Adam provably converges a live one.

Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 2021) answer it through the ODE method of stochastic approximation (Benaïm, 1999). This mission takes the paper's almost-sure convergence theorem for Adam with decreasing stepsizes, Theorem 5.2. Under a stepsize schedule in which $1 - \alpha_n$ and $1 - \beta_n$ shrink in proportion to the stepsize $\gamma_n$, the iterates converge almost surely to the critical points of the objective, provided they stay bounded.

Setting

Let $\xi$ be a random variable on a measurable space $\Xi$ with law $\mu$, let $f : \mathbb R^d \times \Xi \to \mathbb R$ be an integrand with gradient $\nabla f(x, \xi)$ in $x$, and set

$$F(x) = \mathbb E f(x, \xi), \qquad S(x) = \mathbb E\big(\nabla f(x,\xi)^{\odot 2}\big), \qquad \mathcal S = \nabla F^{-1}(\{0\}),$$

where $\odot 2$ is the coordinatewise square and $\mathcal S$ is the critical set. Let $\xi_1, \xi_2, \dots$ be iid copies of $\xi$ on a probability space $(\Omega, \mathcal F, \mathbb P)$.

Algorithm 5.1 takes stepsizes $\gamma_n > 0$, weights $\alpha_n, \beta_n \in [0,1]$ and a constant $\varepsilon > 0$. Starting from $x_0 \in \mathbb R^d$, $m_0 = v_0 = 0$ and $r_0 = \bar r_0 = 0$, it computes for $n \ge 1$, with all vector operations coordinatewise:

$$\begin{aligned} m_n &= \alpha_n m_{n-1} + (1-\alpha_n)\nabla f(x_{n-1}, \xi_n), & v_n &= \beta_n v_{n-1} + (1-\beta_n)\nabla f(x_{n-1}, \xi_n)^{\odot 2},\\ r_n &= \alpha_n r_{n-1} + (1 - \alpha_n), & \bar r_n &= \beta_n \bar r_{n-1} + (1 - \beta_n),\\ x_n &= x_{n-1} - \gamma_n \frac{\hat m_n}{\varepsilon + \sqrt{\hat v_n}}, & \hat m_n &= m_n / r_n,\quad \hat v_n = v_n / \bar r_n . \end{aligned}$$

The divisions by $r_n$, $\bar r_n$ are the bias correction.

The stepsizes satisfy Assumption 5.1: $\gamma_{n+1}/\gamma_n \to 1$, $\sum_n \gamma_n = +\infty$, $\sum_n \gamma_n^2 < +\infty$, and there are $a, b$ with $0 < b < 4a$, $(1-\alpha_n)/\gamma_n \to a$ and $(1-\beta_n)/\gamma_n \to b$. The limiting dynamics is the autonomous ODE $\dot z = h_\infty(z)$ on $\mathcal Z_+ = \mathbb R^d \times \mathbb R^d \times [0,\infty)^d$, written $(\mathrm{ODE}_\infty)$, with

$$h_\infty(x, m, v) = \Big( -\frac{m}{\varepsilon + \sqrt v},\ a(\nabla F(x) - m),\ b(S(x) - v) \Big).$$

Formalization targets

Goal: Theorem 5.2

Assume Assumption 2.2 (regularity and moments of $f$), $F$ coercive (2.3), $S(x) > 0$ coordinatewise (2.4), iid samples (4.1), Assumption 5.1, $\sup_{x\in K}\mathbb E\|\nabla f(x,\xi)\|^4 < \infty$ on compacts (4.2 i) with $p = 4$), that $F(\mathcal S)$ has empty interior, and that $(x_n, m_n, v_n)$ is bounded with probability one. Then, almost surely,

$$d(x_n, \mathcal S) \to 0, \qquad m_n \to 0, \qquad S(x_n) - v_n \to 0,$$

and if $\mathcal S$ is countable, almost surely $(x_n, m_n, v_n) \to (x^*, 0, S(x^*))$ for some $x^* \in \mathcal S$.

Milestones

1. Lemma 9.1 i)–ii): $r_n = 1 - \prod_{i=1}^n \alpha_i$, and $r_n$ increases to $1$.
2. §9.1: in the decomposition $\bar z_{n+1} = \bar z_n + \gamma_{n+1} h_\infty(\bar z_n) + \gamma_{n+1}\chi_{n+1} + \gamma_{n+1}\varsigma_{n+1}$ of $\bar z_n = (x_{n-1}, m_n, v_n)$, the remainder satisfies $\varsigma_n \to 0$ almost surely.
3. §9.1: the piecewise-affine interpolation of $(\bar z_n)$ on the times $\tau_n = \sum_{k\le n}\gamma_k$ is almost surely a bounded asymptotic pseudotrajectory of the semiflow of $(\mathrm{ODE}_\infty)$.
4. Proposition 7.13: $(\mathrm{ODE}_\infty)$ is well posed on $\mathcal Z_+$ and defines a semiflow $\Phi$.
5. Proposition 7.14 (after Benaïm): the limit set of a relatively compact asymptotic pseudotrajectory of a semiflow with a strict Lyapunov function lies in the set of equilibria.
6. Proposition 7.15: on the closed hull of the orbits of a compact set, $W_\delta = V_\infty - \delta\langle\nabla F(x), m\rangle + \delta\|S(x) - v\|^2$ is a strict Lyapunov function for some $\delta > 0$.

Significance

The theorem identifies a regime of Adam's hyperparameters, $1 - \alpha_n \sim a\gamma_n$ and $1 - \beta_n \sim b\gamma_n$ with $b < 4a$, in which the algorithm behaves like a gradient method with vanishing noise: the iterates approach critical points, the momentum dies out, and the second-moment estimate converges to $S(x_n)$. The condition $b < 4a$ ties the two averaging rates together. It is the condition under which the paper's Lyapunov function for the continuous dynamics decreases (Lemma 7.5). The argument structure is also a template for other adaptive methods: once the limiting ODE has a strict Lyapunov function, almost-sure convergence of the iterates follows from the same steps.

The paper proves the result on paper; none of it is machine-checked. A formal proof would also be the first formal instance on Prove2Me of the full ODE method for a concrete stochastic algorithm. That pipeline runs from the iterates to a perturbed Euler scheme, then to an asymptotic pseudotrajectory and a limit-set theorem, and finally to convergence. Benaïm's general results are being formalized separately on the platform (the asymptotic-pseudotrajectory definition this mission reuses comes from that effort), so the two developments meet in milestone 3.

Difficulty

The obvious approach is to treat Adam as stochastic gradient descent with a preconditioner and run a descent-lemma argument on $F(x_n)$. This fails because the update direction $\hat m_n/(\varepsilon + \sqrt{\hat v_n})$ is not a descent direction for $F$: $m_n$ lags behind $\nabla F(x_n)$. Any Lyapunov function has to involve the momentum, and $F$ alone does not decrease. The continuous-time energy $V_\infty$ decreases only weakly, and only its perturbation $W_\delta$ is strict, and only on compact sets. A second difficulty is that the stepsize-dependent coefficients $(1-\alpha_{n+1})/\gamma_{n+1}$ and the bias corrections $r_n$, $\bar r_n$ make the recursion a non-autonomous perturbation of the Euler scheme of $h_\infty$. The remainder must be shown to vanish along almost every path before the general theory applies. Finally, the abstract limit-set theorem needs the semiflow to be well defined on the closed set $\mathcal Z_+$, where $h_\infty$ involves $\sqrt v$ and is not Lipschitz at $v = 0$.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The state space $\mathcal Z$ is the product of three copies with Mathlib's max-of-factors norm, which is equivalent to the Euclidean norm of $\mathbb R^{3d}$ and leaves boundedness and limits unchanged. $F$ and $S$ are Bochner integrals against the law $\mu$. Assumption 2.2 makes the integrands integrable, so they are the true expectations. Moments are lower Lebesgue integrals. Algorithm 5.1 is a pathwise recursion adamIter, driven by a random sequence $\xi : \mathbb N \to \Omega \to \Xi$ whose index $0$ is unused. The iid hypothesis is iIndepFun with every $\xi_{n+1}$ of law $\mu$.

Two hypotheses are left implicit on the page and are added explicitly. The first is $\varepsilon > 0$. The second is $\alpha_1 < 1$ and $\beta_1 < 1$: Assumption 5.1 iii) permits $\alpha_1 = 1$, which gives $r_1 = 0$, and Lean's division by zero returns $0$. Lemma 9.1 is stated with $\gamma_n > 0$ and $\sum\gamma_n = \infty$, which its convergence claim needs. Semiflows are Flow ℝ≥0 on the subtype $\mathcal Z_+$, and the asymptotic pseudotrajectory and limit set are the published StochApproxDyn.LimitSet definitions. The ODE milestones 4–6 hold for abstract $F$, $S$ under Assumptions 7.1–7.2 with $0 < b \le 4a$, as in the paper's §7.

The goal concerns the iterates of Algorithm 5.1 itself. A statement about trajectories of $(\mathrm{ODE}_\infty)$, or one that replaces almost-sure boundedness by a bound uniform in $\omega$ together with deterministic gradients, is a different and much weaker theorem and is ruled out. The interior condition on $F(\mathcal S)$ and the countability of $\mathcal S$ enter exactly as on the page.

A complete development needs the following:

• well-posedness of the ODE on a closed set with a non-Lipschitz field;
• the Benaïm machinery: martingale-noise control via Doob's convergence theorem, and the passage from vanishing perturbations to asymptotic pseudotrajectories;
• the limit-set theorem for strict Lyapunov functions.

The last two are reusable for any stochastic approximation scheme, and contributions to them are welcome independently of Adam.

Selected references

• A. Barakat, P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• D. P. Kingma, J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
• S. J. Reddi, S. Kale, S. Kumar, On the Convergence of Adam and Beyond, ICLR 2018. https://arxiv.org/abs/1904.09237

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

Motivation

A forward-start straddle pays $|S_2 - S_1|$, the absolute change of an asset price between two future dates. A trader who knows the market prices of all vanilla options at both dates knows the laws $\mu$ of $S_1$ and $\nu$ of $S_2$, but not their joint law. Under a pricing measure the price is a martingale, so the admissible joint laws are exactly the martingale couplings of $\mu$ and $\nu$. The highest price consistent with the data is therefore the value of an optimization problem over martingale couplings: maximize $\mathbb E|S_2-S_1|$. Hobson and Neuberger (Robust bounds for forward start options, 2012) studied this problem and identified the maximizing coupling through the dual problem. Beiglböck, Henry-Labordère and Penkner (arXiv:1106.5929) showed that the dual maximizers need not exist in general.

Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 2016) approach martingale transport through the structure of the support of optimal plans. Their Theorem 7.3 recovers the Hobson–Neuberger optimizer for every continuous starting law $\mu$: it is unique and splits each starting point into at most two destinations along two monotone maps.

Timeline.

• 1965: Strassen (doi:10.1214/aoms/1177700153) shows that martingale couplings of $\mu,\nu$ exist iff $\mu$ and $\nu$ are in convex order.
• 2012: Hobson and Neuberger identify the optimizer for $c=-|y-x|$ via a construction of dual maximizers, under conditions on the marginals.
• 2013: Beiglböck, Henry-Labordère and Penkner give an example where the dual maximizers do not exist.
• 2016: Beiglböck and Juillet prove existence, uniqueness and the two-graph structure for every continuous $\mu$, using only the primal problem and a variational lemma.

Setting

A martingale transport plan between probability measures $\mu,\nu$ on $\mathbb R$ with finite first moments is a probability measure $\pi$ on $\mathbb R^2$ with first marginal $\mu$, second marginal $\nu$, and

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

that is, the conditional mean of $y$ given $x$ is $x$. Their set is $\Pi_M(\mu,\nu)$. It is nonempty exactly when $\mu$ and $\nu$ are in convex order, $\mu\preceq_C\nu$: $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi$.

For a cost $c:\mathbb R^2\to\mathbb R$ the problem is

$$C_M(\mu,\nu)=\inf\Big\{\int c\,d\pi:\ \pi\in\Pi_M(\mu,\nu)\Big\},$$

and $\pi$ is optimal if it attains this infimum. This mission concerns the Hobson–Neuberger cost $c(x,y)=-|y-x|$, so optimal plans maximize $\int|y-x|\,d\pi$. The measure $\mu$ is continuous: $\mu(\{x\})=0$ for every $x$.

For $\Gamma\subseteq\mathbb R^2$ write $\Gamma_x=\{y:(x,y)\in\Gamma\}$. A competitor of a finitely supported measure $\alpha$ on $\mathbb R^2$ is a measure $\alpha'$ with the same two marginals and the same conditional barycentres $\int y\,d\alpha_x(y)$.

Formalization targets

Goal: Theorem 7.3 (p. 43)

If $\mu\preceq_C\nu$ are probability measures and $\mu$ is continuous, there is a unique optimal $\pi_{\mathrm{HN}}\in\Pi_M(\mu,\nu)$ for $c(x,y)=-|y-x|$. Moreover there are a Borel set $S$ with $\mu(S)=1$ and functions $T_1,T_2$, nondecreasing on $S$, with

$$T_1(x)\le x\le T_2(x)\ (x\in S),\qquad \pi_{\mathrm{HN}}\big(\{(x,y):x\in S,\ y\in\{T_1(x),T_2(x)\}\}\big)=1.$$

Milestones, in attack order

1. Attainment (§2.1, pp. 10–11): for a lower semicontinuous, sufficiently integrable cost the infimum is attained when $\Pi_M(\mu,\nu)\neq\emptyset$.
2. Lemma 1.11 (p. 8): an optimal plan of finite cost is concentrated on a Borel $\Gamma$ such that no finitely supported $\alpha$ on $\Gamma$ has a cheaper competitor.
3. Lemma 7.5 (pp. 43–44): the sign of $A-B$, an explicit difference of absolute values, as a function of one variable.
4. (23) (p. 44): on such a $\Gamma$, for $(x,y^-),(x,y^+),(x',y')\in\Gamma$ with $y^-<y'<y^+$, neither $y'\le x'<x$ nor $x<x'\le y'$.
5. Lemma 3.2 (p. 19) and the countability of $\{a:|\Gamma_a|>2\}$ (p. 45).
6. Lemma 5.5 (p. 35): a Borel set with at most two points per fibre is the union of two Borel graphs.
7. Monotonicity of $T_1,T_2$ (p. 45).
8. Convexity of the set of optimizers (p. 45) and Lemma 5.6 (p. 36): a nonempty convex set of martingale plans each living on a set with two-point fibres is a single plan.

Significance

The result. Theorem 7.3 gives the extremal martingale coupling for the forward-start straddle in closed structural form: a plan that sends each $x$ to one point below and one point above it, both chosen monotonically in $x$. Combined with the martingale constraint, this determines the transition probabilities at each $x$, so the plan, and the model-independent upper price bound, are pinned down by $\mu$ and $\nu$. Remark 7.6 of the paper shows that continuity of $\mu$ cannot be dropped: for atomic $\mu$ uniqueness can fail.

Formalizing it. The result is proved in the paper; to our knowledge none of it is machine-checked. The mission produces a formal account of a support-based method (variational lemma, forbidden configurations, fibre counting, selection of Borel graphs, uniqueness from convexity). Lemma 3.2, Lemma 5.5 and Lemma 5.6 are general statements reused by the paper's other structure theorems (Corollary 1.6, Theorems 7.1, 7.4) and are of independent use.

Difficulty

The forbidden configurations (23) are pointwise statements about a set $\Gamma$ of full measure, while the conclusion is about functions. Passing from one to the other needs three ingredients that do not follow from (23) alone: a counting argument showing that only countably many fibres can have three or more points (this is where continuity of $\mu$ enters, through Lemma 3.2), a measurable selection of the two branches (Lemma 5.5, a Lusin–Novikov type theorem not in Mathlib), and a uniqueness argument comparing two optimizers through their average. The naive idea of reading uniqueness off from (23) directly fails: (23) constrains each optimizer separately, and two optimizers could a priori live on different pairs of graphs.

Lemma 1.11 itself rests on a duality theorem of Kellerer type for product sets and is the subject of a separate mission of this series.

Formalization scope

The Lean development works with measures on ℝ and ℝ × ℝ and their Borel σ-algebras. Integrals that may be infinite are taken in EReal through the published ModelRiskOT.Duality.extIntegral (positive minus negative part, with $(+\infty)-(+\infty)=-\infty$); the cost of a plan, $C_M$, and the convex order are defined through it. $\Pi_M(\mu,\nu)$ is encoded by the paper's own characterization (4) with bounded test functions, and competitors by the same device; no disintegrations appear in the statements. Cardinalities of fibres are Set.encard, valued in $\mathbb N\cup\{\infty\}$. Continuity of $\mu$ is the hypothesis $\mu(\{x\})=0$ for every $x$. "Concentrated on $A$" is $\pi(A^c)=0$.

The attainment milestone uses the finite-measure class $\mathcal M$ introduced in §2.1: probability normalization is required for Lemma 1.11 and the goal, but not for attainment. The first moments of both marginals are explicit hypotheses in that milestone.

The goal states $T_1,T_2$ as nondecreasing on a Borel set $S$ of full $\mu$-measure, with $T_1\le\mathrm{id}\le T_2$ on $S$. The page writes $T_1,T_2:\mathbb R\to\mathbb R$ nondecreasing everywhere; read literally that version fails when $\mu$ has bounded support and $\nu$ does not, and the paper's proof produces exactly the full-measure form (as in its Corollary 1.6).

Statements (23), the fibre count and the monotonicity of $T_1,T_2$ are stated for an arbitrary set $\Gamma$ with the finite-optimality property of Lemma 1.11 for $c=-|y-x|$, so they do not depend on a plan. A formalization proving only existence of an optimizer, or uniqueness without the two-graph structure, does not settle the goal: both parts are required.

Needed infrastructure: weak compactness of $\Pi_M(\mu,\nu)$ and lower semicontinuity of the cost functional; a Kellerer-type duality for Lemma 1.11; a Lusin–Novikov selection theorem for Lemma 5.5. Contributions to any of these, and alternative proofs of Lemma 5.6, 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
• D. Hobson, A. Neuberger, Robust bounds for forward start options, Mathematical Finance 22(1), 31–56, 2012. doi:10.1111/j.1467-9965.2010.00473.x
• 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. arXiv:1106.5929
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. doi:10.1214/aoms/1177700153
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995 (Theorem 18.11). doi:10.1007/978-1-4612-4190-4

Motivation

Martingale optimal transport asks for the cheapest way to couple two probability laws $\mu$ and $\nu$ on $\mathbb R$ under the extra constraint that the coupling is the law of a one-step martingale. The problem arose in robust mathematical finance: when the prices of all call options at two maturities are observed, the marginal laws of the underlying asset at those maturities are known, and the no-arbitrage bounds on the price of a path-dependent option are the values of a martingale transport problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). The paper of Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 44 (2016)) introduced the structural theory of the one-dimensional problem: a variational principle for optimal plans, a canonical coupling called the left-curtain coupling, and the identification of that coupling as the optimizer for a family of costs.

This mission formalizes that last identification. In classical optimal transport on the line, the monotone (quantile) coupling is the unique optimizer for every cost $h(y-x)$ with $h$ strictly convex; the result here is the martingale counterpart, with a different coupling and a different convexity condition.

Setting

Let $\mu,\nu$ be Borel probability measures on $\mathbb R$ with finite first moment. They are in convex order, $\mu\preceq_C\nu$, if $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (Definition 2.1). A transport plan is a measure $\pi$ on $\mathbb R\times\mathbb R$ with first marginal $\mu$ and second marginal $\nu$; it is a martingale transport plan, $\pi\in\Pi_M(\mu,\nu)$, if under $\pi$ the conditional mean of $y$ given $x$ equals $x$, equivalently

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

Strassen's theorem says $\Pi_M(\mu,\nu)\ne\emptyset$ exactly when $\mu\preceq_C\nu$.

A cost is a function $c:\mathbb R^2\to\mathbb R$. It satisfies the sufficient integrability condition if $c(x,y)\ge a(x)+b(y)$ for all $x,y$ with $a\in L^1(\mu)$, $b\in L^1(\nu)$; then $\int c\,d\pi\in(-\infty,+\infty]$ is well defined for every plan. The martingale transport problem is

$$C_M(\mu,\nu)=\inf_{\pi\in\Pi_M(\mu,\nu)}\int c\,d\pi ,$$

and a plan attaining the infimum is optimal.

A plan $\pi$ is (left-)monotone (Definition 1.4) if it is concentrated on a Borel set $\Gamma$ containing no three points $(x,y^-),(x,y^+),(x',y')$ with $x<x'$ and $y^-<y'<y^+$. For a finite measure $\eta\le\mu$, its shadow $S^\nu(\eta)$ is the least measure in the convex order among the measures $\eta'\le\nu$ with $\eta\preceq_C\eta'$ (Lemma 4.6). The left-curtain coupling $\pi_{lc}$ is the plan that transports $\mu|_{]-\infty,x]}$ onto $S^\nu(\mu|_{]-\infty,x]})$ for every $x$ (Theorem 4.18); writing $\nu^\pi_t$ for the second marginal of $\pi|_{]-\infty,t]\times\mathbb R}$, this says $\nu^{\pi_{lc}}_t=S^\nu(\mu|_{]-\infty,t]})$.

Formalization targets

Goal: Theorem 1.7 (= Theorem 6.1)

Let $\mu\preceq_C\nu$ be probability measures, let $h:\mathbb R\to\mathbb R$ be differentiable with strictly convex derivative $h'$, let $c(x,y)=h(y-x)$ satisfy the sufficient integrability condition, 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. Attainment (§2.1): for a lower semicontinuous cost with the integrability condition, the infimum $C_M(\mu,\nu)$ is attained whenever $\Pi_M(\mu,\nu)\ne\emptyset$.
2. Lemma 1.11 (variational lemma): an optimal plan of finite cost is concentrated on a Borel $\Gamma$ such that no finitely supported $\alpha$ with support in $\Gamma$ has a strictly cheaper competitor (same marginals, same conditional barycentres).
3. The rerouting (proof of Theorem 6.1): for $\lambda y^+ + (1-\lambda)y^- = y'$, the measure $\alpha'$ with masses $1-\lambda,\lambda,1$ at $(x',y^-),(x',y^+),(x,y')$ is a competitor of $\alpha$ with masses $\lambda,1-\lambda,1$ at $(x,y^+),(x,y^-),(x',y')$.
4. Display (15): $d(t)=\lambda h(y^+-t)+(1-\lambda)h(y^--t)-h(y'-t)$ is strictly decreasing.
5. The rerouting is strictly cheaper: for $x<x'$,

$$\lambda c(x,y^+)+(1-\lambda)c(x,y^-)+c(x',y')>\lambda c(x',y^+)+(1-\lambda)c(x',y^-)+c(x,y').$$

6. Every finite optimizer is monotone.
7. Theorem 4.18: $\pi_{lc}$ exists, is unique and lies in $\Pi_M(\mu,\nu)$.
8. Theorem 5.3: a monotone martingale transport plan is the left-curtain coupling of its marginals.
9. Theorem 1.9 (companion): under the goal's hypotheses, for $\pi\in\Pi_M(\mu,\nu)$, "monotone", "optimal" and "$\nu^\pi_t\preceq_C\nu^{\pi'}_t$ for all $\pi'\in\Pi_M(\mu,\nu)$ and $t$" are equivalent.

Significance

The theorem shows that, for every cost $h(y-x)$ with $h'$ strictly convex (for instance $h=\exp$), the martingale transport problem has the same optimizer, determined by $\mu$ and $\nu$ alone. In the financial reading, the model-independent bound on the price of the corresponding forward-start payoff is attained by one explicit martingale, the same for the whole family. Remark 6.2 of the paper derives from it that $\pi_{lc}$ also minimizes the essential supremum of $y-x$. Theorem 1.9 packages the result as an equivalence of a geometric property (monotonicity), an optimality property and an order property of the curtain; later work on the left-curtain coupling, its explicit construction, and its extensions to higher dimensions and to multiple marginals takes these characterizations as its starting point.

The result is proved in the paper. As far as is known, none of it is formalized: Mathlib has the convex order neither for finite measures nor in the form used here, no martingale couplings, and no theory of shadows. The mission produces the statement layer (convex order on finite measures, martingale plans, extended-real costs, shadows, left-monotone plans, competitors) and asks for a machine-checked proof of the goal and of each milestone. The real-variable milestones (displays around (15)) are self-contained and elementary; the measure-theoretic ones carry the weight.

Difficulty

Optimality is a global property of a measure on $\mathbb R^2$, while monotonicity is a pointwise property of its support. Passing from the first to the second requires the variational lemma, whose proof uses a duality theorem for measures with prescribed marginal bounds and a measurable-selection argument; a direct perturbation of $\pi$ along a single bad triple fails because a triple of points carries no mass. The second obstacle is uniqueness of the monotone plan (Theorem 5.3), which needs the shadow construction and the associativity of shadows; monotonicity alone does not visibly pin down the plan. Existence of an optimizer needs weak compactness of $\Pi_M(\mu,\nu)$, which is not immediate because the martingale condition is tested against bounded measurable, not continuous, functions.

Formalization scope

All measures are Borel measures on $\mathbb R$ and $\mathbb R\times\mathbb R$; $\mu,\nu$ in the goal are probability measures. Convex order requires finite mass and finite first moment of both sides. Integrals that may be infinite ($\int c\,d\pi$, $\int\varphi\,d\mu$ for convex $\varphi$) are computed in the extended reals as $\int f^+-\int f^-$ (the published ModelRiskOT.Duality.extIntegral), never as Bochner integrals. $\Pi_M$ is encoded by the test-function condition displayed above (the paper's (4)). Shadows and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain); their existence and uniqueness are theorems, and the goal asserts them rather than assuming them. Strict convexity of $h'$ is strict convexity of deriv h on $\mathbb R$, with $h$ differentiable everywhere. Finiteness of costs is $C_M(\mu,\nu)<+\infty$, which is the same as the existence of a martingale plan of finite cost (Theorem 6.1's wording).

A formalization that assumes an optimizer exists, or that asserts uniqueness only among left-curtain plans, is trivial and is not the goal: the statement asserts a plan with the left-curtain property, its optimality, and that every optimal plan equals it.

The development needs: weak compactness of plan sets on $\mathbb R^2$; lower semicontinuity of extended-real cost functionals; the variational lemma (shared with the companion mission on Lemma 1.11); shadows and their order properties; and the uniqueness of monotone martingale plans. The shadow theory and the variational lemma are reusable across the whole series on this paper. Contributions on any milestone are welcome, including proofs of the elementary displays (15) and the rerouting inequality.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. https://arxiv.org/abs/1208.1509v2
• 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. https://doi.org/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. https://doi.org/10.1214/13-AAP925
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. https://doi.org/10.1214/aoms/1177700153
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9