Robust Optimization

Motivation

Every data-driven decision problem faces the same trap. A decision-maker estimates a risk functional $R(P,\ell) = \mathbb{E}_P[\ell(\xi)]$ from a nominal distribution $\hat P_N$ built from $N$ training samples, then optimizes a loss function $\ell$ against $\hat P_N$ instead of the unknown true distribution $P$. Because the optimizer adapts to the noise in $\hat P_N$, the in-sample risk of the optimizer systematically understates its true, out-of-sample risk — a phenomenon Smith and Winkler named the optimizer's curse (Smith & Winkler, Management Science, 2006). The remedy explored here is to hedge against a whole neighborhood of plausible distributions around $\hat P_N$, rather than trusting the point estimate. Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh's INFORMS TutORials chapter (2019) develops this neighborhood using the Wasserstein distance, and the present mission formalizes its foundational duality theory: the machinery every later result in the chapter (finite-sample guarantees, elliptical tractability, regularization) builds on.

Setting

Fix a norm $\|\cdot\|$ on a finite-dimensional real vector space $E$ (representing $\mathbb{R}^m$). For $p \in [1,\infty)$, the type-$p$ Wasserstein distance between two Borel probability measures $Q, Q'$ on $E$ is

$$W_p(Q,Q') = \left(\inf_{\pi \in \Pi(Q,Q')} \int_{E\times E} \|\xi-\xi'\|^p\, \pi(d\xi,d\xi')\right)^{1/p},$$

where $\Pi(Q,Q')$ is the set of couplings of $Q$ and $Q'$ — joint probability measures on $E \times E$ whose marginals are $Q$ and $Q'$. The optimal $\pi$ can be read as a transportation plan moving one pile of dirt ($Q$) into another ($Q'$) at minimum cost, which is why $W_p$ is also called the earth mover's distance; the underlying linear program was formalized by Kantorovich (1942) after Monge's 1781 original.

Given $N$ training samples $\hat\xi_1,\dots,\hat\xi_N$, the empirical distribution is $\hat P_N = \frac1N\sum_{i=1}^N \delta_{\hat\xi_i}$. Centered at $\hat P_N$, the Wasserstein ambiguity set of radius $\varepsilon \ge 0$ is

$$B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\},$$

where $\Xi \subseteq E$ is a closed set known to contain the support of the true distribution. The worst-case risk of a loss function $\ell$ is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} \mathbb{E}_Q[\ell(\xi)],$$

and minimizing it over a class of admissible loss functions $\mathcal{L}$ is a distributionally robust optimization problem. $\varepsilon$ measures the estimation error one insures against; a larger ambiguity set gives a more conservative (and more expensive) guarantee.

Formalization targets

Goal — Theorem 7, strong duality

$$R_{\varepsilon,p}(\hat P_N,\ell) = \inf_{\gamma \ge 0}\ \mathbb{E}_{\hat P_N}[\ell_\gamma(\xi)] + \gamma\varepsilon^p,\qquad \ell_\gamma(\xi) = \sup_{z\in\Xi} \ell(z) - \gamma\|z-\xi\|^p.$$

This is the Lagrangian dual of the worst-case risk evaluation problem, with $\gamma$ the multiplier of the Wasserstein constraint $W_p(Q,\hat P_N)\le\varepsilon$: it converts a supremum over an infinite-dimensional space of measures into a one-dimensional minimization of the Moreau-Yosida regularization $\ell_\gamma$. Every tractability result later in the chapter (finite convex reformulations, SDP relaxations) specializes this duality by choosing a loss class for which $\ell_\gamma$ is computable.

Supporting dual representations of $W_p$ — Theorems 1 and 2

