Operations Research

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

Motivation

Martingale optimal transport asks for the cheapest way to couple two given laws $\mu$ and $\nu$ of a price at two dates under the constraint that the coupling is a martingale: the conditional mean of the later price given the earlier one equals the earlier one. It is the model-independent pricing problem of mathematical finance: given the marginal laws implied by vanilla option prices, the extreme values of $E[c(X,Y)]$ over all martingale couplings bound the price of the exotic payoff $c$ (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). In the classical (non-martingale) transport problem, the shape of the cost determines the shape of the optimal coupling: for strictly convex costs of $y-x$ on the line the optimizer is a monotone map. The question this mission addresses is the martingale analogue: how much can an optimal martingale coupling split a single starting point, as a function of the cost?

Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 2016) introduced the variational lemma for this problem and used it to prove, among other results, that the left-curtain coupling is optimal for a family of costs and that, for costs $h(y-x)$, the number of points into which an optimal plan sends a non-atom of $\mu$ is bounded by a geometric property of $h'$ alone (their Theorem 7.1). This mission formalizes that bound.

Setting

All measures are Borel measures on $\mathbb R$ or $\mathbb R^2$. A martingale transport plan between probability measures $\mu,\nu$ on $\mathbb R$ is a measure $\pi$ on $\mathbb R\times\mathbb R$ with marginals $\mu$ and $\nu$ such that $\int\rho(x)(y-x)\,d\pi(x,y)=0$ for every bounded Borel $\rho$; equivalently, the disintegration $(\pi_x)$ of $\pi$ along its first coordinate satisfies $\int y\,d\pi_x(y)=x$ for $\mu$-almost every $x$. The set of such plans is $\Pi_M(\mu,\nu)$; it is nonempty exactly when $\mu$ and $\nu$ are in convex order, $\mu\preceq_C\nu$, meaning $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi$.

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 some $a\in L^1(\mu)$, $b\in L^1(\nu)$; then $E_\pi[c]=\int c\,d\pi\in(-\infty,+\infty]$ is well defined for every plan. A plan $\pi\in\Pi_M(\mu,\nu)$ is optimal if $E_\pi[c]\le E_{\pi'}[c]$ for every $\pi'\in\Pi_M(\mu,\nu)$.

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)$. For a set $\Gamma\subseteq\mathbb R^2$, $\Gamma_x=\{y:(x,y)\in\Gamma\}$ is its fibre over $x$.

This mission concerns costs of the form $c(x,y)=h(y-x)$ with $h:\mathbb R\to\mathbb R$ twice continuously differentiable, and the hypothesis that affine functions meet $h'$ in at most $k$ points: for all $s,t\in\mathbb R$, $|\{x:h'(x)=sx+t\}|\le k$. For instance $h(t)=t^4$ satisfies it with $k=3$.

Formalization targets

Goal: Theorem 7.1 (p. 38)

Under the hypotheses above, with $\pi$ an optimal martingale plan of finite cost, there is a disintegration $(\pi_x)_{x\in\mathbb R}$ of $\pi$ such that for every $x\in\mathbb R$

$$\mu(\{x\})>0\qquad\text{or}\qquad\operatorname{card}(\operatorname{spt}\pi_x)\le k,$$

and if $\mu$ has no atoms, $\operatorname{card}(\operatorname{spt}\pi_x)\le k$ holds $\mu$-almost surely for every disintegration of $\pi$.

Milestones

1. Lemma 1.11 (variational lemma, p. 8): an optimal plan of finite cost is concentrated on a Borel set $\Gamma$ such that no finitely supported $\alpha$ with $\operatorname{spt}\alpha\subseteq\Gamma$ has a strictly cheaper competitor.
2. Lemma 3.2 (p. 19): if uncountably many fibres $\Gamma_a$ have at least $k$ points, some $(a,b_1<\dots<b_k)$ is a limit of such configurations from the right and from the left.
3. An interior point off the chord (proof of Theorem 7.1, p. 39): for $b_0<\dots<b_k$, some interior $b_i$ has $h'(b_i-a)$ off the chord of $h'(\cdot-a)$ through $b_0,b_k$.
4. The local sign (p. 39): near such $(a,b_i)$, the cost difference (17) − (18) of a three-point rerouting is nonzero with sign fixed by $a-a'$.
5. Countably many exceptional points (pp. 38–39): on such a $\Gamma$, only countably many continuity points $x$ of $\mu$ have $|\Gamma_x|\ge k+1$.

