Probability

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

Mean field games (MFGs) describe Nash equilibria of stochastic differential games with a very large number of symmetric players, each of whom interacts with the others only through the empirical distribution of their states (and, in this paper, of their controls). They were introduced independently by Lasry and Lions and by Huang, Malhamé and Caines around 2006, and are used for models of systemic risk, price impact in optimal execution, flocking and crowd motion, and large-population economics. The basic mathematical question is existence of an equilibrium: a flow of measures that is reproduced by the optimal behaviour of a representative player who takes that flow as given.

Two families of methods dominate the literature. The analytic approach of Lasry and Lions solves a coupled Hamilton–Jacobi–Bellman / Fokker–Planck system. The probabilistic approach of Carmona and Delarue (arXiv:1210.5780) solves a forward–backward SDE of McKean–Vlasov type in the strong formulation, on a fixed probability space with the controlled state as a strong solution. Both require the coefficients to be regular (Lipschitz or continuous) in the state variable. Carmona and Lacker (arXiv:1307.1152, Ann. Appl. Probab. 2015) introduce a weak formulation, in which controls act through a Girsanov change of measure on a fixed driftless state process. This lets the drift, running reward and terminal reward be merely measurable and path-dependent in the state. The interaction can enter through the law of the state path and through the law of the control. This mission formalizes their existence theorem.

Setting

Fix a dimension $d$, a horizon $T>0$ and the path space $\mathcal C=C([0,T];\mathbb R^d)$ with the sup norm. A measurable $\psi:\mathcal C\to[1,\infty)$ fixes the admissible population laws, $\mathcal P_\psi(\mathcal C)=\{\mu:\int\psi\,d\mu<\infty\}$. The topology $\tau_\psi(\mathcal C)$ is the weakest one making $\mu\mapsto\int f\,d\mu$ continuous for every measurable $f$ with $|f|\le c\,\psi$. A compact convex control set $A$ sits in a normed space, and $\mathcal P(A)$ carries the weak topology.

A probability space carries an initial state $\xi$ and an independent Brownian motion $W$, with filtration $\mathbb F$ generated by $(\xi,W)$. Admissible controls $\mathbb A$ are the progressively measurable $A$-valued processes. The driftless state $X$ solves $dX_t=\sigma(t,X)\,dW_t$, $X_0=\xi$, and its law is $\mathcal X=P\circ X^{-1}$. For a population law $\mu$ and a control $\alpha$, the measure $P^{\mu,\alpha}$ has density $\mathcal E\big(\int_0^\cdot\sigma^{-1}b(t,X,\mu,\alpha_t)\,dW_t\big)_T$ with respect to $P$. Under $P^{\mu,\alpha}$, $X$ is a weak solution of $dX_t=b(t,X,\mu,\alpha_t)\,dt+\sigma(t,X)\,dW^{\mu,\alpha}_t$. Given also a measurable flow $q:[0,T]\to\mathcal P(A)$ of control laws, the reward is

$$J^{\mu,q}(\alpha)=\mathbb E^{\mu,\alpha}\Big[\int_0^Tf(t,X,\mu,q_t,\alpha_t)\,dt+g(X,\mu)\Big],\qquad V^{\mu,q}=\sup_{\alpha\in\mathbb A}J^{\mu,q}(\alpha).$$

The standing assumptions (S) ask for:

• measurability of the coefficients;
• continuity in the control;
• a unique strong solution $X$ with $\mathbb E[\psi^2(X)]<\infty$;
• $\sigma(t,X)$ nonsingular, with $\sigma^{-1}b$ bounded;
• growth of $f$ and $g$ controlled by $\psi$;
• a separated running reward $f=f_1(t,x,\mu,a)+f_2(t,x,\mu,q)$.

The Hamiltonian is $h=f+z\cdot\sigma^{-1}b$. Its maximum over $A$ is $H$, and the set of maximizers is $A(t,x,\mu,z)$.

Formalization targets

Goal: Theorem 3.5

Assume (S), (E) (for each $(t,x)$, the maps $b$, $f$, $g$ are sequentially continuous in the measure and control arguments, on the laws $\mu\sim\mathcal X$ with $\tau_\psi$) and (C) (each $A(t,x,\mu,z)$ is convex). Then there exist $\mu\in\mathcal P_\psi(\mathcal C)$, a measurable $q:[0,T]\to\mathcal P(A)$ and $\alpha\in\mathbb A$ with

