Optimal Transport

Motivation

In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is $c$-cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.

The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale $(X, Y)$ with given marginals $X\sim\mu$, $Y\sim\nu$. Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.

M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for $c$-cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs $h(y-x)$ with $h'$ strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.

Setting

All measures live on $\mathbb R$ or $\mathbb R\times\mathbb R$ with their Borel $\sigma$-algebras. Two probability measures $\mu,\nu$ on $\mathbb R$ with finite first moment 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$.

A transport plan is a measure $\pi$ on $\mathbb R^2$ 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 .$$

A cost is a Borel function $c:\mathbb R^2\to\mathbb R$ satisfying the sufficient integrability condition $c(x,y)\ge a(x)+b(y)$ with $a\in L^1(\mu)$, $b\in L^1(\nu)$; then the cost of a plan, $\int c\,d\pi$, is well defined in $(-\infty,+\infty]$. A plan $\pi\in\Pi_M(\mu,\nu)$ is optimal if $\int c\,d\pi\le\int c\,d\pi'$ for every $\pi'\in\Pi_M(\mu,\nu)$, and it leads to finite costs if $\int c\,d\pi<+\infty$.

A measure $\alpha'$ on $\mathbb R^2$ is a competitor of $\alpha$ (Definition 1.10) if it has the same two marginals as $\alpha$ and the same conditional barycentres: $\int y\,d\alpha_x(y)=\int y\,d\alpha'_x(y)$ for almost every $x$, where $(\alpha_x)$, $(\alpha'_x)$ are disintegrations with respect to the first marginal. A competitor redistributes the mass of $\alpha$ in a way that a martingale plan could absorb: replacing a piece $\alpha$ of a martingale plan by $\alpha'$ keeps both marginals and the martingale property.

Formalization targets

Goal: the variational lemma (Lemma 1.11, p. 8)

Let $\mu\preceq_C\nu$ be probability measures, $c$ a Borel cost satisfying the sufficient integrability condition, and $\pi\in\Pi_M(\mu,\nu)$ optimal with $\int c\,d\pi<+\infty$. Then there is a Borel set $\Gamma\subseteq\mathbb R^2$ with $\pi(\Gamma)=1$ such that

$$\int c\,d\alpha\le\int c\,d\alpha'\quad\text{for every finitely supported }\alpha\text{ with }\operatorname{spt}\alpha\subseteq\Gamma\text{ and every competitor }\alpha'\text{ of }\alpha .$$

The set $\Gamma$ is chosen once, before $\alpha$; the quantifier order is the content.

Milestones

The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:

1. Theorem 3.1 (p. 17), Kellerer's duality in the form of Beiglböck–Goldstern–Maresch–Schachermayer: for a Polish probability space $(Z,\zeta)$ and a Borel $M\subseteq Z^n$, either $M\subseteq\bigcup_i M_i$ with $\zeta(\operatorname{proj}^iM_i)=0$, or some measure $\gamma$ with $\gamma(M)>0$ has all marginals $\le\zeta$.
2. The set $M\subseteq(\mathbb R^2)^n$ of $n$-tuples carrying a non-optimal finite measure is Borel (p. 17).
3. In case (1), a Borel $\Gamma_n$ of full $\pi$-measure supports no improvable $\alpha$ with $|\operatorname{spt}\alpha|\le n$ (p. 18).
4. Every finitely supported $\alpha$ has a cost-minimizing competitor (p. 18).
5. If $\omega\le\pi$ and a competitor $\omega'$ is cheaper than $\omega$, then $\pi-\omega+\omega'$ is a cheaper martingale plan (p. 18).
6. For an optimal $\pi$ of finite cost, case (2) cannot occur (pp. 18–19).
7. $\Gamma=\bigcap_n\Gamma_n$ is as required (p. 17).

Significance

The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs $h(y-x)$ with $h'$ strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound $|\operatorname{spt}\pi_x|\le k$ of Theorem 7.1 and the two-graph structure of the optimizers for $\pm|y-x|$. Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in $\Pi_M(\mu,\nu)$. Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.

Difficulty

The classical proof of $c$-cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every $x$, and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor $\omega'$ of a piece $\omega\le\pi$, is the technical core.

Formalization scope

The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral ($\int f^+-\int f^-$, with $(+\infty)-(+\infty)=-\infty$); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions $\rho(x)$ (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written $\sum_{s\in S}w_s\delta_s$ with $S$ a finite set and weights $w_s\ge0$; this covers every such measure, and masses are taken finite. $(\mathbb R^2)^n$ is Fin n → ℝ × ℝ.

Committed conventions and disclosed additions:

• the goal's hypothesis "leads to finite costs" is $\int c\,d\pi<+\infty$; without it, a cost under which every plan has infinite cost makes optimality empty;
• Theorem 3.1 is stated for Borel $M$, the case proved in the cited source and the only case the paper uses; $\zeta(\operatorname{proj}^iM_i)=0$ is the outer measure, since the projections need not be Borel;
• in milestone 3, $\Gamma_n$ is a Borel subset of the paper's $\mathbb R^2\setminus N$ of full measure, because $N$ need not be Borel;
• milestone 4 states, for the uniform measure $\alpha_p$ on the points of an $n$-tuple $p$, both that an optimal competitor $\alpha'_p$ exists and that it can be chosen measurably in $p$ (p. 18), with Mathlib's σ-algebra on the space of measures.

A formalization in which $\Gamma$ is empty or $\pi$-null, or in which $\Gamma$ is allowed to depend on $\alpha$, is trivial and is ruled out by the statement: $\pi(\Gamma^c)=0$ and $\exists\Gamma\,\forall\alpha$. The competitor $\alpha'$ ranges over all measures, not only finitely supported ones.

Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509, doi:10.1214/14-AOP966
• M. Beiglböck, 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
• H. G. Kellerer, Duality theorems for marginal problems, Z. Wahrsch. Verw. Gebiete 67(4), 399–432, 1984. doi:10.1007/BF00532047
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. doi:10.1007/s00780-013-0205-8
• C. Villani, Optimal Transport, Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

Motivation

The Kalman filter estimates the hidden state of a linear system from noisy observations. At every step it solves a minimum mean square error (MMSE) estimation problem: given a joint normal distribution of a signal $x$ and an observation $y$, find the estimator $\psi(y)$ minimizing $\mathbb E[\|x-\psi(y)\|^2]$. The answer, the conditional mean, is optimal only if the model distribution is correct, and in practice the system matrices and noise covariances are estimated and misspecified.

Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830, NeurIPS 2018) replace the single model by a set of plausible models: all normal distributions within type-2 Wasserstein distance $\rho$ of a nominal normal distribution. The estimator is then chosen to minimize the worst-case mean square error over this set. Their Theorem 2.5 shows that this robust estimation problem, although posed over an infinite-dimensional space of estimators and a nonconvex set of distributions, has the same value as a finite convex program over covariance matrices, and that the robust estimator is affine. Applied at every time step, this yields the Wasserstein distributionally robust Kalman filter of the paper's §4.

This mission formalizes Theorem 2.5 together with the minimax theorem (Theorem 2.3) and the lemmas of its proof.

Setting

Let $n, m \ge 0$ and $d = n+m$. A point of $\mathbb R^d$ is $z = [x; y]$ with signal $x\in\mathbb R^n$ and observation $y\in\mathbb R^m$. A symmetric matrix $S \in \mathbb R^{d\times d}$ is partitioned as $S = \begin{bmatrix} S_{xx} & S_{xy}\\ S_{yx} & S_{yy}\end{bmatrix}$. $\mathbb S^d_+$ ($\mathbb S^d_{++}$) denotes the positive semidefinite (definite) matrices, $A \succeq B$ means $A-B\in\mathbb S^d_+$, $\langle A,B\rangle = \operatorname{Tr}[A^\top B]$, and $A^{1/2}$ is the positive semidefinite square root of $A\succeq 0$.

Normal distributions. $\mathcal N_d(c,S)$ is the normal distribution on $\mathbb R^d$ with mean $c$ and covariance $S\in\mathbb S^d_+$; singular $S$ is allowed. $\mathcal N_d$ is the set of all of them.

Wasserstein distance. For distributions $\mathbb Q_1,\mathbb Q_2$ on $\mathbb R^d$,

$$W_2(\mathbb Q_1,\mathbb Q_2) = \inf_{\pi} \Bigl(\int \|z_1-z_2\|^2\,\pi(dz_1,dz_2)\Bigr)^{1/2},$$

the infimum ranging over all distributions $\pi$ on $\mathbb R^d\times\mathbb R^d$ with marginals $\mathbb Q_1$ and $\mathbb Q_2$.

Ambiguity set. Fix $\mu = [\mu_x;\mu_y]\in\mathbb R^d$, $\Sigma\in\mathbb S^d_{++}$, the nominal distribution $\mathbb P=\mathcal N_d(\mu,\Sigma)$ and a radius $\rho\ge 0$. The Wasserstein ambiguity set is

$$\mathcal P = \{\mathbb Q\in\mathcal N_d : W_2(\mathbb Q,\mathbb P)\le\rho\}.$$

Robust estimation. Let $\mathcal L$ be the set of all measurable functions $\psi:\mathbb R^m\to\mathbb R^n$. The distributionally robust MMSE problem is

$$\inf_{\psi\in\mathcal L}\ \sup_{\mathbb Q\in\mathcal P}\ \mathbb E^{\mathbb Q}\bigl[\|x-\psi(y)\|^2\bigr], \tag{2}$$

and a distributionally robust MMSE estimator is a $\psi$ attaining the outer infimum. Nature's problem exchanges the two optimizations; a $\mathbb Q^\star\in\mathcal P$ attaining its outer supremum is a least favorable prior.

The finite program. With $\underline\sigma = \lambda_{\min}(\Sigma)$, program (5) maximizes $f(S)=\operatorname{Tr}[S_{xx}-S_{xy}S_{yy}^{-1}S_{yx}]$ over $S\in\mathbb S^d_+$ (with $S_{xx}\in\mathbb S^n_+$, $S_{yy}\in\mathbb S^m_+$) subject to

$$\operatorname{Tr}\bigl[S+\Sigma-2(\Sigma^{1/2}S\Sigma^{1/2})^{1/2}\bigr]\le\rho^2,\qquad S\succeq\underline\sigma I_d .$$

Formalization targets

Goal: Theorem 2.5 (p. 3)

1. The optimal value of (2) equals the optimal value of (5).
2. If $S^\star$ is optimal in (5), then

$$\psi^\star(y) = S^\star_{xy}(S^\star_{yy})^{-1}(y-\mu_y)+\mu_x$$

is a distributionally robust MMSE estimator. 3. For the same $S^\star$, $\mathbb Q^\star=\mathcal N_d(\mu,S^\star)$ lies in $\mathcal P$ and is a least favorable prior.

Existence and uniqueness of an optimal $S^\star$ are not part of the statement.

Milestones, in the order of the proof

• Proposition 2.2 (Gelbrich formula): for $\Sigma_1,\Sigma_2\succeq 0$,

$$W_2\bigl(\mathcal N_d(\mu_1,\Sigma_1),\mathcal N_d(\mu_2,\Sigma_2)\bigr)=\sqrt{\|\mu_1-\mu_2\|^2+\operatorname{Tr}\bigl[\Sigma_1+\Sigma_2-2(\Sigma_2^{1/2}\Sigma_1\Sigma_2^{1/2})^{1/2}\bigr]}.$$

• Lemma A.1: the closed form of $\sup_{S\succeq0}\langle D,S\rangle-\gamma\operatorname{Tr}[S-2(\Sigma^{1/2}S\Sigma^{1/2})^{1/2}]$ and its unique maximizer.
• (A.1b): under a fixed normal distribution, affine estimators $y\mapsto Gy+g$ achieve the minimum mean square error over $\mathcal L$.
• Theorem 2.3 (minimax theorem): $\inf_{\psi\in\mathcal L}\sup_{\mathbb Q\in\mathcal P}\mathbb E^{\mathbb Q}[\|x-\psi(y)\|^2] = \sup_{\mathbb Q\in\mathcal P}\inf_{\psi\in\mathcal L}\mathbb E^{\mathbb Q}[\|x-\psi(y)\|^2]$.
• Lemma A.2: the maximizer of $\langle S,D\rangle$ under the Wasserstein-type trace constraint, and $S^\star\succeq\underline\sigma I_d$.
• (A.6): for $S\succ0$, $\min_G\bigl\langle\begin{bmatrix}I_n&-G\\-G^\top&G^\top G\end{bmatrix},S\bigr\rangle=f(S)$, uniquely at $G^\star=S_{xy}S_{yy}^{-1}$.

Significance

The result. Theorem 2.5 gives the robust estimator in closed form from one optimal covariance matrix, and identifies the least favorable distribution as a normal distribution with the nominal mean. Together with Theorem 2.3 it shows that the pair $(\psi^\star,\mathbb Q^\star)$ is a saddle point: the robust estimator is the Bayesian estimator for the least favorable prior. For $\rho=0$ the program has the single feasible point $\Sigma$ and the estimator reduces to the classical conditional mean, so the theorem contains the Kalman update as a special case. The finite program is what makes the robust filter of §4 computable; the paper's §3 (formalized in the companion mission of this series) solves it with a Frank–Wolfe method.

Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked yet. The Gelbrich formula for normal distributions (Proposition 2.2) is cited from the literature and has no formal proof in Mathlib; neither does Lemma A.1, cited from earlier work of the same authors. A closely related statement for a Wasserstein ball over all distributions around an elliptical nominal (Kuhn et al. 2019, Theorem 25) is posed on the platform as WassersteinDRO.Shrinkage.distributionally_robust_mmse_estimator; it is a different theorem, since the ambiguity set there is convex and contains non-normal distributions.

Difficulty

The ambiguity set $\mathcal P$ is not convex, because a mixture of normal distributions is generally not normal. The standard route to a minimax equality, Sion's theorem, needs convexity on nature's side and therefore does not apply to (2) directly; the obvious attempt to interchange the infimum and the supremum fails at this step. The space $\mathcal L$ of measurable estimators is infinite-dimensional, and the Wasserstein constraint is an infimum over couplings, so a proof must pass to finite-dimensional descriptions on both sides (means and covariances for $\mathbb Q$, affine maps for $\psi$) and justify each passage. The matrix-analytic parts involve the nonlinear map $S\mapsto(\Sigma^{1/2}S\Sigma^{1/2})^{1/2}$, for which Mathlib has square roots but little calculus.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin n ⊕ Fin m); the Sum.inl coordinates are $x$, the Sum.inr coordinates are $y$, and the blocks of a matrix are toBlocks₁₁, toBlocks₁₂, toBlocks₂₁, toBlocks₂₂.
• $\mathcal N_d(c,S)$ is Mathlib's multivariateGaussian c S with S.PosSemidef; only the nominal $\Sigma$ is required to be positive definite.
• $W_2$ is the published coupling-based WassersteinDRO.Shrinkage.wassersteinDistance 2 in $[0,\infty]$. The ambiguity set is defined through it, not through the Gelbrich formula; the formula is Proposition 2.2, a milestone.
• Expectations are lower Lebesgue integrals in $[0,\infty]$, with no integrability guard. A non-integrable estimator therefore has infinite risk and cannot lower the infimum through a junk value.
• The values of (2) and of nature's problem are in $[0,\infty]$; the value of (5) is the published sdpValue in EReal, and the two are compared through the coercion.
• $\underline\sigma$ is passed as a real number that is the least eigenvalue of $\Sigma$.
• "Equivalent" in Theorem 2.5 is read as the three claims above. A version that asserts only equality of values, or optimality of $\psi^\star$ among affine estimators only, is weaker than the theorem and is not the goal.
• Lemma A.2 carries the added hypothesis $\rho>0$, without which its algebraic equation has no admissible root.

