Robust Optimization

Motivation

In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.

The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.

Setting

Let the uncertain vector $\tilde u$ take values in $\mathbb R^d$. A probability law $P$ belongs to the moment confidence region $\mathcal P^{CS}$ when it is supported in the Euclidean ball of radius $R$, its mean $m_P$ is within $\Gamma_1$ of an estimate $\hat\mu$, and its covariance $S_P$ is within $\Gamma_2$ of an estimate $\hat\Sigma$ in Frobenius norm. The covariance is $S_P=\mathbb E_P[\tilde u\tilde u^\top]-m_Pm_P^\top$. The thresholds $\Gamma_1,\Gamma_2$ are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).

For a vector $v$, Value at Risk $\operatorname{VaR}^{P}_{\varepsilon}(v)$ is the smallest threshold $t$ for which $P(\tilde u^\top v\le t)\ge1-\varepsilon$. The support function of a set $\mathcal U$ is $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$. The authors construct the set

$$\mathcal U^{CS}_{\varepsilon} =\{\hat\mu+y+C^\top w:\|y\|_2\le\Gamma_1,\ \|w\|_2\le\sqrt{1/\varepsilon-1}\}, \qquad C^\top C=\hat\Sigma+\Gamma_2 I.$$

Here $0<\varepsilon<1$ is the allowed violation probability, $I$ is the identity matrix, and $C$ is a matrix factor of the adjusted covariance. The estimates and $C$ stay fixed while $\varepsilon$ varies. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization targets

The first milestone bounds the quantile for every law in the moment region:

$$\operatorname{VaR}^{P}_{\varepsilon}(v)\le \hat\mu^\top v+\Gamma_1\|v\|_2+ \sqrt{\frac{1-\varepsilon}{\varepsilon}} \sqrt{v^\top(\hat\Sigma+\Gamma_2I)v} \quad(P\in\mathcal P^{CS}).$$

The second milestone evaluates the two linear maxima over the Euclidean balls in $\mathcal U^{CS}_{\varepsilon}$ and identifies $\|Cv\|_2$ with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals $\delta^*(v\mid\mathcal U^{CS}_{\varepsilon})$ for every $v$, while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in $(v,t)$ and in $\varepsilon$ for $0<\varepsilon<3/4$. Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).

Significance

The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.

The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.

Difficulty

A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor $\sqrt{(1-\varepsilon)/\varepsilon}$ is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization scope

Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in $\mathcal P^{CS}$ secures finite first and second moments; no density is assumed. The goal fixes $R\ge0$, $\Gamma_1,\Gamma_2\ge0$, $0<\varepsilon<1$, and $C^\top C=\hat\Sigma+\Gamma_2I$. This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on $\hat\Sigma$ is unnecessary. The matrix need not be triangular because (35) and its support depend on $C^\top C$. The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.

Theorem 10's sampling claim is represented by its deterministic criterion for each $P\in\mathcal P^{CS}$. The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over $\mathcal P^{CS}$, yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the $3/4$ convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.

Selected references

• D. Bertsimas, V. Gupta and N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised in Mathematical Programming 167 (2018), 235–292. arXiv preprint.
• J. Shawe-Taylor and N. Cristianini, Estimating the Moments of a Random Vector with Applications, 2003. University of Southampton ePrint.
• G. C. Calafiore and L. El Ghaoui, On Distributionally Robust Chance-Constrained Linear Programs, Journal of Optimization Theory and Applications 130 (2006), 1–22. DOI.

Motivation

Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.

Setting

A single item is ordered at a single installation over periods $k = 0, \dots, T-1$. The stock at the beginning of the horizon is $x_0$. Orders $u_k \ge 0$ arrive immediately, demand $w_k$ is subtracted, and excess demand is backlogged, so the stock at the end of period $k$ is

$$x_{k+1} = x_0 + \sum_{i=0}^{k} (u_i - w_i).$$

The demand of period $k$ is uncertain: $w_k = \bar w_k + \hat w_k z_k$ with a nominal demand $\bar w_k$, a maximal deviation $\hat w_k \ge 0$ and a scaled deviation $z_k \in [-1, 1]$. A budget of uncertainty $\Gamma_k$ limits the total scaled deviation up to period $k$. The budgets satisfy $0 \le \Gamma_0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

Each period costs $C(u_k) + R(x_{k+1})$. The purchasing cost is $C(u) = K + cu$ for $u > 0$ and $C(0) = 0$, with $c > 0$ and $K \ge 0$. The holding/shortage cost is $R(x) = \max(hx, -px)$, with $h \ge 0$ and $p > c$. The nominal problem with demand $w$ minimizes $\sum_{k<T} (C(u_k) + R(x_{k+1}))$ over $u \ge 0$ for a fixed demand sequence $w$.

For each $k$, $A_k$ is the optimal value of the linear program

$$A_k = \max\Big\{\sum_{i=0}^{k} \hat w_i z_i \;:\; \sum_{i=0}^{k} z_i \le \Gamma_k,\ 0 \le z_i \le 1\Big\} \qquad (13)$$

It is the worst-case deviation of the cumulative demand up to $k$ from its nominal value, with $A_{-1} = 0$. Write $\bar x_{k+1} = x_0 + \sum_{i\le k}(u_i - \bar w_i)$ for the nominal stock. The robust formulation (14) minimizes $\sum_{k<T} (C(u_k) + y_k)$ over $(u, y, q, r)$ subject to the following constraints for every $k < T$:

• $u_k \ge 0$, $q_k \ge 0$, and $r_{ik} \ge 0$, $q_k + r_{ik} \ge \hat w_i$ for $i \le k$;
• $y_k \ge h(\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$;
• $y_k \ge p(-\bar x_{k+1} + q_k\Gamma_k + \sum_{i\le k} r_{ik})$.

The variables $q, r$ are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period $k$ for every demand whose scaled deviations satisfy $|z_i| \le 1$ and $\sum_{i \le k}|z_i| \le \Gamma_k$.

Formalization targets

Goal: Theorem 3.2 (a), (b), (d)

Let the modified demand be

$$w'_k = \bar w_k + \frac{p-h}{p+h}\,(A_k - A_{k-1}). \qquad (20)$$

Write $N_{w'}(u)$ for the nominal cost of $u$ under demand $w'$. Then:

1. For every $u \ge 0$, the minimum of the objective of (14) over the feasible $(y, q, r)$ is attained and equals

$$N_{w'}(u) + \frac{2ph}{p+h}\sum_{k=0}^{T-1} A_k.$$

2. $u$ is the order part of an optimal solution of (14) if and only if $u$ is optimal for the nominal problem with demand $w'$.
3. The optimal cost of (14) is the optimal nominal cost under $w'$ plus $\frac{2ph}{p+h}\sum_k A_k$.
4. If $K = 0$ and $w'_k \ge 0$, the order-up-to policy with levels $S_k = w'_k$ is robust-optimal.

Milestones

The milestones are the steps of the paper's proof, in order:

• LP (13) and its dual are attained with the common value $A_k$.
• The constraints of (14) are the robust counterpart of the $k$-th holding/shortage pair (10)–(11).
• For fixed orders, the value of (14) is the sum (21).
• The modified stock (22) satisfies $x'_{k+1} = \bar x_{k+1} - \frac{p-h}{p+h}A_k$.
• The max identity (23): $\max(h(\bar x+A), p(-\bar x+A)) = \max(hx', -px') + \frac{2ph}{p+h}A$.
• Lemma 3.1(b): for nonnegative demand, the nominal problem without fixed cost is solved by ordering up to $S_k = w_k$.
• Remark 1: $A_{k-1} \le A_k$, so $w'_k \ge \bar w_k$ when $p \ge h$.
• Remark 3: under i.i.d. demand, $A_k = \hat w\Gamma_k$, which gives the closed-form thresholds.

Significance

The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by $\frac{p-h}{p+h}(A_k - A_{k-1})$, upward when shortage is more expensive than holding. The extra cost $\frac{2ph}{p+h}\sum_k A_k$ quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).

The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:

• the budgeted robust counterpart of a pair of piecewise-linear constraints;
• the duality of the fractional knapsack LP (13);
• the optimality of base-stock orders for a deterministic backlogged inventory problem.

Difficulty

The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and $h, p \ge 0$ so that the cost is monotone in $A_k$. The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a $T$-period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.

Formalization scope

All data are real numbers and sequences are ℕ → ℝ; only indices $k < T$ matter. stock w u k denotes $x_{k+1}$, the stock at the end of period $k$. The standing assumptions of §3.1 are fields of the model:

• $c > 0$, $K \ge 0$, $h \ge 0$, $p > c$;
• $\hat w_k \ge 0$;
• $\Gamma_0 \ge 0$ and $\Gamma_k \le \Gamma_{k+1} \le \Gamma_k + 1$.

The conventions and corrections are:

• Fixed cost. The paper writes it with binary variables and a big-$M$ constraint. Here it is the indicator $C(u_k)$ in the objective, as in the paper's own (21).
• "Optimal". It always means minimality over all feasible points.
• The policy. It is the order sequence chosen at time 0.
• $A_k$. It is the value of (13), as in Remark 1 after the theorem, not "the optimal $q^*, r^*$ of (14)", which need not be unique.
• The robust formulation. (14) is formalized as printed: the $k$-th constraint pair is protected by the budget $\Gamma_k$ alone, not by the intersection of all budgets up to $k$.
• Sign slip. The page's $x_{k+1} = \bar x_{k+1} + \sum \hat w_i z_i$ is a sign slip for $\bar x_{k+1} - \sum \hat w_i z_i$. The formal statements use the correct sign; the result is unaffected because the deviation set is symmetric.
• Part (b). It is stated under $w'_k \ge 0$. As printed it fails when $p < h$ makes $w'$ negative, for example $T = 2$, $\bar w = \hat w = (10, 0)$, $\Gamma = (0, 1)$, $c = 1$, $h = 4$, $p = 2$, $x_0 = 0$. Lemma 3.1(b) carries the matching hypothesis of nonnegative demand.
• Remark 3. It adds $\Gamma_0 \le 1$.
• Remark 1. Its inequalities are weak.
• Not stated. The (s, S) clause of (a) and part (c) are excluded. They rest on a stochastic theorem cited from Bertsekas (1995) and on thresholds stated through the optimal ordering times.

A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables $y, q, r$, and $A_k$ is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.

Selected references

• D. Bertsimas, A. Thiele, A Robust Optimization Approach to Inventory Theory, Operations Research 54(1):150–168, 2006. https://doi.org/10.1287/opre.1050.0238
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1):35–53, 2004. https://doi.org/10.1287/opre.1030.0065
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. 1, Athena Scientific, 1995.

Motivation

Many statistical parameters are defined implicitly, as the root $\theta_*$ of an estimating equation $\mathbb E[h(W, \theta_*)] = \mathbf 0$: a mean, a quantile, a regression coefficient, the minimizer of an expected loss. Owen's empirical likelihood builds confidence regions for such parameters by asking how far the empirical distribution of the data must be reweighted before the equation holds, and the profile of that distance has a chi-squared limit (Owen, Empirical Likelihood, 2001).

Blanchet, Kang and Murthy replace reweighting by transport: they measure how much the data must be moved, in the sense of optimal transport, before the equation holds. The resulting Robust Wasserstein Profile (RWP) function plays the role of the empirical-likelihood profile, and its value at the true parameter is exactly the smallest radius of a Wasserstein ball around the data that contains a distribution satisfying the estimating equation. Its asymptotic law is therefore what is needed to choose the radius of Wasserstein distributionally robust estimators, such as the square-root LASSO and regularized logistic regression, in a data-driven way (arXiv:1610.05627, §§1, 3, 4). This mission formalizes the paper's main limit theorem, Theorem 3.

Setting

Let $c : \mathbb R^m \times \mathbb R^m \to [0, \infty]$ be a cost. The optimal transport cost between probability laws $P$ and $Q$ on $\mathbb R^m$ is

$$D_c(P, Q) = \inf\{ \mathbb E_\pi[c(U, W)] : \pi_U = P,\ \pi_W = Q \},$$

the infimum over all joint laws $\pi$ of a pair $(U, W)$ with the given marginals (Eq. (7)). In this mission $c(u, w) = \|w - u\|_q^\rho$ with $\rho \ge 1$ and $q \in (1, \infty]$, and $p$ denotes the conjugate exponent, $1/p + 1/q = 1$.

Let $h : \mathbb R^m \times \mathbb R^l \to \mathbb R^r$ be an estimating function, and let $W, W_1, W_2, \dots$ be i.i.d. random vectors in $\mathbb R^m$ with $\mathbb E[h(W, \theta_*)] = \mathbf 0$. With $\mathbb P_n$ the empirical distribution of $W_1, \dots, W_n$, the RWP function is

$$R_n(\theta) = \inf\{ D_c(P, \mathbb P_n) : \mathbb E_P[h(W, \theta)] = \mathbf 0 \}. \qquad (16)$$

Write $D_w h(w, \theta_*)$ for the $r \times m$ Jacobian of $w \mapsto h(w, \theta_*)$, and $\|\zeta^T D_w h(w, \theta_*)\|_p$ for the $\ell_p$ norm of the row vector $\zeta^T D_w h(w, \theta_*) \in \mathbb R^m$, $\zeta \in \mathbb R^r$. The assumptions are:

• A1) $c(u, w) = \|u - w\|_q^\rho$, $\rho \ge 1$;
• A2) $\mathbb E[h(W, \theta_*)] = \mathbf 0$ and $\mathbb E\|h(W, \theta_*)\|_2^2 < \infty$;
• A3) $h(\cdot, \theta_*)$ is continuously differentiable;
• A4) for every $\zeta \ne 0$, $\mathbb P(\|\zeta^T D_w h(W, \theta_*)\|_p > 0) > 0$.