$$V^{\mu,q}=J^{\mu,q}(\alpha),\qquad P^{\mu,\alpha}\circ X^{-1}=\mu,\qquad P^{\mu,\alpha}\circ\alpha_t^{-1}=q_t\ \text{ for a.e. } t.$$

This is Definition 3.4 of a solution of the MFG. No constants or rates appear; the goal asserts existence only.

Milestones

The milestones are the statements the paper's proof (§7) names, in attack order:

• the BSDE characterization of optimal controls, (7.1)–(7.4) and Remark 7.2;
• Lemma 7.6 (densities of image measures);
• Lemma 7.7 (uniform moment bounds on Girsanov densities);
• Proposition 7.8 (compactness and metrizability of the set $\mathcal Q$ of candidate laws);
• Berge's maximum theorem (Theorem 7.5);
• Lemma 7.9 (continuity of the Hamiltonian on $\mathcal Q$);
• Lemma 7.10 (stability of the BSDE adjoint process);
• Lemma 7.11 (upper hemicontinuity of the optimal-control correspondence);
• the set-valued fixed point theorem, Proposition 7.4.

Significance

The theorem yields equilibria for interactions that are discontinuous in the state and nonlocal in time. Examples are rank-based rewards, path-dependent payoffs, and dependence on the law of the controls ("extended" MFGs, needed for price impact models). Strong-formulation methods do not cover these. It is also the input to the companion results: uniqueness under Lasry–Lions monotonicity (Theorem 3.8) and the construction of approximate Nash equilibria for the $n$-player game (Theorem 4.2), formalized as missions 2 and 3 of this series.

The result is proved in the paper. What this mission adds is a machine-checked development of the weak formulation:

• Girsanov densities with uniform moment bounds;
• the topology $\tau_\psi$ and the compactness of $\mathcal Q$;
• BSDE comparison for control problems;
• upper hemicontinuity of argmax correspondences;
• a Kakutani-type fixed point theorem in locally convex spaces.

None of these is in Mathlib, and no mean field game existence theorem in the weak formulation has been formalized. Formalization also checks the proof. The fixed point theorem as printed (Proposition 7.4, with closed rather than compact values) is false, and the milestone states the corrected version. Connecting it to Lemma 7.11, whose values are closed but not compact in the norm $\mathbb E\int_0^T\|\alpha_t\|\,dt$, is part of the work.

Difficulty

The fixed point is set-valued. Without uniqueness of maximizers, the best response to $(\mu,\nu)$ is a set of controls. Kakutani's theorem in finite dimensions does not apply: the laws live in $\mathcal P_\psi(\mathcal C)$, which with $\tau_\psi$ is neither metrizable nor separable.

The obvious argument would apply Schauder's theorem to $\mu\mapsto P^{\hat\alpha}\circ X^{-1}$ for a measurable selection $\hat\alpha$ of the maximizers. It fails twice. A selection need not depend continuously on $\mu$. And the adjoint process $Z^{\mu,\nu}$, which enters the maximizer, depends on $(\mu,\nu)$ only through a BSDE, with no pointwise regularity.

Compactness has to come from somewhere other than the coefficients. All laws of the form $P^{\mu,\alpha}\circ X^{-1}$ lie in a set $\mathcal Q$ of laws with bounded densities relative to $\mathcal X$. Turning that into compactness for $\tau_\psi$ needs the $\psi^2$-moment of $X$ to upgrade $\tau_1$-convergence to $\tau_\psi$-convergence. Continuity in the control law goes through the stable topology on measures over $[0,T]\times\mathcal P(A)$.

Formalization scope

The Lean development (namespace WeakMFG.Existence) builds on the published Brownian/Itô/BSDE layer Peng1990.SMP.Stochastic. It commits to these conventions:

• Base space. It is an arbitrary probability space carrying $(\xi,W)$, with the filtration of $(\xi,W)$ augmented by null sets. The canonical space $\mathbb R^d\times\mathcal C$ is one instance, and every object of the theorem is a law.
• State equation. It is read through the L² Itô integral, so solutions are square integrable. "$\sigma>0$" is nonsingularity, and the growth function $\rho$ is monotone.
• Types. $\mathbb R^d$ is Fin d → ℝ, time is ℝ≥0, and paths are continuous maps on $[0,T]$.
• Topologies. $\mathcal P_\psi(\mathcal C)$ is its own type carrying $\tau_\psi$. $\mathcal P(A)$ has the weak topology and its Borel $\sigma$-field.
• Densities. Girsanov densities and BSDE solutions are relations. The solution concept asks that a density version exists and that the identities hold for all versions.
• Optimality. $V^{\mu,q}=J^{\mu,q}(\alpha)$ is stated as optimality of $\alpha$ against every admissible control; no real supremum is formed.
• Assumption (E) is sequential continuity, as printed.
• Assumption (C) is required wherever $\sigma(t,x)$ is nonsingular.
• Control set. $A$ is assumed nonempty.