A complete development needs the Gelbrich formula for (possibly degenerate) normal distributions, conditional means of jointly normal vectors, a minimax theorem for convex–concave functions on compact sets, Lagrangian duality for a convex semidefinite program, and calculus of the positive semidefinite square root. The first three are reusable well beyond this mission, and contributions of any of them as separate results are welcome.

Selected references

• S. Shafieezadeh-Abadeh, V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Wasserstein Distributionally Robust Kalman Filtering, NeurIPS 2018; arXiv:1809.08830v3. https://arxiv.org/abs/1809.08830
• M. Gelbrich, On a formula for the L² Wasserstein metric between measures on Euclidean and Hilbert spaces, Mathematische Nachrichten 147, 1990. https://doi.org/10.1002/mana.19901470121
• V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Distributionally robust inverse covariance estimation, arXiv:1802.01981, 2018. https://arxiv.org/abs/1802.01981
• D. Kuhn, P. Mohajerin Esfahani, V. A. Nguyen, S. Shafieezadeh-Abadeh, Wasserstein distributionally robust optimization: theory and applications in machine learning, INFORMS TutORials, 2019; arXiv:1908.08729. https://arxiv.org/abs/1908.08729
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009.

Motivation

A Kalman filter estimates the hidden state $x$ of a linear system from observations $y$, assuming the joint law of $z = (x, y)$ is a known Gaussian. When that law is only approximately known, Shafieezadeh-Abadeh, Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1809.08830v3, NeurIPS 2018) replace it by the worst Gaussian within a 2-Wasserstein ball of radius $\rho$ around a nominal Gaussian with covariance $\Sigma$. Their Theorem 2.5 shows that the resulting minimax estimation problem is equivalent to a finite nonlinear semidefinite program, program (5), whose objective is $f(S) = \mathrm{Tr}[S_{xx} - S_{xy}S_{yy}^{-1}S_{yx}]$.