$$W_p^p(Q,Q') = \sup\left\{\int \psi\,dQ' - \int \varphi\,dQ : \varphi,\psi \text{ bounded continuous},\ \psi(\xi)-\varphi(\xi') \le \|\xi-\xi'\|^p\right\}$$ $$W_1(Q,Q') = \sup_{\mathrm{Lip}(\varphi)\le 1} \int \varphi\,dQ - \int \varphi\,dQ'$$

These identify $W_p$ as a linear program's strong dual (Theorem 1) and, for $p=1$, specialize it to the Kantorovich-Rubinstein form (Theorem 2), which is what lets the worst-case-risk analysis reason about Lipschitz loss functions directly.

Upper and lower bounds — Theorems 5 and 6

$$R_{\varepsilon,p}(\hat P_N,\ell) \le R(\hat P_N,\ell) + \varepsilon\cdot\mathrm{Lip}(\ell)$$ $$R_{\varepsilon,p}(\hat P_N,\ell) \ge \sup\left\{\tfrac1N\textstyle\sum_i \ell(\hat\xi_i+\theta_i) : \hat\xi_i+\theta_i\in\Xi,\ \tfrac1N\textstyle\sum_i\|\theta_i\|^p\le\varepsilon^p\right\}$$

These are the tractable, easily-computed bracket that Theorems 7 and 10 later show is tight in important special cases.

Exact case — Theorem 10

$$\Xi = \mathbb{R}^m,\ \ell \text{ convex},\ p=1 \implies R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon\,\mathrm{Lip}(\ell)$$

Theorem 5's inequality becomes exact under convexity — the cleanest closing corollary of the duality theory, obtained from Theorem 7 by evaluating the Moreau-Yosida regularization of a convex function explicitly.

Significance

Theorem 7 is the hinge on which the entire computational program of Wasserstein distributionally robust optimization turns: every tractable reformulation in the source chapter (piecewise-concave losses via conic duality, quadratic losses via semidefinite programming, the shrinkage-estimator connection) is obtained by substituting a specific loss class into the right-hand side of Theorem 7 and showing the resulting Moreau-Yosida regularization is computable. Kuhn et al. themselves derive it as a corollary of Blanchet & Murthy (2019) and Gao & Kleywegt (2016) for the empirical case, generalized to Polish spaces by Blanchet & Murthy and Gao & Kleywegt independently — the paper cites [12] and [37] for the general statement. Formalizing it is what makes every later, more computational result in the chapter — the ones a solver is more likely to reach for next — rest on a mechanically verified foundation rather than a citation chain.

Status. The mathematical result is well established (multiple independent published proofs cited above); nothing here is open research. What this mission contributes is the first machine-checked formal statement of the duality theorem and its supporting dual representations (Theorems 1, 2, 5, 6, 10) on the Prove2Me platform — none of Wp's dual representation, the Wasserstein ambiguity set, or the worst-case risk functional exist there prior to this mission (see Formalization scope).

Difficulty

The obvious proof strategy — write down the Lagrangian of the semi-infinite program (6), swap the order of the outer supremum over $Q$ and the inner minimization over the multiplier $\gamma$, and invoke ordinary Lagrangian strong duality — fails because (6) is an infinite- dimensional linear program over measures, not a finite convex program: there is no compact feasible set or Slater point in a form that ordinary finite-dimensional duality applies to directly. The actual proof goes through the dual representation of the Wasserstein distance itself (Theorem 1, which is why it is a prerequisite milestone), reformulating the constraint $W_p(Q,\hat P_N)\le\varepsilon$ via its own dual variables and swapping the resulting sup-inf using minimax theorems for semi-infinite programs, not ordinary Lagrangian duality for finite programs.

Formalization scope

$E$ is a generic finite-dimensional real normed space (NormedAddCommGroup, NormedSpace ℝ, Borel-measurable), representing $\mathbb{R}^m$ with the paper's arbitrary fixed norm as a parameter rather than fixing the Euclidean norm. A coupling is formalized directly via MeasureTheory.Measure.map: π.map Prod.fst = Q ∧ π.map Prod.snd = Q'. Constrained infima/suprema (over couplings, over the ambiguity set, over Lipschitz test functions, over perturbation matrices) use Mathlib's guarded-binder idiom ⨅ x (_ : P x), f x, which correctly returns $\top$ (resp. $\bot$) outside the feasible set rather than a finite junk value.

Two deliberate, disclosed conventions keep the extremal-value definitions faithful without extended-real integration machinery, both recorded in MODERATION_NOTES.md:

1. worstCaseRisk and the dual representations (Theorems 1, 2) are valued in EReal, not ℝ, so an unbounded supremum is recorded as $+\infty$ rather than collapsed to Mathlib's real-valued junk value 0 on an unbounded family.
2. The goal theorem (7) and its Moreau-Yosida regularization restrict the loss function to bounded continuous $\ell$ (BoundedContinuousFunction E ℝ), narrower than the paper's general upper-semicontinuous, $\hat P_N$-integrable loss class $\mathcal{L}$ (Assumption 1). This keeps $\ell_\gamma(\xi) = \sup_{z\in\Xi}\ell(z)-\gamma\|z-\xi\|^p$ a finite real number for every nonempty $\Xi$, so the right-hand side's Bochner integral is well-posed; the milestones (Theorems 5, 6, 10) keep the more general real-valued (not necessarily bounded) loss class, since their statements do not require evaluating a pointwise supremum over $\Xi$.
3. Ξ is required closed in Theorems 5, 6 and 7, matching the paper's own standing assumption (p. 6: "we let $\Xi\subseteq\mathbb{R}^m$ be a closed set that is known to contain the support of $P$") for the whole worst-case-risk framework, which is used silently in the paper wherever a theorem takes $\Xi$ as an argument but was not carried into these theorems' own hypothesis lists in an earlier draft.
4. The goal theorem (7) additionally requires $\hat P_N$ itself supported on $\Xi$ ($\hat P_N(\Xi^c)=0$, the same "supported on $\Xi$" convention ambiguitySet uses for $Q\in\mathcal P(\Xi)$), which the paper's framework presupposes for the nominal distribution throughout §2. Combined with $\ell$ bounded, this makes $\ell_\gamma$ bounded on the full-measure set $\Xi$ (above by $\sup\ell$ unconditionally, below by $\ell(\xi)$ itself via $z=\xi$ for $\xi\in\Xi$), which is what makes the right-hand side's integral genuinely well-posed rather than liable to Mathlib's non-integrable junk value $0$.

There is no trivializing formalization risk from a vacuous hypothesis: Ξ.Nonempty and 0 < N are both required exactly where the paper's own indexing and support assumptions require them, and every extremal value uses the extended-real convention above rather than a convention that would make an inequality vacuously true.

No definition in this mission exists on the platform prior to this series (GET /theorems?q=Wasserstein, q=Kantorovich, q=optimal transport, q=coupling return only unrelated discrete/finite-type constructions); all seven definitions and six theorems are drafted fresh. WassersteinDRO.Duality.wassersteinDistance, .ambiguitySet and .worstCaseRisk are the substrate every later mission in this five-part series (Gelbrich tractability, finite-sample guarantees, regularization, shrinkage estimation) either imports directly or redefines locally per the series' reuse rule.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research, 130–166. https://doi.org/10.1287/educ.2019.0198
• Villani, C. (2009). Optimal Transport: Old and New. Springer. (Cited as [108] for Theorems 1 and 2.)
• Smith, J. E., & Winkler, R. L. (2006). The optimizer's curse: Skepticism and postdecision surprise in decision analysis. Management Science, 52(3), 311–322. https://doi.org/10.1287/mnsc.1050.0451
• Gao, R., & Kleywegt, A. J. (2016). Distributionally Robust Stochastic Optimization with Wasserstein Distance. arXiv:1604.02199.
• Blanchet, J., & Murthy, K. (2019). Quantifying Distributional Model Risk via Optimal Transport. Mathematics of Operations Research, 44(2), 565–600. https://doi.org/10.1287/moor.2018.0936

Motivation

Distributionally robust optimization (DRO) hedges a decision against every distribution within some ambiguity set around an estimated (nominal) distribution, rather than trusting the estimate exactly. When the ambiguity set is a ball of radius $\varepsilon$ around the empirical distribution $\hat P_N$ in the type-$p$ Wasserstein metric, the resulting worst-case risk problem inherits attractive statistical guarantees (Mohajerin Esfahani & Kuhn 2018) but is, in general, an optimization problem over an infinite-dimensional space of measures. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter surveys when this problem becomes computationally tractable. One route — the subject of this mission — discards everything about the nominal distribution except its mean vector and covariance matrix and replaces the Wasserstein ball with a set built only from these two moments, the Gelbrich hull. The construction is due to Gelbrich (1990), who first bounded the Wasserstein distance between two distributions using only their means and covariances.

Setting

Fix $\Xi \subseteq \mathbb{R}^m$, a nominal distribution $\hat P_N \in \mathcal{P}(\Xi)$, a radius $\varepsilon > 0$ and an exponent $p \ge 1$. The type-$p$ Wasserstein distance between two probability measures $Q, Q'$ on $\mathbb{R}^m$ is

$$W_p(Q,Q') = \Big(\inf_{\pi \in \Pi(Q,Q')} \int \|\xi-\xi'\|^p \, d\pi(\xi,\xi')\Big)^{1/p},$$