Significance

The result itself. Theorem 7.1 converts a one-dimensional condition on $h'$ into a sparsity statement for every optimal martingale coupling: non-atoms of $\mu$ are sent to at most $k$ points. For $h(t)=t^4$ this gives at most three points, and Section 7.3 of the paper gives an example with continuous $\mu$ where the optimizer splits into more than two points, so for this cost the bound cannot be lowered to two. For costs where $h'$ is strictly convex (so $k=2$), it gives the two-point structure also enjoyed by the left-curtain coupling, which is optimal for those costs (Theorem 1.9). Such support bounds are what make the optimizers computable and the corresponding robust price bounds explicit.

Formalizing it. The theorem is proved in the paper; to our knowledge none of it is formalized. A formal proof requires machine-checked versions of the variational lemma (itself resting on a duality theorem of Kellerer type), the countability argument of Lemma 3.2, and the real-analysis estimate behind the three-point rerouting. Each of these is reusable: Lemma 1.11 drives every structural result of the paper, and Lemma 3.2 is used again for the left-monotonicity theorems.

Difficulty

The natural first attempt is to argue pointwise: if a fibre $\Gamma_a$ has $k+1$ points, reroute mass within that fibre to lower the cost. This fails, because a competitor must preserve the barycentre of each fibre, and within a single fibre no rerouting both preserves the barycentre and the marginals. Any improvement must move mass between two different starting points $a$ and $a'$, and this requires the two fibres to be close to each other and arranged consistently, which a single fibre cannot guarantee. Producing such pairs of fibres needs uncountably many exceptional points (Lemma 3.2) and the set $\Gamma$ of the variational lemma, whose existence is the deep part (it rests on a duality theorem for measures with given marginals). A second difficulty is that the conclusion is required at every non-atom $x$, not only almost everywhere, so the exceptional set must be controlled exactly.

Formalization scope

Lean represents measures with Mathlib's Measure ℝ and Measure (ℝ × ℝ). $\Pi_M$ is encoded through the test-function characterization $\int\rho(x)(y-x)\,d\pi=0$ for bounded Borel $\rho$; costs are extended-real integrals $\int c^+-\int c^-\in[-\infty,+\infty]$ (the published ModelRiskOT.Duality.extIntegral); competitors of a finitely supported $\alpha=\sum_{s\in S}w_s\delta_s$ are encoded through the same test-function device. A disintegration is a Markov kernel $\kappa$ with $\pi=\mu\otimes\kappa$, and $\operatorname{card}(\operatorname{spt}\pi_x)\le k$ is written as "$\kappa(x)$ is concentrated on a set of at most $k$ points", which is equivalent for probability measures on $\mathbb R$. Cardinalities take values in $\mathbb N\cup\{\infty\}$; $h'$ is deriv h.

Standing and added hypotheses of the goal: $\mu,\nu$ are probability measures in convex order; "optimal transport plan" means optimal martingale plan, as throughout Section 7; and, because the proof starts from Lemma 1.11, the hypotheses of that lemma are added: the sufficient integrability condition for $c$ and finite cost of $\pi$. "Continuous $\mu$" is $\mu(\{x\})=0$ for every $x$.

The conclusion is not trivialized: the first part holds for every $x$ with a single chosen kernel, not almost everywhere, and the second part quantifies over all kernels, not one. The hypotheses are jointly satisfiable (for example $h(t)=t^4$, $k=3$, $\mu=\nu=\delta_0$).

A complete development needs disintegration of measures on $\mathbb R^2$ (available in Mathlib as condKernel), the variational lemma with its duality ingredient, and elementary real analysis. Contributions to the variational lemma are reusable across the whole series of missions on this paper.

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
• 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
• M. Beiglböck, M. Goldstern, G. Maresch, W. Schachermayer, Optimal and better transport plans, J. Funct. Anal. 256(6), 1907–1927, 2009. doi:10.1016/j.jfa.2009.01.013

Motivation

Online retailers, search engines and streaming services show products on a sequence of pages, and most consumers look at only the first few. Which products are seen therefore depends on where they are placed. Gallego, Li, Truong and Wang (Operations Research, 2020) call the problem of placing products on pages to maximize expected revenue product framing. They show that it is NP-hard even with two pages and the multinomial logit model, and they give simple algorithms with constant-factor guarantees.