Each step of the robust filter solves program (5), so the filter is only practical if (5) can be solved quickly. The paper solves it with a Frank–Wolfe method (Algorithm 2), which avoids projections by replacing the objective with its linearization at the current iterate and maximizing that linear function over the original feasible set. That inner problem, the direction-finding subproblem, is again a nonlinear SDP. The paper's Algorithm 1 solves it by a one-dimensional bisection, and Theorem 3.2 states that this bisection returns a feasible solution whose objective value is within a prescribed tolerance $\varepsilon$ of the optimum. This mission formalizes that guarantee.

Setting

Fix dimensions $n \ge 1$ (state) and $m$ (observation), $d = n + m$, and index coordinates so that the first $n$ belong to $x$. Let $\mathbb{S}^d_+$ and $\mathbb{S}^d_{++}$ denote the positive semidefinite and positive definite $d\times d$ matrices, and $\langle A, B\rangle = \mathrm{Tr}[A^\top B]$ the trace inner product. The data are a nominal covariance $\Sigma \in \mathbb{S}^d_{++}$ with smallest eigenvalue $\underline\sigma = \lambda_{\min}(\Sigma)$, a radius $\rho > 0$, a tolerance $\varepsilon > 0$, and the current Frank–Wolfe iterate $S \in \mathbb{S}^d_+$, written in blocks $S_{xx}, S_{xy}, S_{yx}, S_{yy}$.

The gradient matrix is