the infimum over couplings $\pi$ (probability measures on $\mathbb{R}^m \times \mathbb{R}^m$ with marginals $Q$ and $Q'$) of the $p$-th root of the expected $p$-th power of Euclidean distance. The Wasserstein ambiguity set is $B_{\varepsilon,p}(\hat P_N) = \{Q \in \mathcal{P}(\Xi) : W_p(Q,\hat P_N) \le \varepsilon\}$, and the worst-case risk of a loss function $\ell$ is $R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)]$.

Suppose $\hat P_N$ has mean vector $\hat\mu$ and covariance matrix $\hat\Sigma \in S^m_+$ (the positive semidefinite $m\times m$ matrices). The mean-covariance uncertainty set is

$$U_\varepsilon(\hat\mu,\hat\Sigma) = \Big\{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}\big[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2}\Sigma\hat\Sigma^{1/2})^{1/2}\big] \le \varepsilon^2\Big\},$$

where $\Sigma^{1/2}$ is the positive-semidefinite square root. The Gelbrich hull is $G_\varepsilon(\hat\mu,\hat\Sigma) = \{Q \in \mathcal{P}(\Xi) : (E_Q[\xi],\mathrm{Cov}_Q[\xi]) \in U_\varepsilon(\hat\mu,\hat\Sigma)\}$: the distributions on $\Xi$ whose own mean and covariance lie in $U_\varepsilon(\hat\mu,\hat\Sigma)$. An elliptical distribution $E_g(\mu,\Sigma)$ has density $f(\xi) = C \cdot \det(\Sigma)^{-1} g\big((\xi-\mu)^\top\Sigma^{-1}(\xi-\mu)\big)$ for a density generator $g$ and normalizing constant $C$; two elliptical distributions "have the same density generator" when their $g$ coincide (e.g. both Gaussian, both Student-$t_\nu$ for the same $\nu$).

Formalization targets

Goal (Theorem 13, Gelbrich hull). For every $p \ge 2$,

$$B_{\varepsilon,p}(\hat P_N) \subseteq G_\varepsilon(\hat\mu,\hat\Sigma).$$

This is an outer approximation: every distribution within $\varepsilon$ of $\hat P_N$ in Wasserstein distance has a mean and covariance inside $U_\varepsilon(\hat\mu,\hat\Sigma)$, so optimizing over the Gelbrich hull instead of the Wasserstein ball can only enlarge the feasible set, never shrink it below the truth.

Supporting results. Theorem 4 (Gelbrich bound) gives the moment-only lower bound on $W_2$ that Theorem 13 is built from, with equality for elliptical distributions sharing a generator. Proposition 1 sharpens the goal's containment to an equality on the mean-covariance projection itself, under the same two conditions ($\Xi = \mathbb{R}^m$, $\hat P_N$ elliptical). Corollary 1 propagates the goal's set containment to the risk level: $R_{\varepsilon,p}(\hat P_N,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell)$ for every $\ell$, where $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ is the Gelbrich risk.

Significance