Some formalizations would be trivial and are ruled out. Every clause of Definition 3.4 is stated. No density version may be missing. Optimality is over the whole admissible class, not a subclass. Replacing the goal by a fixed-point statement about the map $\Phi$ is not acceptable, since that is a step of the proof.

Milestone conventions:

• Milestone (7.4). It adds joint measurability of $f$ in the control-law argument. The page presupposes it when it integrates $f$ against $\nu_t(dq)$.
• Berge's theorem. It assumes a nonempty $K$.
• Proposition 7.4. It assumes nonempty compact values (see Significance).

Infrastructure that is reusable beyond this mission:

• Doléans exponentials of bounded integrands and their $L^q$ bounds;
• weak compactness in $L^1$ (Dunford–Pettis) for density sets;
• the stable topology;
• Cellina's approximate selection theorem;
• Schauder–Tychonoff fixed points in locally convex spaces.

Contributions to any of these, and alternative proofs that avoid the non-compact-valued fixed point step, are welcome.

Selected references

• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015; arXiv:1307.1152v2 (2014). https://arxiv.org/abs/1307.1152
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://arxiv.org/abs/1210.5780
• J.-M. Lasry, P.-L. Lions, Mean field games, Jpn. J. Math. 2(1), 2007. https://doi.org/10.1007/s11537-007-0657-8
• M. Huang, R. Malhamé, P. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6(3), 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14(1), 1990. https://doi.org/10.1016/0167-6911(90)90082-6
• A. Cellina, Approximation of set valued functions and fixed point theorems, Ann. Mat. Pura Appl. 82, 1969. https://doi.org/10.1007/BF02410784
• C. D. Aliprantis, K. C. Border, Infinite Dimensional Analysis, 3rd ed., Springer, 2006. https://doi.org/10.1007/3-540-29587-9

Motivation

Adam (Kingma and Ba, 2015, arXiv:1412.6980) is one of the most widely used optimizers for training neural networks. It is a stochastic gradient method that keeps exponential moving averages of the stochastic gradients and of their coordinatewise squares, rescales both by bias-correction factors, and divides the first by the square root of the second. Its original convergence analysis was shown to be flawed (Reddi, Kale and Kumar, 2018, arXiv:1904.09237), and in the regime in which practitioners actually run it, with a constant step size, the iterates do not converge.

Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 3(1), 2021) describe what constant-step Adam does instead: as the step size $\gamma$ tends to zero, with the averaging parameters tending to one at rates proportional to $\gamma$, the interpolated iterates follow a deterministic non-autonomous ordinary differential equation. This mission formalizes that statement, Theorem 4.3 of the paper, together with the lemmas of its proof (§8.1).

Setting

Let $\mathcal Z = \mathbb R^d\times\mathbb R^d\times\mathbb R^d$ with points $z=(x,m,v)$, and $\mathcal Z_+$ its subset with $v\ge0$ coordinatewise. A random sample $\xi$ with law $\mu$ on a measurable space $\Xi$ enters through an integrand $f(x,\xi)$ with gradient $\nabla f(x,\xi)$ in $x$. The objective is $F(x)=\mathbb E f(x,\xi)$ and the second-moment map is $S(x)=\mathbb E\nabla f(x,\xi)^{\odot2}$.

Given a step size $\gamma>0$, parameters $\alpha=\bar\alpha(\gamma)$, $\beta=\bar\beta(\gamma)$ in $[0,1)$ and $\varepsilon>0$, the Adam map $T_{\gamma,\alpha,\beta}(n,z,\xi)$ sends $(x,m,v)$ to