$$D = \nabla f(S) = [I_n, -G]^\top [I_n, -G], \qquad G = S_{xy}S_{yy}^{-1},$$

which is positive semidefinite and nonzero. The direction-finding subproblem (7b) is

$$\max_{L \succeq \underline\sigma I_d}\ \langle L, D\rangle \quad \text{s.t.}\quad \mathrm{Tr}\Big[L + \Sigma - 2\big(\Sigma^{1/2} L \Sigma^{1/2}\big)^{1/2}\Big] \le \rho^2 ;$$

its constraint says that the Gaussian with covariance $L$ lies within Wasserstein distance $\rho$ of the nominal Gaussian, and $\mathcal F$ denotes its feasible set. For $\gamma$ with $\gamma I_d \succ D$ the paper defines

$$h(\gamma) = \rho^2 - \big\langle \Sigma, (I_d - \gamma(\gamma I_d - D)^{-1})^2\big\rangle, \qquad L(\gamma) = \gamma^2 (\gamma I_d - D)^{-1}\Sigma(\gamma I_d - D)^{-1},$$ $$\Delta(\gamma) = \gamma(\rho^2 - \mathrm{Tr}[\Sigma]) - \langle L(\gamma), D\rangle + \gamma^2\langle(\gamma I_d - D)^{-1}, \Sigma\rangle .$$

Algorithm 1 takes the largest eigenvalue $\lambda_1$ of $D$ and a unit eigenvector $v_1$, and starts from the bracket $[LB, UB] = [\gamma_{\min}, \gamma_{\max}]$ with

$$\gamma_{\min} = \lambda_1\big(1 + \sqrt{v_1^\top\Sigma v_1}/\rho\big), \qquad \gamma_{\max} = \lambda_1\big(1 + \sqrt{\mathrm{Tr}[\Sigma]}/\rho\big).$$

Each pass sets $\gamma = (UB + LB)/2$ and $L = L(\gamma)$, replaces $LB$ by $\gamma$ if $h(\gamma) < 0$ and $UB$ by $\gamma$ otherwise, and the loop exits with output $L$ as soon as $h(\gamma) > 0$ and $\Delta(\gamma) < \varepsilon$.

Formalization targets

Goal: Theorem 3.2

For all inputs as above:

1. Soundness. At every pass $k$ whose exit test holds, with trial point $\gamma_k$,

$$L(\gamma_k) \in \mathcal F \quad\text{and}\quad \langle L', D\rangle \le \langle L(\gamma_k), D\rangle + \varepsilon \ \text{ for all } L' \in \mathcal F .$$

2. Termination. If $h$ has no zero at a dyadic point $\gamma_{\min} + j(\gamma_{\max} - \gamma_{\min})/2^k$, $0 < j \le 2^k$, then some pass satisfies the exit test.

The termination hypothesis is a correction: the printed theorem asserts that the algorithm outputs a solution, but if a trial point (or $\gamma_{\max}$) coincides exactly with the root of $h$, the upper end of the bracket becomes that root, all later trial points have $h < 0$, and the loop never exits. Soundness holds unconditionally. The normalization $\|v_1\| = 1$ is also added; the page says only "an eigenvector", and $\gamma_{\min}$ is not a lower bound for a rescaled one.

Milestones (App. A.3, p. 13, in the order the proof uses them)

• $L(\gamma) \in \mathcal F$ whenever $\gamma I_d \succ D$ and $h(\gamma) > 0$.
• Weak duality: $\langle L', D\rangle \le \gamma(\rho^2 - \mathrm{Tr}[\Sigma]) + \gamma^2\langle (\gamma I_d - D)^{-1}, \Sigma\rangle$ for all $L' \in \mathcal F$ and $\gamma \ge 0$ with $\gamma I_d \succ D$.
• The suboptimality display: if $h(\gamma^\star) = 0$ then $\langle L(\gamma^\star) - L(\gamma), D\rangle \le \gamma(\rho^2 - \mathrm{Tr}[\Sigma]) + \gamma^2\langle(\gamma I_d - D)^{-1}, \Sigma\rangle - \langle L(\gamma), D\rangle$.
• Lemma A.3: every root $\gamma^\star$ of $h$ with $\gamma^\star I_d \succ D$ lies in $[\gamma_{\min}, \gamma_{\max}]$.

Significance

Theorem 3.2 is what makes Algorithm 1 a valid linear-maximization oracle for the Frank–Wolfe method on program (5): the convergence analysis of Frank–Wolfe with inexact oracles requires exactly a feasible point whose linearized objective is within a known tolerance of the optimum. It also shows that the inner problem, a semidefinite program with a matrix square root in the constraint, reduces to a scalar root-finding problem once $D$ is diagonalized, which is why the robust filter runs at a cost comparable to an eigendecomposition per step.

The result is proved in the paper; no machine-checked version exists. The formal version adds what the paper leaves implicit: the termination edge case, the normalization of $v_1$, and the requirement $D \ne 0$ (here $n \ge 1$). The milestone statements on Lagrangian weak duality for the Wasserstein–Gaussian trust region and on the location of the multiplier are reusable for other covariance-robust programs of the same shape, such as Wasserstein shrinkage estimation.

Difficulty

The algorithm is elementary; the analysis is not. Feasibility of $L(\gamma)$ requires computing the matrix square root $(\Sigma^{1/2}L(\gamma)\Sigma^{1/2})^{1/2}$ in closed form and comparing eigenvalues of non-commuting products to obtain $L(\gamma) \succeq \underline\sigma I_d$. The dual bound is a semidefinite Lagrangian duality statement over a constraint involving a matrix square root, whose inner supremum (Lemma A.1, cited from earlier work) must be evaluated in closed form. Termination needs monotonicity and continuity of $h$ on $(\lambda_1, \infty)$ and a careful account of which side of the root each bisection update lands on; the obvious invariant "the root stays strictly inside the bracket" fails precisely in the excluded dyadic case.

Formalization scope

Matrices are indexed by Fin n ⊕ Fin m with blocks toBlocks₁₁ ($xx$), toBlocks₁₂ ($xy$), toBlocks₂₂ ($yy$). The feasible set $\mathcal F$ is the published definition WassersteinDRO.Shrinkage.sdpFeasibleSet ρ Σ σ, which uses the published positive semidefinite square root psdSqrt. Mathlib's matrix inverse returns $0$ on singular matrices; every statement involving $h$, $L$ or $\Delta$ assumes $\gamma I_d \succ D$ or works at trial points that lie above $\lambda_1$, and $S_{yy}^{-1}$ is allowed to be this junk value because the theorem admits any $S \in \mathbb{S}^d_+$ (then $D = \mathrm{diag}(I_n, 0)$). The constants $\underline\sigma$ and $\lambda_1$ are passed as reals together with hypotheses that pin them to the smallest eigenvalue of $\Sigma$ and the largest eigenvalue of $D$. The algorithm is modelled as its sequence of passes, not as a function returning an output, so a non-terminating run cannot silently produce a value.