Theorem 13 is the hinge between an intractable infinite-dimensional worst-case-risk problem and a tractable one: the paper goes on (Theorem 16, outside this mission's scope) to show that for quadratic loss functions and elliptical nominal distributions the Gelbrich risk itself equals the optimal value of a semidefinite program with two linear matrix inequality constraints — and that, under those same conditions, the Wasserstein worst-case risk, the Gelbrich risk and the SDP value all coincide. Corollary 1 is what makes the Gelbrich risk usable as a conservative surrogate even outside that special case: it upper-bounds the true worst-case risk for any loss function and any $p \ge 2$, at the cost of discarding all but first- and second-order information about the nominal distribution. Formalizing the goal and Corollary 1 gives the exact scope in which this moment-relaxation is licensed — the $p \ge 2$ restriction and the outer-approximation direction are both easy to get backwards, and this mission's Lean encoding fixes both irreversibly.

Difficulty

The obvious first argument is to prove containment pointwise: fix $Q \in B_{\varepsilon,p}(\hat P_N)$ and show its mean and covariance land in $U_\varepsilon(\hat\mu,\hat\Sigma)$. That reduces Theorem 13 to Proposition 1's containment half, which in turn reduces to the Gelbrich bound (Theorem 4) applied to the pair $(Q,\hat P_N)$ — the inequality direction of Theorem 4 suffices for containment; only the sharper equality direction (needed for Proposition 1's own equality clause) requires the elliptical hypothesis. The non-obvious step is Theorem 4 itself: bounding $W_2(Q,Q')$ below by a closed-form expression in the two distributions' first two moments only, for arbitrary $Q,Q'$ with those moments, requires an argument that survives every coupling $\pi$ — the paper's proof goes through a lower bound on the coupling's cross-covariance term via the eigenvalues of $\Sigma^{1/2}\Sigma'\Sigma^{1/2}$, not a direct manipulation of $W_2$'s definition.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m); a "distribution" is a MeasureTheory.Measure on it constrained by Q Set.univ = 1 (probability) and Q Ξᶜ = 0 (support in Ξ). The Wasserstein distance is ENNReal-valued (Definition 1's infimum over couplings, matching 01-duality's convention); the worst-case and Gelbrich risks are EReal-valued suprema restricted to loss functions integrable under the candidate distribution, avoiding Mathlib's junk value for a non-integrable Bochner integral. $\Sigma^{1/2}$ is the positive-semidefinite matrix square root, picked by choice from its defining existential and applied in this mission only to matrices hypothesized (or, per Section 2.3's standing assumption, given) positive semidefinite. Elliptical distributions (IsElliptical) are represented by the paper's own density formula (a measure equal to volume.withDensity of C·det(Σ)⁻¹·g((ξ-μ)ᵀΣ⁻¹(ξ-μ)) for some C>0), together with the mean/covariance facts every theorem in this chunk reads off directly; an earlier draft kept only the latter, under which "same density generator" held vacuously for any moment-matched pair — corrected after moderation flagged it (see STATUS.md). Because 01-duality (Wasserstein distance, ambiguity set, worst-case risk) is not yet a published mission, this chunk redefines those objects locally in its own namespace rather than importing an unpublished draft, per the series' definition-reuse policy; a future upload can retire the duplication once 01-duality is live. A formalization that dropped Theorem 4's "same density generator" condition from its equality clause, or that stated the goal's containment for all $p\ge 1$ rather than $p \ge 2$, would be trivializing or simply false — both are explicit hypotheses in the Lean statements. Matrix.PosSemidef and its Loewner order carry the $S^m_+$ constraints; no elliptical-distribution or Gelbrich-hull infrastructure exists elsewhere on the platform, so this mission's definitions are original contributions reusable by any later extension (Theorem 16/17, Lemma 1/2's SDP representations) of this series.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Gelbrich, M. (1990). On a formula for the L2 Wasserstein metric between measures on Euclidean and Hilbert spaces. Mathematische Nachrichten, 147(1), 185–203.
• Mohajerin Esfahani, P., & Kuhn, D. (2018). Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations. Mathematical Programming, 171(1), 115–166.

Motivation

A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius $\varepsilon$ by hand, and it is natural to ask what guarantee that choice actually buys: how large must $\varepsilon$ be, as a function of the sample size $N$ and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.

Setting

Fix $m \in \mathbb{N}$. Let $P$ be the unknown true distribution on $\mathbb{R}^m$ with mean vector $\mu$ and covariance matrix $\Sigma \in S^m_+$, and suppose $P$ is light-tailed: there exist $\alpha > 2$ and $A > 0$ with $E_P[\exp(\|\xi\|_2^\alpha)] \le A$. Let $\hat\xi_1,\dots,\hat \xi_N$ be $N$ independent, identically distributed samples from $P$; write $P^N$ for their joint law (the $N$-fold product measure) and $\hat\mu, \hat\Sigma$ for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution $\hat P_N = \frac{1}{N}\sum_i \delta_{\hat\xi_i}$. Recall from the Gelbrich construction the mean-covariance uncertainty set $U_\varepsilon(\hat\mu,\hat\Sigma) = \{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2} \Sigma\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2\}$, and the Gelbrich risk $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ of a loss function $\ell$ over the Gelbrich hull $G_\varepsilon(\hat\mu,\hat \Sigma)$.

Formalization targets

Milestone (Theorem 21, concentration inequalities II). There is $c > 1$, depending on $P$ only through $\mu,\Sigma,\alpha,A,m$ (not on any finer feature of $P$), such that for every $\eta \in (0,1]$,

$$P^N\big[(\mu,\Sigma) \in U_\varepsilon(\hat\mu,\hat\Sigma)\big] \ge 1-\eta \quad \text{whenever} \quad \varepsilon \ge \varepsilon_N(\eta) := \frac{\log(c/\eta)}{\sqrt N}.$$

Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every $\eta \in (0,1)$ and $\varepsilon \ge \varepsilon_N(\eta)$,

$$P^N\Big\{R(P,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell) \;\; \forall \ell \in L\Big\} \ge 1-\eta.$$

With probability at least $1-\eta$ over the draw of the training sample, the Gelbrich risk computed from that sample upper-bounds the true risk of every admissible loss function simultaneously — not just of one fixed $\ell$ chosen in advance. (The paper's part (b), the analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer $\ell^\star$ of the Gelbrich risk minimization problem, is not formalized in this mission — see Formalization scope.)

Significance

Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, $\varepsilon_N(\eta) = O(N^{-1/2})$, is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with $m$. Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of $\varepsilon_N(\eta)$ and the precise sense in which $c$ is "distribution-free" given $(\mu,\Sigma,\alpha,A,m)$ — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).

Difficulty

The central formalization difficulty is not proving the theorems (both are left as sorry in this draft) but stating the existential constant $c$ correctly. The paper says $c$ "depends on $P$ only through $\mu,\Sigma,\alpha,A,m$" — informally, a promise that $c$ is uniform across every distribution $P$ sharing those five parameters, not merely that some $c$ exists for each $P$ separately (a vacuously true, much weaker statement obtained by naively quantifying $c$ after $P$). The correct encoding places $\exists c$ before the universal quantifier over $P$: for fixed $(\mu,\Sigma,\alpha,A,m)$, one $c$ must work for every $P$ with that mean, covariance, and tail bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee into a triviality (FAITHFULNESS_TRAPS.md trap 8).

Formalization scope

Distributions live on EuclideanSpace ℝ (Fin m); $P^N$, the law of $N$ iid samples, is the $N$-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "$P^N[\text{event}] \ge 1-\eta$" is that product measure's mass on the event set. All risk and uncertainty-set definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull, gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor 02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once those missions are live. The existential constant c is placed before the universal quantifier over P in both theorems, exactly capturing "depends on P only through µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent optimization problem), which is additional infrastructure this mission's time budget did not cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching Assumption 1 (p. 9); both were added after moderation found the goal's original statement, without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension- dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its downstream guarantees and the asymptotic-consistency results) are out of scope for this mission, which targets the Gelbrich-risk branch (Theorems 21/22) specifically.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Fournier, N., & Guillin, A. (2015). On the rate of convergence in Wasserstein distance of the empirical measure. Probability Theory and Related Fields, 162(3), 707–738.
• Gao, R., & Kleywegt, A. J. (2023). Distributionally robust stochastic optimization with Wasserstein distance. Mathematics of Operations Research, 48(2), 603–655.

Motivation

Regularization — adding a penalty on model complexity to an empirical risk minimization objective — is one of the oldest and most reliably effective tools in statistical learning: ridge regression, LASSO, and margin-based support vector machines all fit this template. For decades the regularization weight and penalty function were chosen heuristically or by cross-validation, with only asymptotic or worst-case generalization bounds explaining why they help. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter on Wasserstein distributionally robust optimization (DRO) gives regularization a different, non-asymptotic justification: a decision rule that is robust to adversarial perturbations of its training data, measured in Wasserstein distance, is exactly a regularized empirical risk minimizer — no approximation, no asymptotics. This mission formalizes the general form of that equivalence, Theorem 10 (p. 14), which underlies every regularization-by-robustification result the chapter derives for classification and regression alike.

Setting

Fix a normed space $\Xi = \mathbb{R}^m$, a convex loss function $\ell : \Xi \to \mathbb{R}$, a radius $\varepsilon \ge 0$, and $N$ training samples $\hat\xi_1,\dots,\hat\xi_N \in \Xi$ ($N \ge 1$). The empirical distribution is $\hat P_N = \frac{1}{N}\sum_{i=1}^N \delta_{\hat\xi_i}$. The worst-case risk of $\ell$ at radius $\varepsilon$ (eq. (6), p. 6) is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)],$$