A sequence $X_n$ is asymptotically stochastically bounded by $X$, written $X_n \lesssim_D X$, if $\limsup_n \mathbb E[f(X_n)] \le \mathbb E[f(X)]$ for every continuous, bounded, non-decreasing $f$.

Formalization targets

Goal: Theorem 3 (p. 15)

Let $H \sim \mathcal N(\mathbf 0, \mathbb E[h(W, \theta_*) h(W, \theta_*)^T])$. Under A1)–A4),

$$n^{\rho/2} R_n(\theta_*; \rho) \lesssim_D \bar R(\rho),$$

where for $\rho > 1$

$$\bar R(\rho) = \max_{\zeta \in \mathbb R^r} \Big\{ \rho \zeta^T H - (\rho - 1)\, \mathbb E\|\zeta^T D_w h(W, \theta_*)\|_p^{\rho/(\rho - 1)} \Big\},$$

and for $\rho = 1$

$$\bar R(1) = \max_{\zeta :\ \mathbb P(\|\zeta^T D_w h(W, \theta_*)\|_p > 1) = 0} \zeta^T H.$$

The formal goal also asserts that $R_n(\theta_*)$ is finite and measurable and that both maxima are attained; these are facts the paper's statement presupposes.

Milestones (proof of Theorem 3, App. A.3)

1. Proposition 3 (p. 13): strong duality, $R_n(\theta) = \sup_\lambda \{ -\frac1n \sum_i \sup_u \{\lambda^T h(u, \theta) - c(u, W_i)\} \}$ when $\mathbf 0 \in \operatorname{int} \operatorname{conv} h(\mathbb R^m, \theta)$.
2. (31)–(32) (p. 32): $n^{\rho/2} R_n(\theta_*) = \sup_\zeta \{ -\zeta^T H_n - M_n(\zeta) \}$, with $H_n = n^{-1/2} \sum_i h(W_i, \theta_*)$ and the random penalty $M_n$.
3. Lemma 2 (p. 32): the supremum in (31) localizes to a compact set of $\zeta$ with high probability.
4. (42) (p. 36): $\max_\Delta \{ v^T \Delta - \|\Delta\|_q^\rho \} = \|v\|_p^{\rho/(\rho-1)} (1/\rho)^{1/(\rho-1)} (1 - 1/\rho)$.
5. Lemma 3 (p. 34): a uniform law of large numbers for the localized penalty.

Significance

Theorem 3 gives the rate $n^{-\rho/2}$ at which the RWP function at the true parameter vanishes and an explicit random variable bounding its rescaled limit. The $(1-\alpha)$-quantile $\eta_\alpha$ of $\bar R(\rho)$ yields a radius $\delta = n^{-\rho/2}\eta_\alpha$ for which the Wasserstein ball around $\mathbb P_n$ contains, with asymptotic probability at least $1 - \alpha$, a law satisfying the estimating equation at $\theta_*$ (§3.1, (19)); this is the paper's prescription for the regularization parameter of square-root LASSO and of regularized logistic regression (§4). Example 3 (p. 14) shows the bound is sharp for the mean: $n^{\rho/2} R_n(\theta_*) \Rightarrow \sigma_W^\rho |N(0, 1)|^\rho$. Matching lower bounds (Propositions 4 and 5) need further assumptions and are not part of this mission.

The result is proved in the paper; no machine-checked version of it, or of any RWP or empirical-likelihood limit theorem, is known to exist. A formalization would check the duality argument for the problem of moments, the passage from the dual representation to a localized maximization, and the continuous-mapping step, and would produce reusable statements: strong duality for transport-cost moment problems, the closed form of the conjugate of $\|\cdot\|_q^\rho$, and a uniform law of large numbers over a compact parameter set.

Difficulty

The obvious route is to apply the central limit theorem to $H_n$ and pass to the limit inside the dual representation (31). This fails as stated, for two reasons. First, the supremum in (31) is over all of $\mathbb R^r$, and convergence of the objective on compact sets does not control the supremum; Lemma 2 is needed, and it uses A4) through a lower bound on $\mathbb E\|\bar\zeta^T Dh(W)\|_p^p$ that is uniform over the unit sphere. Second, the penalty $M_n$ involves the derivative of $h$ at points $W_i + n^{-1/2}\Delta u$ that are not localized, with no moment assumption on $Dh$; the proof must truncate to $\|W_i\|_p \le c_0$ and to a specific near-optimal $\Delta$, and then remove the truncation. The case $\rho = 1$ differs: the inner supremum is $0$ or $+\infty$, and the limit becomes a maximization over a constraint set.

Formalization scope

Vectors are Fin k → ℝ; $\ell_q$ and $\ell_p$ norms are Mathlib's PiLp norms, so $q = \infty$ is allowed, with $q \in (1, \infty]$ and p.HolderConjugate q. The samples are a sequence W : ℕ → Ω → (Fin m → ℝ), mutually independent (iIndepFun) and identically distributed with W 0, which plays the role of $W$; $R_n$ uses $W_0, \dots, W_{n-1}$ through the published empiricalDistribution. Distinct samples are not assumed in Theorem 3; Proposition 3 and (31) keep the §3.1 assumption of distinct samples. Transport costs and $R_n$ are $[0, \infty]$-valued lower Lebesgue integrals and infima; $\bar R(\rho)$ is computed in the extended reals with the moment $\mathbb E\|\cdot\|_p^{\rho/(\rho-1)}$ in $[0, \infty]$. $H$'s law is multivariateGaussian 0 Cov on EuclideanSpace ℝ (Fin r).