This mission concerns their second guarantee. In their basic model every consumer chooses with the same choice model, whatever the number of pages she views. In practice the number of pages viewed is itself informative: consumers who browse many pages may be keener buyers. Section 6 of the paper lets the choice model depend on the number of pages viewed and proposes the TRUNC algorithm for this setting. The guarantee is that TRUNC earns at least one third of the optimal expected revenue.

Setting

There are $n$ products with revenues $r_i\ge 0$ and $m$ virtual pages, each holding at most $p$ products; write $[k]=\{1,\dots,k\}$. A framing places each product on at most one page, with at most $p$ products per page. A consumer views a random number $X\in[m]$ of pages, with law $\lambda(x)=\mathbb P[X=x]$, tail $\Lambda(x)=\mathbb P[X\ge x]$ and failure rate $h(x)=\lambda(x)/\Lambda(x)$. Her consideration set is the set of products on pages $1,\dots,X$.

A consumer who views $x$ pages is of type $x$ and buys product $i$ from consideration set $S$ with probability $P_x(i,S)$, where $P_x(i,S)\ge 0$, $P_x(i,S)=0$ for $i\notin S$, and $\sum_{i\in S}P_x(i,S)\le 1$. The revenue of $S$ for type $x$ and the best capacitated revenue are

$$R_x(S)=\sum_{i\in S}r_iP_x(i,S),\qquad U(x)=\max_{S\subseteq[n],\ |S|\le xp}R_x(S).$$

A framing $f$ earns $\sum_{x\in[m]}\lambda(x)R_x(C_f(x))$, where $C_f(x)$ is the set of products on pages $1,\dots,x$. Its maximum over all framings is $V^{OPT}$. The assumptions are:

• B1: $R_x(S)\le R_y(S)$ whenever $x\le y$ and $|S|\le xp$;
• B2: $U(x)/x$ is nonincreasing in $x$;
• B3: problem (9) defining $U$ can be solved, here exactly;
• B4: $X$ has an increasing failure rate (IFR), i.e. $h$ is nondecreasing (Shaked and Shanthikumar 2007).

TRUNC($y$), for $y\in[m]$, picks an optimal assortment $S(y)$ for $U(y)$ and places it, in any arrangement, on pages $1,\dots,y$, leaving the remaining pages blank. TRUNC takes the best of these $m$ framings; its revenue is $V^{TRUNC}$.

The analysis passes through the bound-revealing program (10): minimize $\max_{x\in[m]}U(x)\Lambda(x)$ over nondecreasing $U\ge 0$ with $U(x)/x$ nonincreasing and over tails $1=\Lambda(1)\ge\cdots\ge\Lambda(m)\ge 0$ with $\Lambda(x+1)\Lambda(x-1)\le\Lambda(x)^2$, subject to $\sum_x\lambda(x)U(x)=1$.

Formalization targets

Goal: Theorem 4

Under Assumptions B1–B4, for every choice of optimal assortments and every arrangement on the pages,

$$V^{TRUNC}\;\ge\;\frac13\,V^{OPT}.$$

Milestones

In the order the proof uses them:

1. Upper bound (§6, p. 13): $V^{OPT}\le\mathbf E[U(X)]=\sum_x\lambda(x)U(x)$.
2. Lower bound (§6.1, p. 14): every run of TRUNC($y$) earns at least $U(y)\Lambda(y)$.
3. Lemma 8: for an IFR tail with $\Lambda>0$, $g(x)=x\Lambda(x)$ is weakly unimodal, and its largest maximizer is $\min\{x: h(x)>1/(x+1)\}$.
4. Proposition 5, Lemma 9, Proposition 6, Proposition 7: the structure of every optimal solution of (10) with $\Lambda>0$. With $y$ the largest maximizer of $U(x)\Lambda(x)$:
   • $U(x)/x$ is constant for $x\ge y$;
   • $y$ also maximizes $x\Lambda(x)$;
   • $U(x)\Lambda(x)$ is constant for $x\le y$;
   • $h$ is constant on $[y,m-1]$.
5. Value of (10) (A.4, p. 42): every feasible point of (10) has $\max_xU(x)\Lambda(x)\ge 1/3$.

Significance