A formalization that defines the output with a fuel bound or a default value, that states only optimality of $L(\gamma^\star)$ at the exact root, or that assumes termination as a hypothesis would not be Theorem 3.2; $\varepsilon$-suboptimality is stated against every feasible point, not against a supremum that could be a junk value.

A complete development needs the spectral theorem for symmetric matrices, uniqueness of the positive semidefinite square root, and semidefinite Lagrangian duality; Mathlib supplies the first two. Proofs of the milestones are welcome contributions.

Selected references

• S. Shafieezadeh-Abadeh, V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Wasserstein Distributionally Robust Kalman Filtering, NeurIPS 2018; arXiv:1809.08830v3. https://arxiv.org/abs/1809.08830
• V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Distributionally Robust Inverse Covariance Estimation: The Wasserstein Shrinkage Estimator, Optimization Online, 2018; arXiv:1805.07194 (reference [18] of the paper; source of Lemma A.1). https://arxiv.org/abs/1805.07194
• M. Jaggi, Revisiting Frank–Wolfe: Projection-Free Sparse Convex Optimization, ICML 2013 (reference [13]; Frank–Wolfe with approximate oracles). https://proceedings.mlr.press/v28/jaggi13.html

Motivation

In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution $P$ and judged by its risk under that same $P$. In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at $P$ by the worst risk over a neighbourhood of $P$. When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).

Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual $1/\sqrt n$ rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.

Setting

The instance space $\mathcal Z$ is a Polish metric space with metric $d_{\mathcal Z}$ and Borel $\sigma$-algebra; fix $p\ge1$. For Borel probability measures $P,Q$ on $\mathcal Z$, the $p$-Wasserstein distance is