The goal is a conjunction: finiteness of $R_n(\theta_*)$ for $n \ge 1$, its a.e.-measurability, attainment of the maxima in $\bar R(\rho)$, and the limsup bound. Without the first three, a real-valued formalization could hold for the wrong reason (an infinite $R_n$ converted to $0$, a non-measurable integrand integrated to $0$, or an unbounded supremum replaced by $0$); the conjunction rules this out.

Readings of the page recorded in the items: A1) says $q \ge 1$ while (17) and the proof of Lemma 2 use $q > 1$, and $q \in (1,\infty]$ is used; Proposition 3 is stated for a cost that is finite everywhere, the setting of §3, because for a cost that is infinite on part of the space the interior condition on $h(\mathbb R^m, \theta)$ does not imply the Slater condition used in App. B; Lemmas 2 and 3 state the standing assumptions A1), A3) and i.i.d. sampling that their statements leave implicit. The localized weak limit (45) is not a milestone: its penalty $M'_n$ depends on a $\zeta$-dependent near-optimal direction that is not stated precisely enough on the page.

Needed infrastructure: the multivariate central limit theorem (Mathlib has the real-valued one), Hölder duality for PiLp norms, a strong-duality theorem for moment problems (Proposition 7, quoted from Isii and Karlin–Studden), and a uniform law of large numbers. The duality results and the conjugate formula (42) are reusable beyond this mission. Proofs of any milestone, and lemmas that serve them, are welcome.

Selected references

• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019; arXiv:1610.05627v4. https://arxiv.org/abs/1610.05627
• A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. https://arxiv.org/abs/1604.01446
• K. Isii, On sharpness of Tchebycheff-type inequalities, Ann. Inst. Statist. Math. 14, 1962. https://doi.org/10.1007/BF02868641
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Motivation

A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.

The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.

Setting

Let $n$ assets have a random return vector $\xi\in\mathbb R^n$, and let $x\in\mathbb R^n$ be a portfolio, so the return is $\xi^{\mathsf T}x$. A distribution of $\xi$ is a Borel probability measure on $\mathbb R^n$ with finite second moments. For symmetric matrices, $A\preceq B$ (the Loewner order) means $B-A$ is positive semidefinite.

Given a support set $S$, a centre $\mu_0$, a positive definite matrix $\Sigma_0\succ0$ and $\gamma_1\ge0$, $\gamma_2>0$, the distributional set of Assumption 3 is

$$\mathcal D_1(S,\mu_0,\Sigma_0,\gamma_1,\gamma_2)=\Big\{P\ :\ P(\xi\in S)=1,\ (\mathbb E[\xi]-\mu_0)^{\mathsf T}\Sigma_0^{-1}(\mathbb E[\xi]-\mu_0)\le\gamma_1,\ \mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]\preceq\gamma_2\Sigma_0\Big\}.$$

The second constraint, (1b), is the covariance constraint.

The utility is piecewise linear concave, $u(y)=\min_{k\in\{1,\dots,K\}}a_ky+b_k$ with $K\ge1$ pieces, and the cost of a return is $-u$:

$$h(x,\xi)=\max_{k}\ \big(-a_k\,\xi^{\mathsf T}x-b_k\big).$$

With estimates $\hat\mu$, $\hat\Sigma\succ0$ of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean ($\gamma_1=0$) is

$$\max_{P\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,0,\gamma_2)}\ \mathbb E_P\big[h(x,\xi)\big].\tag{18}$$

The proof relates (18) to a semidefinite program in variables $\Lambda_k\in\mathbb R^{n\times n}$, $\lambda_k\in\mathbb R^n$, $\nu_k\in\mathbb R$:

$$\max\ \sum_k\big(-a_k\,x^{\mathsf T}\lambda_k-b_k\nu_k\big)\quad\text{s.t.}\quad \sum_k\Lambda_k\preceq\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T},\ \ \sum_k\lambda_k=\hat\mu,\ \ \sum_k\nu_k=1,\ \ \begin{bmatrix}\Lambda_k&\lambda_k\\\lambda_k^{\mathsf T}&\nu_k\end{bmatrix}\succeq0.\tag{19}$$

Formalization targets

Goal: Proposition 3

For every $\gamma_1\ge0$ (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case $\gamma_1=0$),

$$\exists\,P^*\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2):\quad \mathbb E_{P^*}\big[(\xi-\hat\mu)(\xi-\hat\mu)^{\mathsf T}\big]=\gamma_2\hat\Sigma\quad\text{and}\quad \mathbb E_Q[h(x,\xi)]\le\mathbb E_{P^*}[h(x,\xi)]\ \ \forall\,Q\in\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2).$$

The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio $x$, every $K\ge1$, every $a,b$, every $\hat\mu$, every $\hat\Sigma\succ0$, every $\gamma_1\ge0$ and every $\gamma_2>0$.

Milestones

1. Every value of (18) is dominated by the value of a feasible point of (19).
2. (19) has an optimal solution at which $\sum_k\Lambda_k=\gamma_2\hat\Sigma+\hat\mu\hat\mu^{\mathsf T}$.
3. If $\begin{bmatrix}\Lambda&\lambda\\\lambda^{\mathsf T}&\nu\end{bmatrix}\succeq0$ and $\nu>0$, a random vector with mean $\lambda/\nu$ and second moment $\Lambda/\nu$ exists.
4. The mixture $\sum_k\nu_kP_k$ of such vectors, built from a tight feasible point with all $\nu_k>0$, lies in $\mathcal D_1$ and has second moment $\gamma_2\hat\Sigma$ about $\hat\mu$.
5. The expected cost under that mixture is at least the objective value of (19) at the point.
6. (18) and (19) have the same attained optimal value.

Significance

The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound $\gamma_3\Sigma_0\preceq\mathbb E[(\xi-\mu_0)(\xi-\mu_0)^{\mathsf T}]$ (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with $\gamma_2=1$, the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).