The theorem shows that framing under type-dependent choice admits a constant-factor approximation using only $m$ calls to an assortment oracle, although the framing problem itself is NP-hard. The constant does not depend on the number of products, pages or page capacity. The bound-revealing program (10) is a self-contained extremal problem about log-concave tails and is reusable wherever a revenue curve with decreasing average returns meets an IFR horizon. The numerical value of (10) decreases with $m$ ($2/3$ at $m=2$, about $0.36$ at $m=40$), so the constant $1/3$ is approached only as the number of pages grows.

The result is proved in the paper. No part of it has a machine-checked proof: the platform has no item on product framing, discrete failure rates or program (10). A complete development would give a machine-checked proof of the approximation ratio. It would also give a checked treatment of the perturbation arguments of Appendix A.4, which the paper presents briefly.

Difficulty

Two steps are elementary: the upper bound (a consumer of type $x$ never sees more than $xp$ products) and the lower bound (every consumer of type $x\ge y$ sees all of $S(y)$).

The difficulty lies in the extremal problem (10). It is not convex: the IFR constraint is a log-concavity condition, and the objective is a maximum of products $U(x)\Lambda(x)$. A direct bound such as $\max_xU(x)\Lambda(x)\ge\sum_x\lambda(x)U(x)/m$ gives a constant that decays with $m$. The uniform constant comes from showing that the extremal tail is geometric beyond the maximizing page and that the extremal $U$ is pinned down on both sides of it. The paper reaches this structure through optimality conditions, so a formal proof must also establish that (10) attains its minimum, or must avoid that step.

Formalization scope

Products are Fin n. Pages are the natural numbers $1,\dots,m$, as in the paper, with $m\ge 1$ and $p\ge 1$. A framing is f : Fin n → ℕ: product $i$ is on page f i when $1\le f(i)\le m$, and f i = 0 means it is not displayed. The law $\lambda$ and the functions of (10) are functions on $\mathbb N$ of which only the values on $[m]$ are used, and $\Lambda(m+1)=0$.

$V^{OPT}$ and $U$ are maxima over finite nonempty families, and $V^{TRUNC}$ is a Finset.sup' over $y\in[m]$. TRUNC is a predicate on its outputs, not a function, and the goal is quantified over every family of runs. Assumption B3 is used with $\epsilon=0$, as everywhere in the paper. IFR is required only where the failure rate is defined ($\Lambda>0$), so laws whose support ends before page $m$ are allowed. Nonnegative revenues $r_i\ge 0$ are assumed; the lower bound of milestone 2 needs them.

No trivializing reading. The goal is not stated for one particular filling heuristic, or for some run only, and $V^{TRUNC}$ is the revenue of the framings themselves, not the lower bound $U(y)\Lambda(y)$.

Page numbers refer to the authors' accepted manuscript of the Operations Research article, which differ from the journal typesetting. The development needs only Mathlib (finite sums and maxima over Finset). Program (10) and Lemma 8 are independent of the framing model. Contributions are welcome at every milestone: Lemma 8 and the bound for (10) are the most self-contained.

Selected references

• G. Gallego, A. Li, V.-A. Truong, X. Wang, Approximation Algorithms for Product Framing and Pricing, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1875
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

A chance-constrained program chooses a decision $x$ so that a random vector $\xi$ falls outside a decision-dependent safety set $\mathcal S(x)$ with probability at most $\epsilon$. Chance constraints are a standard model for reliability requirements in power systems, supply chains and transportation, where a plan must survive random demand or supply with high probability. In practice the distribution of $\xi$ is known only through samples $\xi_1, \dots, \xi_N$, and the sample average approximation (SAA) that replaces it by the empirical distribution $\mathbb P_N$ is sensitive to the particular sample.

Distributionally robust chance constraints regularize SAA by requiring the probability bound for every distribution within Wasserstein distance $\theta$ of $\mathbb P_N$. Chen, Kuhn and Wiesemann (arXiv:1809.00210) and Xie (doi:10.1007/s10107-019-01445-5) showed that, for safety sets defined by linear inequalities, the resulting program (DR-CCP) is a mixed-integer linear program with a big-M constant. These big-M formulations are hard for solvers to close when $\theta$ is small. Ho-Nguyen, Kılınç-Karzan, Küçükyavuz and Lee (doi:10.1007/s10107-020-01605-y) connect the formulation to the mixing sets of SAA and to robust 0–1 programming, and derive a smaller and tighter formulation that is still exact.

Setting