$$\Big(x-\frac{\gamma(1-\alpha^n)^{-1}(\alpha m+(1-\alpha)\nabla f(x,\xi))}{\varepsilon+(1-\beta^n)^{-1/2}(\beta v+(1-\beta)\nabla f(x,\xi)^{\odot2})^{1/2}},\ \alpha m+(1-\alpha)\nabla f(x,\xi),\ \beta v+(1-\beta)\nabla f(x,\xi)^{\odot2}\Big),$$

coordinatewise. The constant-step iterates are $z^\gamma_0=(x_0,0,0)$ and $z^\gamma_n=T_{\gamma,\bar\alpha(\gamma),\bar\beta(\gamma)}(n,z^\gamma_{n-1},\xi_n)$, driven by iid samples $\xi_1,\xi_2,\dots$ with law $\mu$. The interpolated process $\mathsf z^\gamma$ is the piecewise linear function with $\mathsf z^\gamma(n\gamma)=z^\gamma_n$.

The parameters satisfy $(1-\bar\alpha(\gamma))/\gamma\to a>0$ and $(1-\bar\beta(\gamma))/\gamma\to b>0$ as $\gamma\downarrow0$, with $b\le4a$. The limiting Adam ODE is $\dot z(t)=h(t,z(t))$, $z(0)=(x_0,0,0)$, where for $t>0$

$$h(t,z)=\Big(-\frac{(1-e^{-at})^{-1}m}{\varepsilon+\sqrt{(1-e^{-bt})^{-1}v}},\ a(\nabla F(x)-m),\ b(S(x)-v)\Big).$$

The vector field is singular at $t=0$. A global solution is a continuous map $z:[0,\infty)\to\mathcal Z_+$, continuously differentiable on $(0,\infty)$, that satisfies the equation for every $t>0$.

Formalization targets

Goal: Theorem 4.3

Under the paper's assumptions (Assumptions 2.2 to 2.5, 4.1, and 4.2 ii) with $p=2$),

$$\forall T>0,\ \forall\delta>0,\qquad \lim_{\gamma\downarrow0}\mathbb P\Big(\sup_{t\in[0,T]}\|\mathsf z^\gamma(t)-z(t)\|>\delta\Big)=0,$$

where $z$ is the global solution of the Adam ODE from $(x_0,0,0)$.

Milestones, in the order of the proof

• Lemma 8.1. A uniform $(1+s)$-moment bound for the normalised increment $H_\gamma(n+1,z,\xi)$ over states whose debiased version $e_\gamma(n,z)$ lies in a ball.
• Lemma 8.2. Uniform integrability of the increments of the truncated iterates $z^{\gamma,R}$, which are stopped when the debiased iterate leaves the ball of radius $R$.
• Lemma 8.3. Tightness of the truncated interpolated processes $\mathsf z^{\gamma,R}$ in $C([0,\infty),\mathcal Z)$, and vanishing in probability of the accumulated martingale noise.
• Proposition 7.6. The debiased trajectories $\bar e(t+\eta,z(t))$ of the ODE stay in one compact set, and $F(x(t))\le F(x_0)$.
• Lemma 8.4. The mean field $h_\gamma(\varphi_n,z_n)$ converges to $h(t,z)$ when $\gamma\varphi_n\to t$.
• Proposition 7.12. The ODE has exactly one global solution.
• Eq. (8.4). For $R\ge R_0+1$, with $R_0=\sup_{t>0}\|\bar e(t,z(t))\|$, the truncated process converges in probability to $z$, uniformly on $[0,T]$.

Significance

The theorem justifies the continuous-time model of Adam that the rest of the paper studies. The convergence of the ODE to critical points of $F$ (Theorem 3.2) and its rates (Theorem 3.4) say something about the algorithm only through this approximation. It also isolates the role of the bias correction: the initial condition $(x_0,0,0)$ and the singular factors $(1-e^{-at})^{-1}$ are exactly the trace of the debiasing step. The result is also the first step towards the long-run statement, Theorem 4.5, which bounds the time the iterates spend away from the critical points as $\gamma\to0$.

The result is proved on paper. To the knowledge of the mission, none of it is machine-checked: there is no formal statement of Adam's dynamics on Prove2Me. A complete development would give a checked instance of the ODE method for a non-autonomous, non-Lipschitz limit field and a non-homogeneous Markov chain. The surrounding stochastic-approximation library (truncation by stopping, uniform integrability, tightness of interpolated processes, identification of limits by uniqueness) applies to other adaptive methods, such as RMSProp and AdaGrad variants, whose limits have the same structure.

Difficulty