The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with $\mathcal D_1(\mathbb R^n,\hat\mu,\hat\Sigma,\gamma_1,\gamma_2)$; the paper's proof writes out only $\gamma_1=0$ "for simplicity of our derivations". The goal states the proposition for every $\gamma_1\ge0$; the milestones follow the written proof and are stated for $\gamma_1=0$.

Difficulty

The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in $\mathcal D_1$ must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in $\xi$. Second, an optimal point of (19) must be turned back into a distribution in $\mathcal D_1$; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where $\nu_k=0$, which the paper sets aside "without loss of generality" although such a block can carry a nonzero $\Lambda_k$ that the mixture would lose.

Formalization scope

• Vectors are Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; $A\preceq B$ is (B - A).PosSemidef; $\Sigma_0^{-1}$ is Mathlib's matrix inverse, used only with $\Sigma_0\succ0$.
• A distribution is a Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in $L^2$ (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to $0$.
• $P(\xi\in S)=1$ is an almost-everywhere statement; the goal uses $S=\mathbb R^n$ ("infinite support constraint"). The convexity of $S$, $\mu_0\in\operatorname{int}S$ and the separation oracle of Assumption 3 concern the paper's algorithms and are not part of the set.
• The maximum of (18) is never a real supremum: the goal asserts a maximizer that dominates every member of the set. The cost uses a finite maximum over $K\ge1$ pieces ([NeZero K]).
• Standing hypotheses: $\hat\Sigma\succ0$ (Assumption 3's $\Sigma_0\succ0$, and endnote 1), $\gamma_2>0$ (§3), $\gamma_1\ge0$ (Assumption 3) in the goal; the milestones fix $\gamma_1=0$ as the proof does. The portfolio $x$ ranges over all of $\mathbb R^n$; the simplex constraint (16b) plays no role in the inner problem, so dropping it only strengthens the statements.
• The objective of (19) has the sign of the proof's final computation (p. 21), $\sum_k(-a_kx^{\mathsf T}\lambda_k-b_k\nu_k)$; display (19a) on p. 19 prints the opposite signs, a misprint.
• Ruling out trivial readings: the goal requires both membership in $\mathcal D_1$ with tight covariance and domination of every member of $\mathcal D_1$. A distribution with covariance $\gamma_2\hat\Sigma$ alone, or a maximizer alone, would not suffice. The goal does not claim that every maximizer is tight; for $K=1$ the cost is linear and every member of $\mathcal D_1$ is a maximizer.
• Infrastructure needed: existence of distributions with prescribed mean and covariance (for instance multivariate Gaussians, or degenerate laws on a subspace), finite mixtures of measures and their moments, Schur complements of positive semidefinite block matrices, and compactness of the feasible set of (19). Proofs of the milestones in any order are welcome.

The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.

Selected references

• E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010 (authors' draft of 20 February 2008 used here). https://doi.org/10.1287/opre.1090.0741
• I. Popescu, Robust mean-covariance solutions for stochastic optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• Y. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Many planning problems are made in two stages: a first decision $x$ is fixed before an uncertain parameter is revealed, and a second decision $y$ is taken afterwards. Two models compete for such problems. Two-stage stochastic optimization assumes a probability distribution over the scenarios and minimizes the expected cost, letting the second-stage decision depend on the scenario. Robust optimization asks for one solution that is feasible in every scenario and minimizes the worst-case cost. The robust problem is usually far easier to solve: it is a single deterministic problem, while the stochastic problem optimizes over policies. The question is how much cost one gives up by solving the easy problem instead of the hard one.

Bertsimas and Goyal (Math. Oper. Res. 2010) measure this loss by the stochasticity gap, the ratio of the robust optimum to the stochastic optimum. Their Theorem 2.1 shows that when only the right-hand side of the constraints is uncertain, the uncertainty set is symmetric and the distribution is centred at the point of symmetry, the robust optimum is at most twice the stochastic one. Section 3 asks whether the same holds when the second-stage costs are uncertain as well, and answers no with an explicit instance: Theorem 3.1. This mission formalizes that instance.

Setting

There are no first-stage variables. The second-stage decision is a vector $y\in\mathbb R^n_+$ with $n\ge1$ continuous coordinates, subject to the single covering constraint

$$y_1+y_2+\dots+y_n\ \ge\ 1 ,$$

the constraint $By\ge b$ with $B=[1,1,\dots,1]\in\mathbb R^{1\times n}$ and $b=1$. A set $\Omega$ of scenarios carries a cost map $d:\Omega\to\mathbb R^n$; in scenario $\omega$ the second-stage cost is $d(\omega)^{\mathsf T}y$. The uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)) : \omega\in\Omega\}$, here $\{1\}\times[0,1]^n$: the range of $d$ is the whole cube $[0,1]^n$. A probability measure $\mu$ on $\Omega$ makes the coordinates $d_1,\dots,d_n$ independent, each uniformly distributed on $[0,1]$.

The stochastic problem $\Pi_{\mathrm{Stoch}}(b,d)$, display (1.4) of the paper, chooses a policy $\omega\mapsto y(\omega)\ge0$ satisfying the constraint in every scenario and minimizes $\mathbb E_\mu[d(\omega)^{\mathsf T}y(\omega)]$; its optimal value is $z_{\mathrm{Stoch}}(b,d)$. The robust problem $\Pi_{\mathrm{Rob}}(b,d)$, display (1.5), chooses one $y\ge0$ satisfying the constraint and minimizes $\max_{\omega\in\Omega} d(\omega)^{\mathsf T}y$; its optimal value is $z_{\mathrm{Rob}}(b,d)$. A set $P$ is symmetric (Definition 1.2) if there is $u^0\in P$ with $u^0+z\in P\iff u^0-z\in P$ for every $z$.

The Lean development names these zStochBD and zRobBD (the general problems (1.4) and (1.5) with data $A$, $B$, $b$, $c$, $d$ and integer coordinate sets), and IsSymmetricAbout (Definition 1.2).

Formalization targets

Goal: Theorem 3.1 (p. 22)

$$z_{\mathrm{Rob}}(b,d)\ \ge\ (n+1)\cdot z_{\mathrm{Stoch}}(b,d).$$

The constant $n+1$ is the paper's. Both sides are pinned down separately by the milestones, so the goal cannot be satisfied by a degenerate value of either side.

Milestones