The random vector lives in $\mathbb R^K$ with an arbitrary norm $\|\cdot\|$; in the formalization it is a finite-dimensional real normed space $E$. The dual norm of a linear functional $b$ is $\|b\|_* = \sup_{\|\xi\| \le 1} b^\top \xi$. The decision $x$ ranges over a set $\mathcal X \subseteq \mathbb R^L$.

The 1-Wasserstein distance between distributions $\mathbb P, \mathbb P'$ is the infimum of $\mathbb E\|\xi - \xi'\|$ over couplings of $\mathbb P$ and $\mathbb P'$. The ambiguity set $\mathcal F_N(\theta)$ is the set of distributions within distance $\theta$ of $\mathbb P_N = \frac1N \sum_{i} \delta_{\xi_i}$. The feasible region of (DR-CCP) is

$$\mathcal X_{\mathrm{DR}}(\mathcal S) = \Big\{x \in \mathcal X : \sup_{\mathbb P \in \mathcal F_N(\theta)} \mathbb P[\xi \notin \mathcal S(x)] \le \epsilon\Big\}.$$

Throughout, $\epsilon \in (0,1)$ and $\theta > 0$ are fixed.

The paper studies joint chance constraints with right-hand side uncertainty: for $p \in [P]$ there are $a_p \in \mathbb R^L$, $b_p$ and $d_p \in \mathbb R$, and

$$\mathcal S(x) = \{\xi : b_p^\top \xi + d_p - a_p^\top x > 0,\ p \in [P]\}.$$

Write $g_{i,p}(x) = (b_p^\top\xi_i + d_p - a_p^\top x)/\|b_p\|_*$ and $k = \lfloor \epsilon N \rfloor$. Let $q_p$ be the $(k+1)$-th largest value among $\{-b_p^\top\xi_i\}_{i\in[N]}$, and let $[N]_p = \{i : -b_p^\top \xi_i > q_p\}$.

The big-M formulation (5) of Chen et al. uses binaries $z \in \{0,1\}^N$, slacks $r \ge 0$ and a scalar $t \ge 0$ with

$$\epsilon t \ge \theta + \tfrac1N \textstyle\sum_i r_i,\qquad M(1 - z_i) \ge t - r_i,\qquad g_{i,p}(x) + M z_i \ge t - r_i.$$

The paper's improved formulation (20) keeps the first two families, adds the knapsack constraint $\sum_i z_i \le k$, replaces $M$ in the third family by $h_{i,p} = (-b_p^\top\xi_i - q_p)/\|b_p\|_*$, imposes it only for $i \in [N]_p$, and adds $(-q_p + d_p - a_p^\top x)/\|b_p\|_* \ge t$ for every $p$.

Formalization targets

Goal: Theorem 3 (p. 655)

$$\mathcal X_{\mathrm{DR}}(\mathcal S) = \{x \in \mathcal X : \exists\,(z, r, t) \text{ satisfying (20b)–(20d)}\}.$$

The goal states equality of feasible sets of $x$. Because the objective $c^\top x$ depends on $x$ alone, this is the paper's "exact reformulation".

Milestones, in attack order

1. (4b), p. 646: $\operatorname{dist}(\xi, \mathcal S(x)) = \max\{0, \min_p (b_p^\top\xi + d_p - a_p^\top x)/\|b_p\|_*\}$, where $\operatorname{dist}(\xi, \mathcal S) = \inf\{\|\xi - \xi'\| : \xi' \notin \mathcal S\}$ is (1).
2. (3), p. 645: for open $\mathcal S(x)$, $\mathcal X_{\mathrm{DR}}(\mathcal S)$ is the set of $x \in \mathcal X$ admitting $t \ge 0$, $r \ge 0$ with $\operatorname{dist}(\xi_i, \mathcal S(x)) \ge t - r_i$ and $\epsilon t \ge \theta + \frac1N\sum_i r_i$.
3. (6), p. 646: $\mathcal X_{\mathrm{DR}}(\mathcal S) = \{x \in \mathcal X : \text{(5b)–(5e)}\}$.
4. Theorem 1, p. 648: adding $\sum_i z_i \le k$ and $g_{i,p}(x) + M z_i \ge 0$ to (5) keeps it exact.
5. Theorem 2, p. 651: replacing $M$ in (5e) by $h_{i,p}$, with the knapsack constraint, keeps it exact.
6. Lemma 1, p. 653: for $x \in \mathcal X_{\mathrm{DR}}(\mathcal S)$, $t$ may be taken equal to the $(k+1)$-th smallest of the distances $\operatorname{dist}(\xi_i, \mathcal S(x))$.
7. Proposition 1, p. 654: for $x \in \mathcal X_{\mathrm{DR}}(\mathcal S)$, some solution of (17) also satisfies $(-q_p + d_p - a_p^\top x)/\|b_p\|_* - t \ge 0$ for every $p$.