$$W_p(P,Q)=\Bigl(\inf_{M}\ \mathbf E_M[d^p_{\mathcal Z}(Z,Z')]\Bigr)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho>0$, $B^W_{\varrho,p}(P)=\{Q:W_p(P,Q)\le\varrho\}$ is the Wasserstein ball around $P$.

A hypothesis is a function $f:\mathcal Z\to\mathbb R$, read as a loss; a hypothesis class is a set $\mathcal F$ of them. The risk of $f$ under $Q$ is $R(Q,f)=\int f\,dQ$. The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f),\qquad R^*_{\varrho,p}(P,\mathcal F)=\inf_{f\in\mathcal F}R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n\sim P$ with empirical distribution $P_n=\frac1n\sum_i\delta_{Z_i}$, the local minimax ERM is

$$\hat f\in\arg\min_{f\in\mathcal F}R_{\varrho,p}(P_n,f).$$

The standing assumptions are:

• Assumption 1. $\mathcal Z$ is bounded: $\mathrm{diam}(\mathcal Z)=\sup_{z,z'}d_{\mathcal Z}(z,z')<\infty$.
• Assumption 2. Every $f\in\mathcal F$ is upper semicontinuous with $0\le f(z)\le M$.
• Assumption 4. Some $f_0\in\mathcal F$ satisfies $f_0(z)\le C_0\,d^p_{\mathcal Z}(z,z_0)$ for all $z$, for some $C_0\ge0$ and $z_0\in\mathcal Z$.

The complexity of $\mathcal F$ is measured by the entropy integral $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$, where $\mathcal N$ is the covering number of $\mathcal F$ in the uniform norm.

Formalization targets

Goal: Theorem 3, display (11)

Under Assumptions 1, 2 and 4, for every $\delta\in(0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f)-R^*_{\varrho,p}(P,\mathcal F)\le\frac{48\,\mathfrak C(\mathcal F)}{\sqrt n}+\frac{24\,C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}\Bigl(1+\Bigl(\frac{\mathrm{diam}(\mathcal Z)}{\varrho}\Bigr)^p\Bigr)+3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones

1. Proposition 4 (Gao–Kleywegt strong duality): $R_{\varrho,p}(Q,f)=\min_{\lambda\ge0}\{\lambda\varrho^p+\mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$ with $\varphi_{\lambda,f}(z)=\sup_{z'}\{f(z')-\lambda d^p_{\mathcal Z}(z,z')\}$, in the bounded setting.
2. Lemma 2: the optimal dual multiplier of a minimiser of $R_{\varrho,p}(Q,\cdot)$ lies in $\Lambda=[0,\,C_0 2^{p-1}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)]$.
3. (C.2): for an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le\int\varphi_{\lambda^*,f^*}\,d(P_n-P)$.
4. (C.3): $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)\le\sup_{\varphi\in\Phi}\int\varphi\,d(P-P_n)$, with $\Phi=\{\varphi_{\lambda,f}:\lambda\in\Lambda,f\in\mathcal F\}$.
5. (C.4): with probability at least $1-\delta/2$, the left side of (C.3) is at most $2\mathfrak R_n(\Phi)+M\sqrt{2\log(2/\delta)/n}$, where $\mathfrak R_n$ is the expected Rademacher average.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le M\sqrt{\log(2/\delta)/(2n)}$.
7. Lemma 5: $\mathfrak R_n(\Phi)\le\frac{24}{\sqrt n}\mathfrak C(\mathcal F)+\frac{12C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)$.

The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.

Significance

The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when $p>1$: a function with $\sup_{z,z'}(f(z')-f(z))/d^p_{\mathcal Z}(z,z')<\infty$ is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as $\varrho$ grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).

Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.

Difficulty

The obvious argument decomposes the excess risk through $f^*$ and bounds $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)$ by a uniform deviation over $\mathcal F$. That step fails: $R_{\varrho,p}(\cdot,f)$ is a supremum over a ball of measures, not an expectation, so it is not an empirical process in $f$. Passing to the dual makes it one, but the dual multiplier $\hat\lambda$ depends on the sample and has no a priori bound, so the class $\{\varphi_{\lambda,f}\}$ over all $\lambda\ge0$ is too large. Without uniform smoothness of $\mathcal F$ there is no obvious a priori bound on $\hat\lambda$, and the entropy of the resulting two-parameter class must still be controlled at rate $1/\sqrt n$. Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and $\mathrm{diam}(\mathcal Z)$ is Metric.diam Set.univ. Throughout, $p\ge1$ and $\varrho>0$ (the paper's standing choice, p. 3).
• The Wasserstein distance and ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's $\mathcal P_p(\mathcal Z)$ ball.
• Local risks, $\varphi_{\lambda,f}$, $\Lambda$, $\Phi$ and $\mathfrak R_n$ are real-valued suprema and infima, used only for classes bounded in $[0,M]$, where they are finite.
• The sample is a point of $\mathcal Z^n$ under $P^{\otimes n}$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$; this equals the probability when the set is measurable and is stronger otherwise.
• The ERM is a sample-indexed function $\hat f$ with hypotheses $\hat f(\omega)\in\mathcal F$ and minimality of $R_{\varrho,p}(P_n,\cdot)$. These hypotheses presuppose that an empirical minimiser exists, as (7) does. No measurability of $\hat f$ is assumed.
• The covering number is internal (centres in $\mathcal F$). $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$, and every bound containing it assumes $\mathfrak C(\mathcal F)<\infty$: otherwise the paper's bound is $+\infty$, while its conversion to a real number would be $0$.
• Proposition 4 is stated for bounded upper semicontinuous $f$ on bounded $\mathcal Z$, the only case the paper uses. The printed statement covers every usc $f$ and every $Q\in\mathcal P_p(\mathcal Z)$.
• (C.2) and (C.5) assume an achiever $f^*$, as printed; the goal does not.

The following formalizations would trivialize the goal and are ruled out: a bound for each fixed $f\in\mathcal F$ in place of $R^*_{\varrho,p}(P,\mathcal F)$; an $\hat f$ defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite $\mathfrak C(\mathcal F)$.

The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.

Selected references

• J. Lee, M. Raginsky, Minimax statistical learning with Wasserstein distances, NeurIPS 2018; arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• A. Sinha, H. Namkoong, J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1, 1967. https://doi.org/10.1016/0022-1236(67)90017-1

Motivation

A decision based on observed data can change when the data law differs from the one used to choose it. Distributionally robust optimization addresses this by evaluating each decision against a family of nearby probability laws. Optimal transport gives one way to define “nearby”: a candidate law is admissible when probability mass can be moved from the baseline law at a bounded expected cost. For a linear decision rule, the resulting worst-case expectation is usually harder to optimize than an ordinary sample-average loss. Blanchet, Murthy, and Zhang identify a dual objective whose variables are the decision vector and a scalar transport multiplier, then study its curvature near the multipliers that actually minimize it (Blanchet–Murthy–Zhang, 2022).

The paper proves that this dual objective is jointly strongly convex on a specified region for sufficiently small transport radius. This matters because ordinary convexity allows flat directions in the joint decision–multiplier space. The joint lower Hessian bound gives local curvature in every direction with one positive modulus that remains independent of the radius apart from the paper's explicit factor $\sqrt{\delta}$ (Theorem 4, p. 11).

Setting

Let $X\in\mathbb R^d$ have a baseline probability law $P_0$, and let a decision be a vector $\beta$ in a nonempty compact convex set $B\subseteq\mathbb R^d$. The loss of a possible outcome $x$ is $\ell(\beta^{\mathsf T}x)$ for a convex function $\ell:\mathbb R\to\mathbb R$. A state-dependent positive-definite matrix $A(x)$ sets the cost of moving mass from $x$ to $x'$:

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x').$$

Assumption 1 requires this cost to be lower semicontinuous and the eigenvalues of $A(x)$ to lie between positive constants $\rho_{\min}$ and $\rho_{\max}$ for $P_0$-almost every $x$. Assumption 2 requires at most quadratic growth of $\ell$ and a finite fourth moment of $P_0$. The ambiguity radius $\delta$ is positive (Assumptions 1–2, pp. 9–10).

The paper's dual objective is an expectation under the known law $P_0$. Write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$. For a scalar $\lambda\ge0$ and an auxiliary scalar $\gamma$, set

$$F(\gamma,\beta,\lambda;x) =\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr) -\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr), \qquad f_\delta(\beta,\lambda)=\mathbb E_{P_0}\!\left[\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;X)\right].$$

This value may be $+\infty$. Under the paper's duality conditions, minimizing $f_\delta(\beta,\lambda)$ over $\lambda\ge0$ gives the worst-case loss at $\beta$ (Theorem 1 and (7), p. 10).

Formalization targets

Assumption 3 bounds $\ell''$ above by $M>0$ and excludes an almost surely zero $\ell'(\beta^{\mathsf T}X)$ for each $\beta\in B$. Assumption 4 makes $B$ compact. Lemma 6 supplies positive constants $\underline L,\overline L$ bounding $\mathbb E_{P_0}[\ell'(\beta^{\mathsf T}X)^2]$ uniformly over $B$. With $R_\beta=\sup_{\beta\in B}\|\beta\|$, the constants $K_1,K_2$ are those of (28), and

$$\mathbb V_\delta=\{(\beta,\lambda):\beta\in B,\ \lambda\ge0,\ K_1\|\beta\|\le\lambda\le K_2\|\beta\|\}.$$

Theorem 3 first gives a bounded Hessian on $\mathbb V_\delta$ and a positive lower bound on its $\beta$ block when $0<\delta<\delta_0$, with the explicit $\delta_0$ from p. 36. The goal, Theorem 4, adds Assumption 5: $\ell$ is locally strongly convex and, at each $\beta\in B$, the loss derivative and the linear score are simultaneously separated from zero with positive probability. It asserts the joint bound

$$\exists\,\delta_1\in(0,\delta_0),\ \kappa_1>0\quad \forall\,\delta\in(0,\delta_1),\ \forall\,\theta\in\mathbb V_\delta:\quad \nabla^2 f_\delta(\theta)\succeq\sqrt\delta\,\kappa_1 I_{d+1}.$$

The order of the quantifiers is part of the target: $\kappa_1$ works for every sufficiently small $\delta$ (Theorems 3–4, p. 11).

Significance

The Hessian bound makes the joint dual parameters locally identifiable by curvature on a region that contains every dual optimizer. In the paper, this structure also underlies the analysis of algorithms and of how the optimizer changes with the transport radius (Proposition 1, p. 11; §3 and §5.4). Theorem 4 is already proved in the paper; this mission asks for its machine-checked formalization, together with the stated bounds on multipliers, the maximizing scalar, and the intermediate curvature results. The general optimal-transport integral used here already has a published Prove2Me definition from Blanchet and Murthy's earlier model-risk work. The new definitions specify this paper's Mahalanobis model, regions, and smoothness assumptions.