1. Symmetry of the instance (proof of Theorem 3.1, pp. 22–23): the uncertainty set is symmetric about $(1,(\tfrac12,\dots,\tfrac12))$ and $\mathbb E_\mu[d(\omega)]=(\tfrac12,\dots,\tfrac12)$, so the hypotheses of the symmetric theory hold.
2. Robust side (p. 23): $z_{\mathrm{Rob}}(b,d)\ge1$.
3. Eq. (3.1) (p. 23): $z_{\mathrm{Stoch}}(b,d)\le\mathbb E_\mu[\min(d_1(\omega),\dots,d_n(\omega))]$.
4. Eq. (3.2) (p. 23): $\mathbb E_\mu[\min(d_1(\omega),\dots,d_n(\omega))]=\dfrac1{n+1}$.

Significance

Theorem 3.1 marks the boundary of the paper's positive results. The bound $z_{\mathrm{Rob}}\le2\,z_{\mathrm{Stoch}}$ of Theorem 2.1 needs only symmetry of the uncertainty set and a centred distribution. The instance here has both, has no integer variables and a single constraint, and still has a gap that grows linearly in the dimension. So symmetry alone does not make a robust solution a good approximation of the stochastic optimum when costs are uncertain. The paper's abstract states this as one of its main conclusions, and it is why Sections 4 and 5 compare the robust problem with the adaptive problem, whose worst-case objective does not suffer from it.

The result is proved in the paper; to our knowledge it has no machine-checked proof. What this mission adds is a formal proof of the instance against the general definitions of the two-stage problems, including the probabilistic computation (3.2), the expected minimum of independent uniform random variables, which Mathlib does not contain. That computation is reusable wherever order statistics of uniforms appear, for example in auctions, secretary problems and random-assignment bounds.

Difficulty

The robust half is short. The stochastic half has two parts. Eq. (3.1) needs a measurable policy that selects a cheapest coordinate; the policy printed in the paper puts a unit on every minimizing coordinate, which at ties overpays, so a formal proof must choose a single minimizer measurably and use integrability on the probability space. Eq. (3.2) is the main work: it is a genuine integral over the $n$-dimensional cube against a product measure, for every $n$, and Mathlib has no lemma on the distribution or the expectation of the minimum of independent random variables.

Formalization scope

• Vectors are Fin k → ℝ with the componentwise order; $B$ is the all-ones Matrix (Fin 1) (Fin n) ℝ, $A$ and $c$ live on Fin 0, $b(\omega)=1$, and the integer coordinate sets are empty ($p_1=p_2=0$).
• Optimal values are infima in EReal, $+\infty$ when infeasible; the robust worst-case cost is an EReal supremum. No optimal solution is assumed to exist: the paper's "consider an optimal solution" is a proof device, and the statements are about the infima.
• Stochastic policies must be integrable, together with their cost $\omega\mapsto d(\omega)^{\mathsf T}y(\omega)$, and satisfy the constraint in every scenario, as on the page, not only almost surely.
• The scenario space is an arbitrary probability space $(\Omega,\mu)$ with a measurable $d$ whose range is exactly $[0,1]^n$ and whose law is the product of $n$ uniform distributions on $[0,1]$. This is the paper's "each $d_j$ is distributed uniformly at random between 0 and 1 and independent of other coefficients" together with its description of $I_{(b,d)}(\Omega)$.
• $n\ge1$ is assumed; the paper leaves it implicit.
• The paper prints $\mathbb Z^{n_2}_+$ for the second-stage integer block in (1.4)–(1.5); $\mathbb Z^{p_2}_+$ is meant, and here $p_2=0$. Eq. (3.2) is called an inequality on the page; it is formalized as the equality it is.

A real-valued infimum would assign the value $0$ to an infeasible or ill-posed problem and make the goal trivially true; the EReal infima, and the separate milestones fixing $z_{\mathrm{Rob}}\ge1$ and $z_{\mathrm{Stoch}}\le\mathbb E[\min_j d_j]=1/(n+1)$, rule that out.

Contributions are welcome on each milestone separately. The expected-minimum computation (3.2) is self-contained and of independent use; a general lemma on the law of the minimum of independent random variables would serve it and other missions.

Selected references

• D. Bertsimas, V. Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited here from the authors' manuscript, MIT DSpace).
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• D. Bertsimas, M. Sim, The Price of Robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

Many operations problems are decided in two stages: a first-stage decision is fixed before an uncertain quantity is revealed, and a second-stage (recourse) decision is chosen afterwards. Two classical ways to optimize such a problem differ in how they treat the uncertainty. Two-stage stochastic optimization minimizes the expected cost under a probability distribution over scenarios, with a recourse decision adapted to each scenario. Robust optimization fixes a single solution that must be feasible for every scenario in an uncertainty set, and minimizes the worst-case cost. The robust problem is usually far easier to solve, but it is conservative; the question is how much it can lose.

Bertsimas and Goyal (Math. Oper. Res. 35(2), 2010) answer this for uncertain right-hand sides. Their main positive result (Theorem 2.1) bounds the stochasticity gap: if the uncertainty set and the probability measure are both symmetric, the robust optimum is at most twice the stochastic optimum. This mission formalizes the companion negative result, Theorem 2.6: once the uncertainty set is not symmetric, the gap is not bounded by any constant. The example is the simplest non-symmetric set in practice, the corner of the unit simplex, with the uniform distribution on it. It shows that the symmetry hypothesis in the positive result is not an artefact of the proof.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$ and costs $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$. Let $\Omega$ be a set of scenarios, $b:\Omega\to\mathbb R^m_+$ the right-hand side realized in each scenario, and $I_b(\Omega)=\{b(\omega)\mid\omega\in\Omega\}$ the uncertainty set. Let $\mu$ be a probability measure on $\Omega$.

• The stochastic problem $\Pi_{\mathrm{Stoch}}(b)$ (1.1) chooses $x\ge 0$ and a second-stage policy $y(\omega)\ge 0$ with $Ax+By(\omega)\ge b(\omega)$ for every $\omega\in\Omega$, minimizing $c^Tx+\mathbb E_\mu[d^Ty(\omega)]$. Its optimal value is $z_{\mathrm{Stoch}}(b)$.
• The robust problem $\Pi_{\mathrm{Rob}}(b)$ (1.2) chooses a single pair $x\ge 0$, $y\ge 0$ with $Ax+By\ge b(\omega)$ for every $\omega$, minimizing $c^Tx+d^Ty$. Its optimal value is $z_{\mathrm{Rob}}(b)$.