Milestones 2 and 3 are results of Chen, Kuhn and Wiesemann that this paper cites and uses, not results it proves.

Significance

Theorem 3 says that the scenario-wise big-M rows of the Wasserstein chance constraint can be replaced by at most $\lfloor\epsilon N\rfloor$ rows per $p$, with coefficients computed from the data. Remark 2 of the paper counts at least $((1-\epsilon)N - 1)P$ fewer rows than (17). The reduced form exposes a robust 0–1 substructure, and the paper adapts Atamtürk's valid inequalities for it. Its computational study reports order-of-magnitude speed-ups on stochastic transportation problems.

The results are proved on paper; none is machine-checked. The formalization would give a verified chain from the Wasserstein worst-case probability to a finite mixed-integer system. Milestone (3), the dual reformulation, is reusable for any distributionally robust chance constraint over a 1-Wasserstein ball around an empirical distribution, and (4b) for any polyhedral safety set. A second formalization layer would verify the order-statistic arguments (Lemma 1, Proposition 1) used throughout the quantile-strengthening literature.

Difficulty

The deterministic parts — Theorems 1–3 given (3) and (4b) — are finite case analyses on $z_i \in \{0,1\}$, but each step relies on order statistics of the sample with ties. Lemma 1 rests on the paper's "without loss of generality, sort the distances", and a formal proof must handle ties and the floor $\lfloor\epsilon N\rfloor$ exactly. The paper's proof of Theorem 2 argues "at optimality"; for a statement about feasible sets that argument has to be replaced by an explicit choice of $z$.

The hard step is (3). It exchanges a supremum over all Borel probability measures in a Wasserstein ball for a scalar system. The naive attempt, which perturbs $\mathbb P_N$ by moving mass from the samples to the nearest unsafe points, proves only one inclusion. The other needs strong duality for worst-case probabilities over transport balls, together with attainment of the dual infimum, which uses $\theta > 0$.

Formalization scope

• The ξ-space is a type E with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] and its Borel σ-algebra. The norm is arbitrary, not the sup norm of Fin K → ℝ.
• Each $b_p$ is a continuous linear functional (StrongDual ℝ E), so $\|b_p\|_*$ is its operator norm.
• Decisions are Fin L → ℝ, with $a_p^\top x$ written a p ⬝ᵥ x. Indices are 0-based.
• The worst-case probability is the published ModelRiskOT.WorstProb.worstProb with cost $\|u - v\|$, valued in $[0,\infty]$, around the published WassersteinDRO.Duality.empiricalDistribution.
• The distance (1) is Metric.infDist.
• Binaries are reals with $z_i \in \{0,1\}$.
• Order statistics sort the multiset of values, so ties count with multiplicity.

Standing assumptions and pins in every statement:

• $N \ge 1$, $\epsilon \in (0,1)$ and $\theta > 0$ (p. 645);
• $P \ge 1$ and $b_p \neq 0$, which (4) needs;
• for every statement involving $M$, one bound $|b_p^\top\xi_i + d_p - a_p^\top x|/\|b_p\|_* \le M$ over $x \in \mathcal X$ and all $i, p$. This is Remark 1's (10), taken uniform in $i$. It replaces the compactness of $\mathcal X$ assumed on p. 642, which is not assumed;
• for the general-$\mathcal S$ milestone (3), $\mathcal S(x)$ open with nonempty complement.

In (17b), the printed "(5b)–(5d) and (5c)" is read as "(5b)–(5d) and (8c)", following the proof of Theorem 2 and (20b).

Several trivializing formalizations are ruled out:

• an empty or degenerate ball: $N \ge 1$ makes $\mathbb P_N$ a probability measure inside its own ball;
• a junk distance: the unsafe set is nonempty under the pins, so infDist never sees the empty set;
• a junk order statistic: the rank $k$ is below $N$;
• a fixed norm;
• a relaxation of $z$ to $[0,1]$, which is a different theorem.

Welcome contributions:

• the 1-Wasserstein duality for indicator losses on empirical distributions;
• order-statistic lemmas for the multiset sort;
• the distance from a point to the complement of an open polyhedron in a normed space.

Selected references

• N. Ho-Nguyen, F. Kılınç-Karzan, S. Küçükyavuz, D. Lee, Distributionally robust chance-constrained programs with right-hand side uncertainty under Wasserstein ambiguity, Mathematical Programming Ser. B 196 (2022) 641–672. https://doi.org/10.1007/s10107-020-01605-y
• Z. Chen, D. Kuhn, W. Wiesemann, Data-driven chance constrained programs over Wasserstein balls, Operations Research (2024); preprint 2018. https://arxiv.org/abs/1809.00210
• W. Xie, On distributionally robust chance constrained programs with Wasserstein distance, Mathematical Programming 186 (2021) 115–155. https://doi.org/10.1007/s10107-019-01445-5
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44 (2019) 565–600. https://doi.org/10.1287/moor.2018.0936
• A. Atamtürk, Strong formulations of robust mixed 0–1 programming, Mathematical Programming 108 (2006) 235–250. https://doi.org/10.1007/s10107-006-0709-5

Why radius sensitivity matters

A distributionally robust decision evaluates a rule against every data distribution within a specified transport budget of a baseline law. The budget is a modeling choice: increasing it expresses more uncertainty about the data. A robust objective value can increase with that budget, but the value alone does not describe how the adverse distribution changes. For a fixed linear decision, Blanchet, Murthy, and Zhang identify the worst-case distribution and ask what happens to each observation as the budget increases. Their Theorem 7 gives a sample-wise answer in a small-radius regime: adverse observations move along straight lines, and their distance from the original observations grows monotonically.

This matters when a robust solution is interpreted through its adverse scenarios. The result says that two nearby ambiguity budgets do not produce unrelated worst-case data sets. They produce a coherent family of transported observations whose directions are determined by the sign of the loss derivative. The theorem is a structural property of an optimal-transport ambiguity set, beyond a bound on its optimal value. It appears in a paper that also develops dual formulas and iterative optimization schemes for the same model Blanchet, Murthy, and Zhang, 2022.

Model and notation

Let $X$ take values in $\mathbb R^d$ with baseline law $P_0$. A decision $\beta$ belongs to a convex set $B\subseteq\mathbb R^d$ and incurs loss $\ell(\beta^\top X)$. At each source point $x$, a positive-definite matrix $A(x)$ defines the transport cost