The standard argument for constant-step stochastic approximation assumes a time-homogeneous mean field that is locally Lipschitz. Neither holds here. The mean field $h_\gamma(n,z)$ depends on the iteration index through the bias-correction factors $(1-\bar\alpha(\gamma)^n)^{-1}$. Its limit $h(t,z)$ blows up as $t\downarrow0$, and it is not Lipschitz in $v$ near $v=0$. A direct Gronwall comparison between the iterates and the ODE therefore fails at the origin of time, which is exactly where the iterates start.

The iterates are also not known to be bounded. Moment bounds are only available while the debiased iterate stays in a ball. This forces the truncation $B_R$ and an argument that the truncation is asymptotically never triggered. That argument needs uniform-in-time bounds on the ODE solution (Proposition 7.6) and uniqueness of the solution (Proposition 7.12), and both rest on a Lyapunov function specific to the case $b\le4a$.

Formalization scope

• Spaces and norm. $\mathcal Z$ is E d × E d × E d with E d = EuclideanSpace ℝ (Fin d). The paper's $\|z\|$ is the Euclidean norm of $\mathbb R^{3d}$, written zNorm, not Mathlib's max norm on products.
• Randomness. The probability space is explicit, with a probability measure $\mathbb P$. Independence of $(\xi_{n+1})_n$ is stated with iIndepFun. Every $\xi_n$ with $n\ge1$ has law $\mu$, and $\xi_0$ is unused.
• Gradient. $\nabla f$ is a given function, measurable in $\xi$, that equals the gradient of $f(\cdot,\xi)$ for $\mu$-almost every $\xi$.
• Expectations. Moments, the supremum in Lemma 8.1 and the uniform-integrability expectations are lower Lebesgue integrals in $[0,\infty]$. $F$, $S$ and $h_\gamma$ are Bochner integrals, which the hypotheses make integrable.
• Solutions of the ODE. Solutions are maps $\mathbb R\to\mathcal Z$ constrained only on $[0,\infty)$, and uniqueness means agreement on $[0,\infty)$. The deterministic Propositions 7.6 and 7.12 are stated for any $F$, $S$ satisfying the paper's §7 hypotheses.
• Limit and supremum. The limit is $\gamma\downarrow0$ (𝓝[>] 0). The event $\sup_{t\in[0,T]}\|\cdot\|>\delta$ is written as $\exists t\in[0,T],\ \|\cdot\|>\delta$, which is the same event.
• Tightness. Tightness uses the paper's definition with the compact-open topology on $C([0,\infty),\mathcal Z)$.
• Corrections. Two corrections to the page are recorded in the items. Lemma 8.1 restricts its $n=0$ case to $m=0$, because as printed that case is false. Lemma 8.4 states the implicit regime $\gamma_n\to0$.

A trivializing formalization is ruled out. $T$ and $\delta$ are universally quantified before the limit and do not depend on $\gamma$. The limit is in $\gamma$, not in $n$ at fixed $\gamma$; constant-step Adam does not converge in $n$. The solution $z$ is tied to the $F$, $S$, $a$, $b$ of the stochastic model. All hypotheses are satisfiable, for example by $f(x,\xi)=\tfrac12\|x\|^2+\xi\langle\mathbf 1,x\rangle$ with $\xi=\pm1$ equiprobable.

A complete development needs:

• the deterministic ODE theory of the companion missions (Lyapunov function, boundedness, uniqueness);
• moment and uniform-integrability bounds;
• a tightness criterion in $C([0,\infty),\mathcal Z)$ (Arzelà–Ascoli);
• Prokhorov's and Skorokhod's theorems, or a direct substitute;
• dominated convergence for $h_\gamma$.

Contributions to any of these, including reusable statements about interpolated processes, are welcome.

Selected references

• A. Barakat and 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
• D. P. Kingma and J. Ba, Adam: A Method for Stochastic Optimization, ICLR, 2015. https://arxiv.org/abs/1412.6980
• S. J. Reddi, S. Kale and S. Kumar, On the Convergence of Adam and Beyond, ICLR, 2018. https://arxiv.org/abs/1904.09237
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• P. Bianchi, W. Hachem and A. Salim, Constant step stochastic approximations involving differential inclusions: stability, long-run convergence and applications, Stochastics 91, 2019, pp. 288–320 (reference [6] of the paper; its Lemma 6.2 gives Lemma 8.3). https://arxiv.org/abs/1802.07981

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.