In general some coordinates of $x$ and $y$ are required to be integers; in this mission's instance there are none. A set $P\subseteq\mathbb R^n$ is symmetric (Definition 1.2) if some $u^0\in P$ satisfies $u^0+z\in P\iff u^0-z\in P$ for every $z\in\mathbb R^n$.

The instance of Theorem 2.6 has no first stage ($n_1=0$, so $A=0$, $c=0$), $n_2=m=n\ge 3$, $B=I_n$, and $d=e_n=(0,\dots,0,1)$. The uncertainty set is the corner simplex (2.29)

$$I_b(\Omega)=\Big\{\,b\in\mathbb R^n \;:\; \sum_{j=1}^n b_j\le 1,\ b\ge 0\,\Big\},$$

and $\mu$ is the uniform probability measure on it: $\mu(S)=\operatorname{volume}(\{b(\omega)\mid\omega\in S\})/\operatorname{volume}(I_b(\Omega))$.

Formalization targets

Goal: Theorem 2.6

On this instance,

$$z_{\mathrm{Rob}}(b)\ \ge\ (n+1)\cdot z_{\mathrm{Stoch}}(b).$$

The constant $n+1$ is the paper's, and it is exact: the robust optimum is $1$ and the stochastic optimum is at most $1/(n+1)$.

Milestones

1. Lemma 2.4. The corner simplex is not symmetric for $n\ge 2$.
2. Robust side (p. 20). Every robust-feasible $y$ has $y_j\ge 1$ for all $j$, so $z_{\mathrm{Rob}}(b)\ge 1$.
3. Eq. (2.30). The policy $\hat y(\omega)=b(\omega)$ is feasible for $\Pi_{\mathrm{Stoch}}(b)$, so $z_{\mathrm{Stoch}}(b)\le\mathbb E_\mu[b_n(\omega)]$.
4. Eq. (2.32), denominator. $\operatorname{vol}(I_b(\Omega))=1/n!$.
5. Eq. (2.32), numerator. $\int_{I_b(\Omega)}x_n\,dx=1/(n+1)!$.
6. Eqs. (2.31)–(2.32). $\mathbb E_\mu[b_n(\omega)]=1/(n+1)$.

Significance

The result. Together with Theorem 2.1, Theorem 2.6 locates the boundary of the paper's positive theory. Theorem 2.1 says a static robust solution loses at most a factor of $2$ against the fully adaptive stochastic optimum under symmetry; Theorem 2.6 says that without symmetry the factor can be $n+1$, hence arbitrarily large as the dimension grows. The paper's later results (the bound for "positive" uncertainty sets, Theorem 2.7) are motivated by this example: some structural condition replacing symmetry is necessary. The same instance also separates the adaptive problem from the stochastic one (p. 21), which shows that the gap comes from comparing a worst case with an expectation, not from the lack of adaptivity.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The formalization adds two things beyond the paper. First, it pins down the problems as optimization problems over integrable policies with values in the extended reals, so that the inequality cannot hold for a degenerate reason. Second, it requires the volume of the corner simplex and the first moment of a coordinate on it, which the paper calls "standard computation". Neither is in Mathlib at the time of writing: Mathlib has the standard simplex as a convex set but no volume formula for it.

Difficulty

The optimization part is short: one feasible stochastic policy and the vertices of the simplex give both bounds. The work is in the measure theory. The volume $1/n!$ and the moment $1/(n+1)!$ are iterated integrals with variable upper limits, and the paper calls them "standard computation"; as statements about Lebesgue measure on $\mathbb R^n$ they are dimension-dependent identities that Mathlib does not contain, for the simplex or for the convex hull of $n+1$ points. The other technical point is the scenario model: the uniform measure lives on $\Omega$, while the integrals live on $\mathbb R^n$, so the expectation must be moved through the push-forward of $\mu$ by $b$.

Formalization scope

• Vectors are Fin k → ℝ with the componentwise order; products are A *ᵥ x and c ⬝ᵥ x. The paper's $n$-th coordinate is index $n-1$ of Fin n, and $e_n$ is lastUnit n.
• The optimal values $z_{\mathrm{Rob}}$ and $z_{\mathrm{Stoch}}$ are EReal infima over the feasible set, equal to $+\infty$ when the problem is infeasible. No optimal solution is assumed to exist.
• Policies of $\Pi_{\mathrm{Stoch}}(b)$ are $\mu$-integrable functions $\Omega\to\mathbb R^n$ (the paper takes their expectation), and the constraints hold for every scenario, as printed, not almost surely.
• The integer coordinates are given as a set of indices; the instance uses the empty set ($p_2=0$, as in the displays on p. 20). The generic definitions keep the mixed-integer domain so that they agree with the other missions of this series.
• The uniform measure is encoded by quantifying over every scenario model $(\Omega,\mu,b)$ in which $\mu$ is a probability measure, $b$ is measurable, the range of $b$ is the corner simplex, and the push-forward of $\mu$ by $b$ equals Lebesgue measure restricted to the simplex divided by its volume. The model $\Omega=$ simplex, $b=$ identity satisfies these hypotheses; the paper's formula for $\mu(S)$ is read as a statement about this push-forward.
• The hypothesis $n\ge 3$ is the paper's and is kept; the argument appears to need only $n\ge 1$.
• Ruled out: a real-valued infimum for $z_{\mathrm{Stoch}}$, which would be a junk $0$ on an infeasible problem and make the goal trivially true; an arbitrary measure, or a Dirac mass at the mean, in place of the uniform measure; and constraints only $\mu$-almost surely.

Needed infrastructure: the volume of the corner simplex in $\mathbb R^n$ and the integral of a coordinate over it (reusable well beyond this mission, for example for Dirichlet distributions and order statistics), and the change of variables from $\Omega$ to $\mathbb R^n$ through the push-forward. Contributions of either simplex integral, in any form that implies the stated milestones, are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 284–305, 2010. https://doi.org/10.1287/moor.1090.0440 (formalized from the authors' manuscript, MIT DSpace / MIT Open Access Articles)
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1), 1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 35–53, 2004. https://doi.org/10.1287/opre.1030.0065
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Two-stage optimization separates a decision made before uncertainty is observed from one made after a scenario is known. A fully adaptive policy can choose a different second-stage decision in each scenario, while a static robust solution commits to a single second-stage decision that works in every scenario. Static solutions can be simpler to implement, but their worst-case cost may be higher. Bertsimas and Goyal ask how large this cost difference can be when both the right-hand sides of the constraints and the second-stage prices vary. Their Theorem 5.1 gives a factor of four when the paired uncertainty set is symmetric and nonnegative, even when both stages contain integer variables.