Difficulty

Convexity alone gives only a nonnegative Hessian; it cannot produce a strictly positive joint lower bound. Even curvature of $\ell$ does not by itself control directions that combine a change in $\beta$ with a change in $\lambda$. The inner supremum over $\gamma$ can become infinite outside its effective domain, while at $\beta=0$ its maximizer ceases to be unique. The theorem therefore needs a region where the dual objective is finite and differentiable and a probabilistic condition that prevents the relevant score and derivative from vanishing together. The target keeps the actual $\sqrt\delta$ scale instead of settling for a radius-dependent positive constant (§2.2.2 and Remark 4, pp. 10–12, 39).

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$, a Borel probability measure for $P_0$, and EReal for $f_\delta$ and the inner supremum. The reused extended-real integral records the $+\infty$ and $-\infty$ cases; the Hessian is taken only where $f_\delta$ is finite on a neighborhood and its real representative is differentiable there. Quadratic Hessian forms use $\|v_\beta\|^2+v_\lambda^2$, since Lean's product norm is not the paper's Euclidean norm. The compact set $B$ is explicitly nonempty, and the positive ambiguity radius $\delta$ is quantified inside the goal so that $\delta_1$ and $\kappa_1$ are uniform in $\delta$. Theorem 3 additionally assumes $R_\beta>0$ for the proof's explicit formula for $\delta_0$: nonempty compact $B=\{0\}$ would make that formula zero. Assumption 5 already gives $R_\beta>0$ in the goal.

The goal retains Assumption 5's per-decision quantifiers. That assumption itself excludes $0\in B$: its strict score event is empty at $\beta=0$. Intermediate statements where the printed wording includes $\beta=0$ but the claim fails there state $\beta\ne0$ explicitly. Lemma 5 also states the differentiability and positive-multiplier conditions needed for its derivative and division. Proposition 9(b)'s printed strict curvature-margin inequality is corrected to the nonstrict inequality derived in its proof; its original wording is preserved in the milestone quotation. The claims are about the expectation $f_\delta$, with $\kappa_1$ independent of $\delta$, rather than a pointwise or merely convex substitute.

A complete development needs measurable extended-real integration, the matrix quadratic form and its inverse, almost-everywhere spectral bounds, differentiability under an expectation, and Hessian estimates for an optimized scalar. The transport integral, the assumptions and constants, and the multiplier bounds are intended as reusable interfaces for the companion missions. Contributions that close the listed lemmas or add the paper's omitted second-order kernel formula are within scope.

Selected references

• José Blanchet, Karthyek Murthy, and Fan Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3; DOI:10.1287/moor.2021.1178.
• José Blanchet and Karthyek Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2.

Motivation

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a decision $\beta$ under a baseline distribution $P_0$ by its worst case over all distributions $P$ that are close to $P_0$. When closeness is measured by an optimal transport cost, the worst case over this infinite-dimensional ball has a one-dimensional dual: by Theorem 1 of Blanchet, Murthy and Zhang (arXiv:1810.02403v3, Math. Oper. Res. 47(2), 2022), building on the strong duality of Blanchet and Murthy (arXiv:1604.01446),

$$\sup_{P : D_c(P_0, P) \le \delta} E_P\big[\ell(\beta^{\mathsf T}X)\big] = \inf_{\lambda \ge 0} f_\delta(\beta, \lambda).$$

The robust problem $\inf_{\beta \in B} \sup_P E_P[\ell(\beta^{\mathsf T}X)]$ thus becomes a joint minimization of the dual objective $f_\delta$ over $(\beta, \lambda)$. Whether that minimization is a convex program, and on which set the objective is finite, decides whether first-order methods such as the stochastic gradient schemes of the same paper apply at all. This mission formalizes the paper's answer, Theorem 2.

Setting

The data $X$ take values in $\mathbb{R}^d$ with law $P_0$, a Borel probability measure. A decision is a vector $\beta$ in a convex set $B \subseteq \mathbb{R}^d$, the loss is $\ell(\beta^{\mathsf T}x)$ for $\ell : \mathbb{R} \to \mathbb{R}$, and $\delta > 0$ is the transport budget.