$$c(x,x')=(x-x')^\top A(x)(x-x').$$

The matrix may depend on $x$, so movement can be cheaper in different directions and at different observations. The model requires lower semicontinuity of $c$ and almost-sure lower and upper spectral bounds for $A(x)$. A distribution $P$ is within the ambiguity ball of radius $\delta>0$ when it can be coupled with $P_0$ at expected cost at most $\delta$. The worst-case objective is the supremum of $E_P[\ell(\beta^\top X)]$ over that ball. In Lean, the equivalent coupling formulation records a joint law $\pi$ with first marginal $P_0$, second marginal $P$, and cost at most $\delta$.

The paper reduces the worst-case calculation to a dual objective $f_\delta(\beta,\lambda)$, where $\lambda\ge0$ prices the transport budget. Its pointwise term $\ell_{\rm rob}(\beta,\lambda;x)$ is the supremum over a scalar $\gamma$ of the function $F(\gamma,\beta,\lambda;x)$ in display (7). The set of maximizing scalars is $\Gamma^*(\beta,\lambda;x)$. A scalar maximizer $G_\delta(x)$ produces a transported observation

$$X^*_\delta=x+\sqrt\delta\,G_\delta(x)A(x)^{-1}\beta.$$

Assumptions 2–4 require a convex loss with controlled growth, a fourth moment of $P_0$, bounded second derivatives of the loss, a nondegenerate loss derivative, and compactness of $B$. The statement here also uses Assumption 5, local strong convexity with a positive-probability nondegeneracy condition. The paper’s proof of Theorem 7 uses that condition through its small-radius strong-convexity result Theorems 4 and 7.

Formalization targets

For each fixed $\beta\in B\setminus\{0\}$, the goal asserts that there is a common threshold $\delta_1>0$ and a family $G_\delta$ such that the law of $X^*_\delta$ is the unique worst-case distribution for every $0<\delta<\delta_1$. For any pair $0<\delta<\delta'<\delta_1$, it asserts, $P_0$-almost surely,

$$\begin{aligned} 0&<\sqrt\delta\,G_\delta<\sqrt{\delta'}\,G_{\delta'} &&\text{if }\ell'(\beta^\top X)>0,\\ \sqrt{\delta'}\,G_{\delta'}&<\sqrt\delta\,G_\delta<0 &&\text{if }\ell'(\beta^\top X)<0,\\ G_\delta&=0 &&\text{if }\ell'(\beta^\top X)=0. \end{aligned}$$

Consequently,

$$\|X^*_\delta-X\|\le\|X^*_{\delta'}-X\|.$$

The goal keeps the uniqueness and primal attainment clauses together with these comparisons. The milestones follow the paper’s prerequisites: the optimizer and curvature bounds of Proposition 9, the unique worst-case law of Theorem 6(e), uniqueness of the dual minimizer at small radius, and the sign of the pointwise maximizer. Each has its own statement so solvers can use it elsewhere.

What the result establishes

The theorem gives a consistent interpretation of changes in the ambiguity radius. If the loss increases locally in the decision direction, an adverse observation moves farther in that direction; if the loss decreases, it moves farther in the opposite direction; at a stationary score it stays put. The corresponding displacement norm is monotone for each radius pair, almost surely. This is stronger than monotonicity of the worst-case objective value: it describes the geometry of a family of optimizers, not only their values.

The paper proves the result in §5.4. The work of this mission is to formalize its hypotheses, optimality claims, and sample-wise inequalities in Lean. The published ModelRiskOT.Duality coupling definitions already give a reusable primal interface; this mission adds the state-dependent quadratic cost, the scalar dual model, its small-radius regions, and the comparative-statics statements. The proof obligations remain open in this draft. Their formalization would also make the dual optimizer bounds and the deterministic transport representation reusable in later optimal-transport DRO developments.

Where the mathematical difficulty sits

The worst-case value being monotone in $\delta$ does not force a particular worst-case distribution, or each observation in one, to move monotonically. The theorem needs a unique worst-case law and a coherent choice of pointwise maximizers as $\delta$ varies. The scalar maximizer depends on both the radius and the dual price, while the optimal dual price itself changes with the radius. The paper’s small-radius conditions keep this joint variation controlled. Without uniqueness, two optimal laws could differ even at the same radius, and a sample-wise comparison would have no fixed object to compare.

The result also involves several layers of almost-sure reasoning. Spectral bounds on $A(x)$ hold only outside a null set; the relevant maximizer and its transported law must be measurable enough to define pushforwards and expectations. These conditions must be carried through the theorem without silently replacing an almost-sure claim by a pointwise one.

Formalization scope

Vectors use EuclideanSpace ℝ (Fin d), and the baseline is a Borel probability measure. The decision set is convex and compact and is explicitly nonempty. Assumption 1 gives positive definiteness of $A(x)$ everywhere, lower semicontinuity of the cost, and almost-sure uniform spectral bounds. The loss satisfies Assumptions 2–5. The fourth moment in Assumption 2 and the bounds on $\ell''$ control the integrals used by the dual theory. A positive ambiguity radius is required whenever its square root appears.

The dual terms $\ell_{\rm rob}$ and $f_\delta$ use extended-real values, since the pointwise supremum can be infinite. The worst-case value is a supremum over feasible couplings, with signed loss integrated using the published extended-real integral. A graph coupling witnesses attainment, and every optimal coupling must have the same second marginal. This ties the family $G_\delta$ to the actual worst-case distribution rather than an arbitrary monotone scalar field. Almost-everywhere measurability of $G_\delta$ and the transport map is part of the conclusion.

The radius $\delta$ varies inside the goal. The threshold $\delta_1$ is chosen before any radius pair, and the comparisons are stated almost surely for each pair. The paper prints Theorem 7 under Assumptions 1–4 while referring to $\delta_1$ and invoking Theorem 4, which uses Assumption 5; this mission includes Assumption 5 explicitly. It also reads the singleton clause of Theorem 6(e) almost surely, because its threshold is an essential supremum, and uses a non-strict lower curvature bound in Proposition 9(b), as its proof permits. Contributions on the small-radius dual theory, measurable maximizers, primal attainment, and the radius comparisons are all within scope.

Selected references

• J. Blanchet, K. Murthy, and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3.
• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.