The distinction matters in planning problems where one policy is fixed in advance and another could respond to realized demand or prices. A uniform bound lets a planner assess the cost of the static restriction without solving every adaptive policy exactly. The source is the authors' manuscript; all page and result numbers in this mission refer to that manuscript, not to the journal pagination.

Setting

Fix matrices $A\in\mathbb R^{m\times n_1}$ and $B\in\mathbb R^{m\times n_2}$. A scenario $\omega\in\Omega$ supplies a right-hand side $b(\omega)\in\mathbb R_+^m$ and a second-stage cost vector $d(\omega)\in\mathbb R_+^{n_2}$. The first-stage cost vector is $c\in\mathbb R_+^{n_1}$. For a set $I$ of designated integer coordinates, write $D_I$ for the nonnegative real vectors whose coordinates in $I$ are integers. After relabelling, this is the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$.

In the robust problem $\Pi_{\mathrm{Rob}}(b,d)$, one first-stage decision $x\in D_{I_1}$ and one second-stage decision $y\in D_{I_2}$ must satisfy $Ax+By\ge b(\omega)$ for every scenario. Their cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty$. In the adaptive problem $\Pi_{\mathrm{Adapt}}(b,d)$, $x$ is still chosen once, but $y(\omega)\in D_{I_2}$ may depend on the scenario. Its constraints are $Ax+By(\omega)\ge b(\omega)$ for every $\omega$, and its cost is $c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega)$. The optimal values $z_{\mathrm{Rob}}(b,d)$ and $z_{\mathrm{Adapt}}(b,d)$ are infima over feasible decisions in these respective problems; these are models (1.5)–(1.6).

The paired uncertainty set is $I_{(b,d)}(\Omega)=\{(b(\omega),d(\omega)): \omega\in\Omega\}$. It is symmetric when it contains a point $u^0$ such that $u^0+z$ belongs to the set exactly when $u^0-z$ does, for every displacement $z$. The point $u^0$ is itself a scenario realization. The smallest coordinatewise bounding hypercube has lower and upper corners $(b^l,d^l)$ and $(b^h,d^h)$; its center is $((b^l+b^h)/2,(d^l+d^h)/2)$. These are Definition 1.2 and displays (2.5)–(2.7).

Formalization targets

The adaptability gap

The goal is Theorem 5.1:

$$z_{\mathrm{Rob}}(b,d)\le 4z_{\mathrm{Adapt}}(b,d).$$

The factor applies to every nonnegative symmetric paired uncertainty set and to both continuous and mixed-integer decisions. The theorem does not require an optimal adaptive policy to attain its infimum. The milestones record the source's geometric Lemma 2.3 and the estimates labelled (5.1)–(5.4), which supply the center-scenario cost and feasibility statements with the explicit factor four. They are stated for arbitrary feasible adaptive policies so the conclusion also covers nonattained infima.

Significance

The result bounds the price of committing to a single second-stage decision, despite uncertainty in both the constraints and the objective. In this setting the comparison is independent of the number of scenarios and of the dimensions $m,n_1,n_2$. The paper also considers right-hand-side-only uncertainty, positive sets, and hypercubes; this mission isolates its symmetric paired-uncertainty result §5.1.

The theorem is proved in the paper. The remaining formalization work is a machine-checked development of the model, the bounding-hypercube geometry, the cost inequalities, and the passage from arbitrary feasible policies to the optimal values. The resulting definitions of mixed-integer domains, robust and adaptive feasibility, and extended-real optimal values can also support the other results in this paper's mission series. The theorem statements here are open proof targets, with no machine-checked proofs claimed.

Difficulty

The worst-case maximizer of $d(\omega)^Ty(\omega)$ can vary with $\omega$, and an adaptive policy can choose a different integer vector in every scenario. Selecting one of those vectors as a static decision therefore gives no immediate cost or feasibility guarantee. The point of symmetry is a realizable scenario, but it must control both components of every other paired scenario. Without nonnegative data, doubling the center-scenario decision may fail to cover a positive right-hand side, and the cost comparison can fail as well. Integer coordinates also constrain which scalings preserve the decision domain; the exact factor in the theorem is compatible with doubling, unlike arbitrary fractional rescalings.

Formalization scope

Vectors are real functions on finite index types, matrices use Mathlib's matrix-vector product, and inequalities are componentwise. The scenario set is the range of $\omega\mapsto(b(\omega),d(\omega))$, with a product-space symmetry predicate. No probability measure or measurability structure is used in these worst-case problems. Both stages may have integer coordinates designated by sets $I_1,I_2$; no continuous-only second-stage restriction is imposed.

Optimal values and worst-case costs use extended real numbers. An infeasible problem has value $+\infty$; a real infimum over an empty feasible set would incorrectly return a default zero. Symmetry includes a center belonging to the scenario range, so the scenario set is nonempty. Combined with nonnegative coordinates, symmetry bounds every scenario coordinate and makes the bounding-hypercube endpoints meaningful. The hypotheses retain $c\ge0$, $b(\omega)\ge0$, and $d(\omega)\ge0$, which the source uses in its factor-four estimate. A statement restricted to continuous recourse, an assumed optimal adaptive policy, or a zero-valued infeasible problem would not express this target.

The source prints $\mathbb Z_+^{n_2}$ in (1.5)–(1.6), although the model's second-stage integer count is $p_2$; the domain here follows the surrounding $p_2$ convention. Lemma 2.3 is stated here for nonnegative sets, the regime needed for its second inequality. Its coordinatewise suprema and infima agree with the printed maxima and minima in this bounded symmetric setting. Contributions to the shared domain and geometry lemmas, the mixed-integer scaling fact, and the optimal-value comparison are all useful to the goal.

Selected references

• Dimitris Bertsimas and Vineet Goyal, On the Power of Robust Solutions in Two-Stage Stochastic and Adaptive Optimization Problems, authors' manuscript of Mathematics of Operations Research, 2010. DOI: 10.1287/moor.1090.0440.