The transport cost is the state-dependent Mahalanobis cost $c(x, x') = (x - x')^{\mathsf T}A(x)(x - x')$ for a map $A$ from $\mathbb{R}^d$ to positive definite $d \times d$ matrices. Assumption 1: $c$ is lower semicontinuous (1a), and $\rho_{\min}\|v\|^2 \le v^{\mathsf T}A(x)v \le \rho_{\max}\|v\|^2$ for $P_0$-almost every $x$, with $\rho_{\min} > 0$ (1b). Write $q_\beta(x) = \beta^{\mathsf T}A(x)^{-1}\beta$.

Assumption 2: $\ell$ is convex, its growth exponent

$$\kappa = \inf\Big\{ s \ge 0 : \sup_{u \in \mathbb{R}} \big(\ell(u) - s u^2\big) < \infty \Big\}$$

is finite, and $E_{P_0}\|X\|^4 < \infty$.

For $\gamma \in \mathbb{R}$, $\lambda \ge 0$ and $x \in \mathbb{R}^d$ define, as in display (7),

$$F(\gamma, \beta, \lambda; x) = \ell\big(\beta^{\mathsf T}x + \gamma\sqrt{\delta}\, q_\beta(x)\big) - \lambda\sqrt{\delta}\big(\gamma^2 q_\beta(x) - 1\big),$$

the robust loss $\ell_{rob}(\beta, \lambda; x) = \sup_{\gamma \in \mathbb{R}} F(\gamma, \beta, \lambda; x) \in \mathbb{R} \cup \{+\infty\}$, its set of maximizers $\Gamma^*(\beta, \lambda; x)$, and the dual objective

$$f_\delta(\beta, \lambda) = E_{P_0}\big[\ell_{rob}(\beta, \lambda; X)\big] \in \mathbb{R} \cup \{\pm\infty\}.$$

The effective domain is $\mathbb{U} = \{(\beta, \lambda) \in B \times \mathbb{R}_+ : f_\delta(\beta, \lambda) < \infty\}$, and with the threshold $\lambda_{thr}(\beta) = \kappa\sqrt{\delta}\,\operatorname{ess\,sup}_{P_0} q_\beta$ the paper sets $\mathbb{U}_1 = \{\lambda > \lambda_{thr}(\beta)\}$ and $\mathbb{U}_2 = \{\lambda \ge \lambda_{thr}(\beta)\}$ inside $B \times \mathbb{R}_+$.

Formalization targets

Goal: Theorem 2 (p. 10)

Under Assumptions 1 and 2, $f_\delta : B \times \mathbb{R}_+ \to \mathbb{R} \cup \{\infty\}$ is proper and convex: $f_\delta > -\infty$ on $B \times \mathbb{R}_+$; for each $\beta \in B$ some $\lambda \ge 0$ has $f_\delta(\beta, \lambda) < \infty$; and for $\theta_1, \theta_2 \in B \times \mathbb{R}_+$, $\alpha \in [0, 1]$,

$$f_\delta\big(\alpha\theta_1 + (1 - \alpha)\theta_2\big) \le \alpha f_\delta(\theta_1) + (1 - \alpha) f_\delta(\theta_2).$$

Milestones

1. Lemma 3 (p. 32). For each $\varepsilon > 0$ there are $C_1, C_2 > 0$, not depending on $x$, $\beta$, $\lambda$, such that whenever $\lambda \ge (\kappa + \varepsilon)\sqrt{\delta}\,q_\beta(x)$ we have $\sqrt{\delta}|g|q_\beta(x) \le 1 + C_1\varepsilon^{-1}(1 + |\beta^{\mathsf T}x|)$ for every $g \in \Gamma^*(\beta, \lambda; x)$, and $\ell_{rob}(\beta, \lambda; x) \le \lambda\sqrt{\delta} + C_2(1 + \varepsilon + \varepsilon^{-1})(1 + |\beta^{\mathsf T}x|)^2$.
2. Display (25) (p. 32). $\sup_{\Delta \in \mathbb{R}^d}\{\ell(\beta^{\mathsf T}(x + \Delta)) - \tfrac{\lambda}{\sqrt\delta}(\Delta^{\mathsf T}A(x)\Delta - \delta)\} = \ell_{rob}(\beta, \lambda; x)$.
3. Lemma 2 (p. 16). $(\beta, \lambda) \mapsto \ell_{rob}(\beta, \lambda; x)$ is convex on $B \times \mathbb{R}_+$ for every $x$.
4. Lemma 1 (p. 16). $\Gamma^* \neq \emptyset$ and $\ell_{rob}$ finite if $\lambda > \kappa\sqrt{\delta}\,q_\beta(x)$; $\Gamma^* = \emptyset$ and $\ell_{rob} = \infty$ if $\lambda < \kappa\sqrt{\delta}\,q_\beta(x)$; consequently $\mathbb{U}_1 \subseteq \mathbb{U} \subseteq \mathbb{U}_2$.

Lemma 3 is stated with constants depending only on $\varepsilon$ (and the fixed data), as its proof produces them and as the paper's later arguments integrate bound (b) over $x$.

Significance

Theorem 2 is the structural fact behind the paper's algorithms: with Theorem 1 it turns a minimax problem over probability measures into a convex minimization in $d + 1$ real variables, on which the paper's strong convexity results (Theorems 3–5) and its stochastic gradient schemes are built. Lemma 1 identifies the effective domain up to its boundary, which tells an algorithm where the dual multiplier must lie, and Lemma 3 gives the growth control of the robust loss used throughout the appendix.

The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the dual objective as an extended-real integral and of its convexity and properness, reusable by the other missions of this series (strong convexity near the optimizers, worst-case distributions, comparative statics in $\delta$), and contributions of formal proofs of the milestones and the goal.

Difficulty

The objective takes the value $+\infty$ on part of its domain: Lemma 1(b) shows that $\ell_{rob} = +\infty$ below the threshold, so the naive reading "$f_\delta$ is a real convex function" is false, and convexity must be handled for functions with values in $\mathbb{R} \cup \{\infty\}$, including the conventions $0 \cdot \infty = 0$ at the endpoints of the segment. Properness requires a bound on $\ell_{rob}$ that is integrable in $x$, so the constants of Lemma 3 must not depend on $x$; a bound that is only pointwise finite does not suffice. The identity (25) relates a supremum over $\mathbb{R}^d$ to a supremum over $\mathbb{R}$ through a change of the dual variable, and the two multipliers must be kept apart. Finally, the expectation in $f_\delta$ is an integral of an extended-real function whose measurability is not assumed but has to be derived from Assumption 1.

Formalization scope

$\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) and parameters $(\beta, \lambda)$ live in EuclideanSpace ℝ (Fin d) × ℝ. $\ell_{rob}$ is an EReal supremum; $f_\delta$ is the published ModelRiskOT.Duality.extIntegral, $\int \varphi^+\,dP_0 - \int \varphi^-\,dP_0$ with lower Lebesgue integrals. $\kappa$ is a real infimum and $\lambda_{thr}$ uses the real essential supremum; both are used only under Assumptions 1–2, which make them meaningful. Convexity of extended-real maps is written as the explicit inequality in EReal, since ConvexOn does not apply.

Standing assumptions carried by every statement: $P_0$ a probability measure, $\delta > 0$, $B$ convex (the paper's standing assumption). Conventions committed to: "for any $x$" in Lemmas 1–2 is every $x$, not almost every; Lemma 2 assumes only Assumption 1a and the convexity of $\ell$; the identity (25) is stated with the old multiplier written as $\lambda/\sqrt{\delta}$; the typo "$\beta A(x)^{-1}\beta$" in Lemma 1 is read as $\beta^{\mathsf T}A(x)^{-1}\beta$; the goal's "finite somewhere" is stated for each $\beta \in B$, so the goal is vacuous only when $B = \emptyset$. The fourth-moment condition of Assumption 2 is kept as printed.

A trivializing formalization is ruled out: "proper" is not encoded as "finite everywhere" (false by Lemma 1(b)), and pointwise convexity of $\ell_{rob}$ (Lemma 2) is a milestone, not the goal, which is about the expectation $f_\delta$.

A complete development needs: positive definite matrices and the quadratic minimization behind (25); continuity of convex functions and growth bounds; lower Lebesgue integrals of extended-real functions and their monotonicity and additivity; measurability of a supremum over $\gamma$ of continuous functions. The definitions layer is shared with the other four missions of this series. Proofs of any milestone and of the goal are welcome.

Selected references

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