where $B_{\varepsilon,p}(\hat P_N)$ is the type-$p$ Wasserstein ball of radius $\varepsilon$ around $\hat P_N$ (Definition 1, p. 3) — the set of probability measures on $\Xi$ within Wasserstein distance $\varepsilon$ of the empirical distribution, under a norm $\|\cdot\|$ on $\Xi$ and its transportation exponent $p$. The Lipschitz modulus $\mathrm{Lip}(\ell) = \sup_{\xi\ne\xi'} \frac{|\ell(\xi)-\ell(\xi')|}{\|\xi-\xi'\|}$ (possibly $+\infty$) measures how fast $\ell$ can grow.

Formalization targets

Goal (Theorem 10, convex loss and $p=1$). If $\ell$ is convex and $p=1$, then the worst-case risk of $\ell$ over the type-1 Wasserstein ball around the empirical distribution coincides with the Lipschitz-regularized empirical loss:

$$R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon \cdot \mathrm{Lip}(\ell),$$

where $R(\hat P_N,\ell) = \frac{1}{N}\sum_{i=1}^N \ell(\hat\xi_i)$ is the ordinary empirical risk. The left side is the worst-case expected loss under adversarial perturbations of the training data of bounded aggregate Wasserstein cost; the right side is the ordinary empirical risk plus a regularization term proportional to the perturbation radius $\varepsilon$ and the loss's own Lipschitz modulus — no approximation, an exact equality for every convex $\ell$.

Significance

This is the single result underlying every specific regularization-by-robustification corollary the chapter derives — the $\ell_2$-regularized SVM and its $\ell_1$/$\ell_\infty$ variants, regularized logistic regression, and the regression analogue with a Lipschitz loss (Proposition 3) — because each of those is obtained by substituting a specific convex, Lipschitz loss (hinge, logloss, a linear-model margin loss) for the general $\ell$ here and reading off $\mathrm{Lip}(\ell)$ in closed form. Theorem 10 is exact ($p=1$, Ξ = R^m) precisely because a type-1 transportation cost is dual to the Lipschitz modulus (a consequence of the Kantorovich- Rubinstein duality this book's earlier duality theorems establish), whereas the corresponding statement for $p \ge 2$ (Theorem 11 elsewhere in the chapter) needs a strictly stronger hypothesis on $\ell$. Formalizing Theorem 10 fixes, machine-checkably, the exact scope of the equivalence — which losses qualify (convex, no boundedness or smoothness needed), which transportation exponent is required ($p=1$, not any $p\ge1$), and that the equality is exact, not an upper or lower bound — the single fact every classification- and regression-specific robustification corollary in the chapter cites without re-deriving.

Difficulty

The natural first attempt treats the worst-case risk as an instance of the general finite convex reduction (Theorem 8, which needs $\ell$ or a related concave/convex-conjugate structure and applies for a general norm exponent $p,q$ with $1/p+1/q=1$) and specializes it to $p=1$. This is not the paper's own route for Theorem 10: at $p=1$ the dual exponent $q=\infty$, and the general finite-convex-program reduction (11) degenerates in a way that is more naturally derived directly from the type-1 Wasserstein distance's own dual (Kantorovich-Rubinstein) representation — a Lipschitz test function pairs exactly with a type-1 transportation cost, which is why the answer is Lipschitz-regularization and not some other penalty. The Lean statement records only the final equality (the proof itself, via Theorem 8 or the direct Kantorovich-Rubinstein route, is left as sorry, as required for a draft item), but the choice of which milestones would support that proof is exactly this: the type-1/Lipschitz-modulus duality is a structurally different argument from the finite-convex-program machinery Theorem 8 needs for other $p$, which is why this chapter's earlier draft mistakenly tried to reach a specialization of Theorem 10 (Proposition 2, restated for a labeled, $\kappa=\infty$ ambiguity set) through a finite-atom shortcut that does not actually capture the general type-1 ball Theorem 10's own proof needs — see Formalization scope.

Formalization scope

$\Xi$ is EuclideanSpace ℝ (Fin m) (fixed to Set.univ, matching the theorem's own "Ξ = R^m" hypothesis) with an arbitrary fixed norm as a type-class parameter, not specialized to Euclidean. The worst-case risk, Wasserstein distance, ambiguity set, nominal risk, empirical distribution and Lipschitz modulus are all redefined locally in this chapter's own namespace, verbatim restatements of 01-duality's own drafts of the same objects (identical EReal/ENNReal/Integrable conventions), because 01-duality is not yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once it is live. hN : 0 < N excludes the empty-sample case the paper's own "N training samples" presupposes; hℓ : Integrable ℓ (empiricalDistribution ξhat) guards the empirical risk's Bochner integral (automatically satisfied under any real-valued ℓ since the empirical distribution is a finite convex combination of Dirac masses, but stated explicitly rather than assumed silently). No constant is pinned to a numeral. This mission originally targeted Proposition 2 (regularization by robustification for classification, p. 25), a specialization of Theorem 10 to a labeled, κ=∞ input-output ambiguity set — but that draft's κ=∞ ambiguity set restricted admissible perturbations to a finite family of exactly N atoms, each sample's entire mass moving as one indivisible unit, which is a strict, non-faithful subset of the true κ=∞ Wasserstein ball (splitting a sample's mass across several destinations is a legitimate, and for a convex loss strictly more powerful, perturbation by Jensen's inequality). This made the goal theorem false for at least one of the three loss functions (Table 1) the mission itself certified as covered (logloss), not merely narrower than the paper's claim — moderation caught this and required either a faithful general-ambiguity-set reformulation or retargeting the goal. This mission takes the latter: Theorem 10 itself, already correctly and generally stated using the unrestricted Wasserstein ball throughout, is now the goal, with no further milestone (no other numbered result in this chunk's scope is needed for Theorem 10's own statement beyond the shared definitions above). A future mission in this series can revisit Proposition 2/3 with a properly general labeled ambiguity set once that construction (label-pinned marginal plus an aggregate coupling condition on the input coordinate, rather than a finite atom family) is built.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Shafieezadeh-Abadeh, S., Esfahani, P. M., & Kuhn, D. (2015). Distributionally robust logistic regression. Advances in Neural Information Processing Systems, 28.
• Blanchet, J., Kang, Y., & Murthy, K. (2019). Robust Wasserstein profile inference and applications to machine learning. Journal of Applied Probability, 56(3), 830–857.

Motivation

Minimum mean square error (MMSE) estimation — predicting a signal $x$ from a noisy observation $y$ by minimizing expected squared prediction error — underlies linear systems theory, linear regression, Kalman filtering, and multiple-input multiple-output signal processing. Its classical solution assumes the joint distribution of $(x,y)$ is known exactly; in practice it is estimated from data, and the estimator inherits sampling error and model risk. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter shows that hedging the MMSE objective against every distribution in a Wasserstein ball around the empirical distribution — an infinite-dimensional worst case over an intractable set of measures, a priori — collapses to a tractable, finite-dimensional convex semidefinite program (Theorem 25, p. 29), building on the Gelbrich-hull machinery of Section 2.3. This mission formalizes that reduction.

Setting

Fix $m_x, m_y \in \mathbb{N}$ and let $\xi = (x,y) \in \mathbb{R}^{m_x} \times \mathbb{R}^{m_y}$ be a random vector: $x$ the signal to be estimated, $y$ the observation. An estimator is a measurable function $\psi : \mathbb{R}^{m_y} \to \mathbb{R}^{m_x}$; write $\Psi$ for the family of all estimators. The distribution of $\xi$ is only known to lie in a type-2 Wasserstein ball $B_{\varepsilon,2}(\hat P_N)$ centered at an elliptical nominal distribution $\hat P_N = E_g(\hat\mu,\hat\Sigma)$ with nominal mean $\hat\mu \in \mathbb{R}^m$ ($m=m_x+m_y$), nominal covariance $\hat\Sigma \in S^m_+$, and density generator $g$. The distributionally robust MMSE estimation problem is

$$\inf_{\psi \in \Psi} \sup_{Q \in B_{\varepsilon,2}(\hat P_N)} E_Q\big[\|x-\psi(y)\|_2^2\big]. \tag{35}$$

Writing $\hat\Sigma = \begin{pmatrix}\hat\Sigma_{xx}&\hat\Sigma_{xy}\\\hat\Sigma_{yx}& \hat\Sigma_{yy}\end{pmatrix}$ blockwise, the nonlinear convex SDP

$$\max_S f(S) = \mathrm{Tr}[S_{xx} - S_{xy}S_{yy}^{-1}S_{yx}] \quad \text{s.t.} \quad S = \begin{pmatrix}S_{xx}&S_{xy}\\S_{yx}&S_{yy}\end{pmatrix} \succeq 0,\; S_{xx} \succeq 0,\; S_{yy} \succeq 0,\; \mathrm{Tr}[S+\hat\Sigma-2(\hat\Sigma^{1/2}S\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2,\; S \succeq \lambda_{\min}(\hat\Sigma) I \tag{36}$$

is the finite-dimensional relaxation the chapter builds toward.

Formalization targets

Goal (Theorem 25, distributionally robust MMSE estimator). If $\hat\Sigma \succ 0$, then the optimal value of problem (35) equals the optimal value of SDP (36). Moreover, if $S^\star$ is optimal in (36) with $S^\star_{yy}$ invertible, then the affine function

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

attains the outer infimum of (35) — it is a distributionally robust MMSE estimator, exhibited in closed form from an SDP optimizer.

Significance

Theorem 25 reduces an a priori infinite-dimensional, worst-case functional optimization problem (an infimum over all measurable estimators of a supremum over all distributions within a Wasserstein ball) to a finite convex program with one linear matrix inequality, one Loewner-order lower bound, and one trace/matrix-square-root constraint — solvable in polynomial time, with the optimal estimator recovered in closed form from the SDP's optimal block matrix. It shows that robustifying MMSE estimation against distributional ambiguity does not sacrifice tractability: the resulting estimator remains affine, the same functional form as the classical (non-robust) best linear unbiased estimator, only with its coefficients drawn from a regularized covariance estimate rather than the raw sample covariance. Formalizing it fixes, machine-checkably, the exact shape of that regularization — which SDP constraints are load-bearing (the Loewner lower bound in particular rules out a numerically unstable near-singular $S_{yy}$) and which conditions ($\hat\Sigma \succ 0$, $S^\star_{yy}$ invertible) the closed-form estimator formula actually needs.

Difficulty

The paper's own remark (p. 29) names the two nontrivial steps: first, "establishing a minimax theorem for (35) and exploiting the properties of elliptical distributions" to show the outer infimum is attained by an affine estimator — a priori (35) ranges over all measurable $\psi$, and there is no obvious reason the worst case forces linearity. Second, "combining this structural insight with Theorem 16" (the SDP-representability result for indefinite quadratic losses under an elliptical nominal distribution, itself a nontrivial closed-form reduction of an infinite-dimensional worst-case risk) to convert the now-restricted problem over affine estimators into the finite SDP (36). Neither step is a routine consequence of the ambiguity-set definitions alone; each requires structural facts about elliptical distributions and quadratic losses proved earlier in the chapter.

Formalization scope

The signal-observation space is EuclideanSpace ℝ (Fin mx ⊕ Fin my), with $x$ and $y$ recovered as the two summand projections; the block matrix $S$ is Matrix (Fin mx ⊕ Fin my) (Fin mx ⊕ Fin my) ℝ, and Matrix.toBlocks₁₁/toBlocks₁₂/toBlocks₂₁/toBlocks₂₂ give its four blocks. The constraint "$S_{xy}=S_{yx}^\top$" is not stated as a separate hypothesis: it follows automatically once $S$ is symmetric (implied by S.PosSemidef), so encoding the feasible set from a single symmetric S rather than four independently-quantified blocks makes it structurally impossible to drop — see pitfall 4 of BRIEF.md. The outer infimum of problem (35) ranges only over measurable $\psi$ (Measurable ψ on the binder), matching the paper's own definition of $\Psi$ as "the family of all possible measurable estimators" (p. 29) exactly. λ_min(Σ̂) is taken as a hypothesis parameter characterized by the two properties that make it the minimum ("≤ every eigenvalue of Σ̂, and attained by some eigenvalue"), rather than invoking a specific Mathlib min-eigenvalue API by name. S_{yy}⁻¹ uses the ordinary matrix inverse (junk zero matrix when singular), matching the paper's literal notation; S^\star_{yy} invertible is stated as an added hypothesis, not present verbatim on the page, because the paper leaves the formula's well-definedness implicit — disclosed per pitfall 5 rather than silently assumed away. The paper's own "which is always solvable" clause is not asserted: Theorem 25 states, as part of itself, that SDP (36) attains its maximum (an unconditional existence claim for an optimal $S^\star$); this formalization states only the conditional consequences of such an $S^\star$ existing, not that one does — proving or asserting solvability is out of this mission's scope, so the Lean statement is strictly weaker than Theorem 25's own conclusion on this point, disclosed rather than silently dropped. All risk-style suprema are EReal-valued and Integrable-guarded, matching the series' convention. No milestone theorem is included: the paper's own proof sketch derives (33)'s and by extension (36)'s SDP "via Theorem 16", but Theorem 16 (indefinite quadratic loss and $p=2$, eq. 23) was itself judged too heavy to state faithfully in 02-gelbrich's time budget and is not redefined here either — see STATUS.md. Theorem 24 (the Wasserstein shrinkage estimator, this chapter's originally recommended goal) is out of scope: its closed-form eigenvalue transformation (eq. 34a/34b) requires transcribing nested square roots from a rendered PDF page that this session's time budget did not allow verifying to the standard the brief demands (pitfall 1); the brief's own documented fallback to Theorem 25 was taken instead.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Nguyen, V. A., Shafieezadeh-Abadeh, S., Yue, M.-C., Kuhn, D., & Wiesemann, W. (2021). Optimistic distributionally robust optimization for nonparametric likelihood approximation. Advances in Neural Information Processing Systems, 32.
• Shafieezadeh-Abadeh, S., Nguyen, V. A., Kuhn, D., & Mohajerin Esfahani, P. (2018). Wasserstein distributionally robust Kalman filtering. Advances in Neural Information Processing Systems, 31.

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$, finite on $(0,\infty)$, and satisfies $\phi(1)=0$; the value $\phi(0)$ may be $+\infty$. Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

$$I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),$$

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$, a function with values in $\mathbb R\cup\{+\infty\}$.

Fix $a\in\mathbb R^n$, $B\in\mathbb R^{n\times m}$ with columns $b_i$, $\beta\in\mathbb R$, $C\in\mathbb R^{k\times m}$ with columns $c_i$, $d\in\mathbb R^k$, a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$. The uncertainty region is

$$U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},$$

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$. A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

$$(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}$$

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$. Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

$$a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}$$

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$. The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$:

1. Closing identity. For $\lambda\ge0$, $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$, with the convention above at $\lambda=0$.
2. Eq. (15). For $q>0$ and $\lambda\ge0$,

$$g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).$$

3. Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$, $\eta\ge0$. This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$, where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$. The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$, and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$, the conjugate may be $+\infty$, and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

• Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
• $\phi$ is ℝ → EReal, never $-\infty$, finite on $(0,\infty)$, with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
• $I_\phi(p,q)$, $\phi^*$, $(\lambda\phi)^*$, $L$, $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$. The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$, and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
• The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$.
• $m$ and $k$ may be $0$.

Corrected slip. The paper's standing assumption is $q\ge0$. The third equality of (15) substitutes $p_i=q_it$, which needs $q_i>0$, and Theorem 1 is false for $q\ge0$: with $m=k=2$, $n=1$, $\phi(t)=|t-1|$, $q=(1,0)$, both columns of $C$ equal to $(1,-1)^\top$, $d=(1,-1)$, $a=0$, $B=(0\ \ 1)$, $x=1$, $\rho=1$, $\beta=0$, the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$, $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$. The hypothesis $q\in U$ (the paper's "such that $q\in U$") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$, a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$-self-concordant ($\kappa\ge0$) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

$$\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},$$

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$-th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$. Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

$$\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},$$

and its logarithmic barrier (35) is

$$\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y$$

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$, with $h_1$ along $s$ and $h_2$ along $y$, and $h\in\mathbb R^3$ for $\varphi_B$.

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$,

$$|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}$$

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$-self-concordant on $F_f$.

Milestones (the displayed steps of the proof)

1. Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$.
2. The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$.
3. Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$:

$$\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.$$

4. Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$, then $\varphi_B$ is $(1+\beta/3)$-self-concordant on $F_f$.

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$. A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$.

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$, which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$, together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$. The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$, fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$. A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$. Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$, but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

• "$f:\mathbb R^+\to\mathbb R$" is read as $f$ convex on the open half-line $(0,\infty)$; the Burg case $f=-\log$ is undefined at $0$, and $f$ is only evaluated at $s/y$ with $s,y>0$.
• $f$ is assumed $C^3$ on $(0,\infty)$. The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$.
• The printed third-differential display ends in $s^3h_x^3/y^5$; the correct term is $s^3h_2^3/y^5$, and the Lean statement uses it. The milestone text keeps the printed version.
• Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$", which is false for $\beta<0$: with $f\equiv0$, (36) holds for every $\beta$ and $\beta=-3$ would give a $0$-self-concordant $-\ln z-\ln s-\ln y$. The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$, the domain is exactly $F_f$ (not a subset such as $\emptyset$), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
• Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791