Linear Optimization

Motivation

The data of a linear program are often not known exactly: they are measured or estimated, or they are forecasts. The robust counterpart approach, going back to Soyster (1973), asks for a solution that is feasible for every data matrix in a prescribed uncertainty set and is best among such solutions. Ben-Tal and Nemirovski's 1999 paper [1] showed that the method stays computationally tractable for a broad class of uncertainty sets, the ellipsoidal uncertainties: the robust counterpart of an uncertain LP is then a conic quadratic program (CQP), solvable by interior point methods at roughly the cost of an LP of similar size. This result is the basis of robust linear optimization as it is used today [2], [3]. It is also the reason ellipsoidal sets are the default choice in robust portfolio selection (§4 of the paper) and in many later robust models.

Timeline. Soyster (1973) treated column-wise box uncertainty, for which the counterpart is again an LP [4]. Ben-Tal and Nemirovski (1998) developed the general theory of robust convex optimization [5]. The present paper (1999) proved the ellipsoidal-to-CQP reduction for LPs (Theorem 3.1). Its proof relies on the conic duality theory of Nesterov and Nemirovski (1994) [6].

Setting

An uncertain linear program in the homogeneous form (6) is

$$\min\{c^Tx \mid Ax \ge 0,\ f^Tx = 1\},$$

where $c, f \in \mathbb R^n$ are fixed and the matrix $A \in \mathbb R^{m\times n}$ lies in an uncertainty set $\mathcal U$. A point $x$ is robust feasible if $f^Tx = 1$ and $Ax \ge 0$ for every $A \in \mathcal U$. The robust counterpart $(P_{\mathcal U})$ minimizes $c^Tx$ over the robust feasible set

$$G_{\mathcal U} = \{x \mid Ax \ge 0\ \forall A \in \mathcal U,\ f^Tx = 1\}.$$

An ellipsoid in $\mathbb R^{m\times n}$ (display (14)) is a set

$$U(\Pi, Q) = \{\Pi(u) \mid \|Qu\| \le 1\},$$

where $\Pi(u) = P^0 + \sum_{j=1}^L u_jP^j$ is affine in $u \in \mathbb R^L$, $Q$ is an $M\times L$ matrix, and $\|\cdot\|$ is the Euclidean norm. A singular $Q$ gives an ellipsoidal cylinder, which may be unbounded. An ellipsoidal uncertainty is a set

$$\mathcal U = \bigcap_{\ell=0}^k U(\Pi_\ell, Q_\ell)$$

(condition A) that is bounded (condition B) and contains a matrix $A$ with $A = \Pi_\ell(u^\ell)$ and $\|Q_\ell u^\ell\| < 1$ for every $\ell$ (condition C, a Slater condition).

Formalization targets

Goal: Theorem 3.1

For every $x \in \mathbb R^n$,

$$x \in G_{\mathcal U} \iff f^Tx = 1 \ \text{ and }\ \forall i \le m\ \ \exists\, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)} :\ (x, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)}) \text{ satisfies } (\mathcal C_i).$$

Here $(\mathcal C_i)$ is an explicit system: linear equations and one linear inequality in $(x, \lambda, \mu, \nu)$, together with the second-order cone constraints $\|\mu^{(i)}_\ell\| \le \nu^{(i)}_\ell$. Its coefficients are the matrices $P^j_\ell$ and $Q_\ell$. The robust feasible set is therefore the projection of the feasible set of the conic quadratic program (CQP), which minimizes $c^Tx$ subject to $(\mathcal C_1), \dots, (\mathcal C_m)$ and $f^Tx = 1$.

Milestones, in the order of the Appendix's proof

1. $\mathcal U$ equals the image of the feasible set of the problem $(P_i[x])$ under $u \mapsto \Pi_0(u^0)$ (p. 15).
2. Claim (I): with $f^Tx = 1$, $x$ is robust feasible iff every $(P_i[x])$ has nonnegative optimal value (p. 15).
3. Claim (II): conic quadratic duality. A strictly feasible primal that is bounded below has a solvable dual with equal optimal value (p. 15).
4. Conditions B and C make every $(P_i[x])$ strictly feasible and bounded below (p. 16).

Companion results

The CQP forms (16) and (17) of the simplest cases (a single ellipsoid; constraint-wise ellipsoids), Remark 3.1 (bounded polytopes are ellipsoidal uncertainties), and the robust portfolio counterpart (22).

Significance

The result. Theorem 3.1 turns a semi-infinite constraint system (one constraint for every $A \in \mathcal U$) into finitely many conic quadratic constraints whose size is polynomial in the data. Robust LPs with ellipsoidal uncertainty, which by Remark 3.1 include polytopic uncertainty, can therefore be solved by standard conic solvers. Later robust optimization results, such as budgeted uncertainty, affinely adjustable policies and distributionally robust LPs, refine this pattern.

Formalizing it. The theorem is classical and its proof is complete, but no machine-checked proof exists. A formal proof needs a conic quadratic strong duality theorem with dual attainment (claim (II)), which Mathlib does not have in this form. That duality theorem can be reused well beyond this mission. The companion results (16), (17) and (22) are self-contained computations of a minimum of a linear function over a Euclidean ball.

Difficulty

The "if" direction is weak duality: a solution of $(\mathcal C_i)$ certifies that the $i$-th constraint holds for all of $\mathcal U$. The content is the "only if" direction. It requires dual attainment, not merely equality of optimal values, because a solution of $(\mathcal C_i)$ must exist. Dual attainment fails without a constraint qualification. Condition C must hold strictly for every ellipsoid, including $\ell = 0$, and the ellipsoids may be cylinders, so the variables $u^\ell$ can range over unbounded sets even though $\mathcal U$ is bounded. Projecting the problem onto a single parameter space is not available in general, because the maps $\Pi_\ell$ need not be injective.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The indices $\ell = 0, \dots, k$ are Fin (k + 1), and the $k$ equality multipliers $\lambda_\ell$, $\ell \ge 1$, are indexed by Fin k. Every norm is Euclidean, written out as euclidNorm v = √(∑ v_j²), because Mathlib's norm on Fin M → ℝ is the sup norm, under which ellipsoids would become boxes. Condition B is a uniform bound on all matrix entries, and condition C is required for every $\ell = 0, \dots, k$. The page's words say "$\ell = 1, \dots, k$", but its display and the proof use every $\ell$. Injectivity of $\Pi_\ell$ is not assumed, and neither is §2.1's standing assumption that $\mathcal U$ is convex and closed. An ellipsoidal uncertainty is convex automatically, and closedness is not used, so both omissions generalize the statement. Three printed slips are corrected and disclosed: the sum in the equality constraint of (CQP$_d$) runs over $\ell = 0, \dots, k$; $(\mathcal C_i)$ has $\varphi^{(i)}[x]$ where the page prints $f^{(i)}[x]$; and Remark 3.1 has the factor $2/(r_i - s_i)$ where the page prints $(r_i - s_i)/2$.

The goal is not the contentless statement "some conic quadratic program has $G_{\mathcal U}$ as a projection", which holds for every closed convex set. It names the system $(\mathcal C_i)$ built from the data $P^j_\ell$, $Q_\ell$. The goal also does not mention optimal values, (CQP$_p$) or strict feasibility; those are milestones.

Contributions are welcome on the conic duality theorem (II) as a standalone result, on the finite-dimensional facts that minimize a linear function over a Euclidean ball (used in (16), (17) and (22)), and on the goal itself.

Selected references

1. 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
2. A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
3. D. Bertsimas, D. B. Brown, C. Caramanis, Theory and applications of robust optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510
4. A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
5. A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
6. Yu. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Robust linear optimization replaces an uncertain constraint $\tilde a'x \ge b$ by the requirement that $a'x \ge b$ hold for every $a$ in an uncertainty set $\mathcal U$ (Ben-Tal and Nemirovski 1999). The method leaves open where $\mathcal U$ should come from. Risk theory answers a related question from the other side: a decision maker's attitude to an uncertain reward is described by a risk measure $\mu$, and the constraint is imposed as $\mu(\tilde a'x - b) \le 0$.

Bertsimas and Brown (2009) connect the two. When $\mu$ is coherent and $\tilde a$ is supported on finitely many observed data points $a_1, \dots, a_N$, the risk constraint is exactly a robust constraint whose uncertainty set is built from the data and the family of probability vectors generating $\mu$. For the class of distortion risk measures, the uncertainty set has an explicit polyhedral form, the $q$-permutohull of the data, and the robust constraint has a reformulation of polynomial size. This mission formalizes that chain of results, Sections 2–4.3 of the paper.

Setting

The sample space is finite, $\Omega = \{\omega_1, \dots, \omega_N\}$, and a random variable is a vector $X \in \mathbb R^N$, read as a reward; $X \ge Y$ means $X_i \ge Y_i$ for every $i$. The probability simplex is $\Delta^N = \{p \in \mathbb R^N_+ : e'p = 1\}$, and $\mathbb E_q[X] = \sum_i q_i X_i$.

A risk measure is a function $\mu : \mathbb R^N \to \mathbb R$ with $X \ge Y \Rightarrow \mu(X) \le \mu(Y)$ and $\mu(X + c) = \mu(X) - c$. It is coherent if it is moreover convex and positively homogeneous. A set $\mathcal Q \subseteq \Delta^N$ generates $\mu$ if $\mu(X) = \sup_{q \in \mathcal Q} \mathbb E_q[-X]$ for all $X$. The conditional value-at-risk under a probability vector $p$ is $\mathrm{CVaR}_\alpha(X) = \inf_{\nu \in \mathbb R}\{\nu + \frac1\alpha \mathbb E_p[(-\nu - X)^+]\}$ for $\alpha \in (0,1]$.

Two random variables are comonotone if $(X(\omega) - X(\omega'))(Y(\omega) - Y(\omega')) \ge 0$ for all $\omega, \omega'$; $\mu$ is comonotonic if it is additive on comonotone pairs, and law invariant if it takes equal values on random variables with the same distribution. A distortion risk measure is a coherent, comonotonic, law-invariant risk measure. From Section 4.2 on, $\Omega$ carries the uniform distribution $\mathbb P\{\omega_i\} = 1/N$.

The restricted simplex is $\hat\Delta^N = \{q \in \Delta^N : q_1 \ge \cdots \ge q_N\}$. For $q \in \hat\Delta^N$ put

$$\mu_q(X) = -\sum_{i=1}^N q_i x_{(i)},$$

where $x_{(1)} \le \cdots \le x_{(N)}$ are the increasing order statistics of $X$. The data are $\mathcal A = \{a_1, \dots, a_N\} \subseteq \mathbb R^n$, the uncertain vector $\tilde a$ takes the value $a_i$ at $\omega_i$, and the $q$-permutohull of $\mathcal A$ is

$$\Pi_q(\mathcal A) = \operatorname{conv}\Big\{\sum_{i=1}^N q_{\sigma(i)} a_i : \sigma \in S_N\Big\}.$$

Formalization targets

Goal: Theorem 4.3

Under the uniform distribution, for every distortion risk measure $\mu$ there is $q \in \hat\Delta^N$ with $\mu = \mu_q$, and for this $q$, all data and every $b$,

$$\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \Pi_q(\mathcal A)\} = \{x : \exists y_1, y_2 \in \mathbb R^N,\ e'y_1 + e'y_2 \ge b,\ y_{1,i} + y_{2,j} \le q_i\, a_j'x\ \forall i, j\}.$$

The vector $q$ depends on $\mu$ only; the data are quantified after it.

Milestones

1. Theorem 2.1. $\mu$ is coherent if and only if some family $\mathcal Q \subseteq \Delta^N$ generates it.
2. Theorem 3.1. For coherent $\mu$ generated by $\mathcal Q$, $\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \operatorname{conv}\{Aq : q \in \mathcal Q\}\}$; conversely every nonempty $\mathcal U \subseteq \operatorname{conv}(\mathcal A)$ arises from the coherent measure generated by $\{q \in \Delta^N : Aq \in \mathcal U\}$.
3. Generation of (4). $\mu_q$ is generated by the permuted vectors $q \circ \sigma$, $\sigma \in S_N$.
4. Theorem 4.1 (Schmeidler). A coherent $\mu$ is comonotonic if and only if $\mu(X) = \int (-X)\,dg$ (Choquet integral) for a monotone, normalized, submodular $g : 2^\Omega \to [0,1]$.
5. Second differences (proof of Lemma 4.1). A submodular $g$ depending only on $|A|$ has nonincreasing increments along $\emptyset \subset \{\omega_1\} \subset \{\omega_1, \omega_2\} \subset \cdots$.
6. Lemma 4.1. A risk measure is a distortion risk measure if and only if $\mu(X) = \int_{(0,1]} \mathrm{CVaR}_\alpha(X)\,\nu(d\alpha)$ for a probability measure $\nu$.
7. The CVaR display (proof of Theorem 4.2). $\mathrm{CVaR}_\alpha(X) = \sup\{\mathbb E_q[-X] : q \in \Delta^N,\ q_i \le 1/(N\alpha)\} = \mu_{q^\alpha}(X)$ with $q^\alpha \in \hat\Delta^N$.
8. Theorem 4.2. A risk measure is a distortion risk measure if and only if $\mu = \mu_q$ for some $q \in \hat\Delta^N$; every such $q$ is a convex combination of the generators $\hat q^j$ of $\mathrm{CVaR}_{j/N}$.
9. Assignment duality (proof of Theorem 4.3). $a'x \ge b$ on $\Pi_q(\mathcal A)$ if and only if the linear system in $(y_1, y_2)$ above is feasible.

A companion item states Corollary 4.3: $\Pi_{\sum_j \lambda_j \hat q^j}(\mathcal A) = \operatorname{conv}\{\sum_j \lambda_j \frac1j \sum_{i \le j} a_{\sigma_j(i)} : \sigma_j \in S_N\}$, and the class equality it yields: the uncertainty sets $\Pi_q(\mathcal A)$ of all distortion risk measures $\mu = \mu_q$ are exactly the polytopes $\mathcal U_\lambda(\mathcal A)$, $\lambda \ge 0$, $\sum_j \lambda_j = 1$.

Significance

The goal theorem identifies the uncertainty set implied by any distortion risk measure: it is a permutohull of the data, a polytope with up to $N!$ vertices that is nevertheless representable with $2N$ extra variables and $N^2$ linear constraints. Combined with Theorem 4.2, the uncertainty sets of distortion measures are exactly the mixtures of the sets of $j$-point averages of the data (Corollary 4.3), with $\mathrm{CVaR}_{j/N}$ as the generators. The later sections of the paper build on this: centrally symmetric permutohulls (Section 4.4) and the construction of a distortion risk measure from a given polyhedral uncertainty set (Section 4.5) are the subjects of the two companion missions.

The results are proved in the paper; no machine-checked version is known. The formalization adds checked statements of the finite-space representation theory of coherent and distortion risk measures, which the paper obtains partly by citing general results, and records the corrections the printed statements need.

Difficulty

The two equalities of the goal have unequal weight. The second is a statement about one polytope with up to $N!$ vertices and a linear system of size $O(N^2)$; it is finite-dimensional linear programming. The first requires the complete characterization of distortion risk measures on a finite uniform space, and that is where the obvious approach fails. The known representation of law-invariant comonotonic coherent measures as mixtures of CVaR (Kusuoka 2001) is proved for atomless spaces and does not transfer to a discrete $\Omega$. The uniform distribution is essential, not a convenience: Remark 4.2 of the paper gives a two-point space with probabilities $1/3, 2/3$ and a monotone, normalized, submodular set function depending only on probability whose induced distortion is not concave, so the conclusion of Theorem 4.2 fails there.

Formalization scope

• $\Omega$ is Fin N with $N \ge 1$; random variables are Fin N → ℝ; indices are 0-based throughout, so qhat j is the paper's $\hat q^{j+1}$ and $q_1 \ge \cdots \ge q_N$ is Antitone q. Order statistics are X ∘ Tuple.sort X.
• Probability measures on $\Omega$ are probability vectors in stdSimplex ℝ (Fin N). Generation (1) is an IsLUB over an arbitrary set of probability vectors, not a maximum over a finite family (that version is false).
• Sign of the risk constraint. Display (2) and Theorem 4.3 print $\mu(\tilde a'x - b) \ge 0$. The paper introduces the constraint as $\mu(\tilde a'x - b) \le 0$ (p. 1486) and the proof of Theorem 3.1 computes $\mu(\tilde a'x - b) = -\inf_{a \in \mathcal U} a'x + b$; all statements use $\le 0$.
• Standing assumptions. Theorems 2.1 and 3.1 assume a probability vector $p$ with $p_i > 0$ (full support makes $\mathbb Q \ll \mathbb P$ vacuous; with a null atom Theorem 2.1 fails for functions on $\Omega$). From Lemma 4.1 on the distribution is uniform (Assumption 4.1). Theorem 3.1's converse adds $\mathcal U \neq \emptyset$.
• CVaR is a real infimum, used only for $\alpha \in (0,1]$, where the objective is bounded below by $\mathbb E[-X]$. In Lemma 4.1 the mixing measure $\nu$ is a probability measure on $(0,1]$; the page's $\int_0^1$ is read over $(0,1]$. The CVaR display uses the corrected coefficient $(N\alpha - \lfloor N\alpha \rfloor)/(N\alpha)$ in place of the printed $/\lfloor N\alpha \rfloor$. The assignment-duality milestone is stated for every $q \in \mathbb R^N$.
• The goal must assert the representation $\mu = \mu_q$ together with the set equalities: a statement "there is some $q$ for which the sets coincide" would let $q$ depend on the data and is not Theorem 4.3. The goal does not assume $\mu = \mu_q$, which is Theorem 4.2's conclusion.
• Needed infrastructure: Birkhoff's theorem (in Mathlib), LP duality, the rearrangement inequality, Choquet integrals of step functions. Lemmas about $\mu_q$ and order statistics are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

• D. Bertsimas, D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
• 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
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• D. Schmeidler, Integral representation without additivity, Proceedings of the AMS 97(2):255–261, 1986. https://doi.org/10.1090/S0002-9939-1986-0835875-8
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
• S. Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3:83–95, 2001. https://doi.org/10.1007/978-4-431-67891-5_4
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075

Motivation

A linear decision made with uncertain coefficients can be protected by requiring the constraint to hold for every coefficient vector in an uncertainty set. Choosing that set determines how conservative the decision is. Bertsimas and Brown connect this choice to a risk measure: a functional that assigns a cost to the random reward left by a decision. Their construction turns certain risk constraints into robust linear constraints over a convex hull of weighted samples. This mission isolates the structural question asked in §4.4 of their paper: which such risk measures always produce uncertainty sets that are centrally symmetric about the sample mean? The answer matters because this symmetric family is the class used in the paper's subsequent approximation of general polyhedral uncertainty sets. Bertsimas and Brown (2009), §§4.3–4.5.

Setting

There are $N\ge1$ observations, indexed by $i=1,\ldots,N$, with equal reference probabilities. A probability weight vector $q=(q_1,\ldots,q_N)$ has nonnegative entries summing to one. The restricted simplex $\widehat\Delta^N$ contains those vectors whose entries are nonincreasing: $q_1\ge\cdots\ge q_N$. For a reward vector $X=(x_1,\ldots,x_N)$, write $x_{(1)}\le\cdots\le x_{(N)}$ for its increasing order statistics. The associated distortion risk measure is $\mu_q(X)=-\sum_iq_i x_{(i)}$. A larger reward therefore reduces risk. Under the uniform distribution, the paper's Theorem 4.2 identifies these functionals, for $q\in\widehat\Delta^N$, with its distortion risk measures. Bertsimas and Brown (2009), Theorem 4.2.

Take arbitrary sample vectors $a_1,\ldots,a_N\in\mathbb R^n$. For a permutation $\sigma$ of their indices, form the weighted vector $\sum_iq_{\sigma(i)}a_i$. The $q$-permutohull $\Pi_q(\mathcal A)$ is the convex hull of all these vectors. Its center of interest is the sample mean $\widehat a=N^{-1}\sum_i a_i$. A set $P$ is centrally symmetric through $x_0\in P$ when $x_0+x\in P$ implies $x_0-x\in P$ for every $x$. The quantifier “for any data” ranges over every dimension $n$ and every choice of $N$ sample vectors. It is stronger than symmetry for one selected data set. Bertsimas and Brown (2009), Definitions 4.7–4.8.

Formalization targets

The first target is Proposition 4.1's characterization of weights giving universal symmetry. If $e_N$ is the vector with every entry $1/N$, then

$$\bigl[\Pi_q(\mathcal A)\text{ is centrally symmetric through }\widehat a \text{ for every }n,\mathcal A\bigr] \quad\Longleftrightarrow\quad \exists\sigma\in S_N:\ q=2e_N-q_\sigma.$$

This condition defines the symmetric restricted simplex $\widehat\Delta^N_{\mathrm{sym}}$ inside $\widehat\Delta^N$. Bertsimas and Brown (2009), Proposition 4.1 and Definition 4.9.

The main target is Theorem 4.4. Put $\widehat N=\lfloor N/2\rfloor+1$. For $1\le j\le\widehat N$, define a generator $\bar q^{\,j}$ by

$$\bar q_i^{\,j}= \begin{cases} 2/N,&i<j,\\ 1/N,&j\le i\le N-j+1,\\ 0,&\text{otherwise}. \end{cases}$$

A functional represented by a $q\in\widehat\Delta^N$ whose permutohull is symmetric for every data set is exactly a convex mixture of the $\widehat N$ generator functionals:

$$\mu(X)=\sum_{j=1}^{\widehat N}\lambda_j\mu_{\bar q^{\,j}}(X), \qquad \lambda_j\ge0,\qquad\sum_{j=1}^{\widehat N}\lambda_j=1.$$

The milestones also state the two set inclusions behind the equality of $\widehat\Delta^N_{\mathrm{sym}}$ with the convex hull of these generators, including the coordinate reversal identity. Bertsimas and Brown (2009), Theorem 4.4 and its proof.

Significance

The result gives a finite list of risk functionals from which every member of the universally symmetric distortion subclass can be formed. The number of generators is $\lfloor N/2\rfloor+1$, rather than an unspecified family. It also connects a geometric property of a robust uncertainty set to a checkable condition on its weights. The paper uses this symmetric subclass to formulate the inner approximation problem in §4.5, where a symmetric permutohull is fitted inside another polytope. Bertsimas and Brown (2009), §§4.4–4.5.

The mathematical result is proved in the 2009 paper. This formalization task is to obtain Lean proofs of the classification and its source-stated intermediate claims. The definition layer is a reusable interface for finite distortion risk measures, permutohulls, and symmetry under coordinate permutations. Formal proofs here would provide a checked foundation for later robust optimization statements using the same finite sample model. The proposed goal and milestones are open Lean statements; compiling them verifies their syntax and types, not their proofs.

Difficulty

Symmetry of one pictured polygon does not determine its weight vector. The hypothesis demands symmetry for every possible collection of sample vectors, so the converse in Proposition 4.1 must recover a relation among weights from a universal geometric property. Another difficulty is that the explicit generators change shape at the midpoint, and the odd and even cases have different middle ranges. The paper writes the calculation for odd $N$ and says the even case is analogous; the theorem itself makes no parity restriction. A proof therefore has to cover the even boundary, including the generator whose $1/N$ band is empty. Bertsimas and Brown (2009), Proposition 4.1 and proof of Theorem 4.4.

Formalization scope

The Lean sample space is Fin N, with $N>0$. Its indices start at zero; the prose and source formulas above start at one. The source's $\widehat N$ is N / 2 + 1 in natural numbers. Probability vectors use Mathlib's standard simplex together with antitone coordinate order. Permutohulls use convexHull of the finite permutation family, and order statistics use Tuple.sort. The reference distribution is uniform, as in the paper's Assumption 4.1. Real vector spaces of dimension zero are allowed because the claim quantifies over every dimension; the nonempty sample condition excludes division by zero.

The goal takes an arbitrary functional $\mu$ and requires an actual representation $\mu=\mu_q$ by a restricted-simplex weight. This is the paper's Theorem 4.2 parametrization of distortion risk measures, stated directly because that theorem is being drafted in a separate mission of the same series. Universal symmetry is derived from the data quantifier; it is not assumed as a condition on $q$. The generator mixture is likewise the conclusion, with its coefficients nonnegative and summing to one. Central symmetry includes membership of the center in the set.

Useful contributions include proofs of the source's permutation characterization, validity and symmetry of generator mixtures, and their converse spanning property. The definitions of finite probability weights and weighted permutation hulls can support further finite sample robust optimization results. The paper's inconsistent accent on the generator risk measure in Theorem 4.4 is read as the functional of the displayed generator vector; its intermediate sum on p. 1492 does not alter the stated normalized mixture.

Selected references

• Dimitris Bertsimas and David B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6), 1483–1495, 2009. DOI: 10.1287/opre.1080.0646.

Motivation

A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.

Setting

There are $m$ nests $M$ and $n$ products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$, and the products in each nest are ordered so that $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$. The weight of choosing no nest at all is $v_0 \ge 0$. If the assortment $S_i \subseteq N$ is offered in nest $i$, write

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j\in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \quad R_i(\emptyset) = 0 .$$

A customer picks nest $i$ with probability $Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l\in M} V_l(S_l)^{\gamma_l})$, and then a product of that nest by the multinomial logit model. The expected revenue is

$$\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i(S_1, \dots, S_m)\, R_i(S_i),$$

and problem (2) is $Z^* = \max_{S_i \subseteq N} \Pi(S_1, \dots, S_m)$.

The linear program (3) in the variables $(x, y_1, \dots, y_m)$ minimizes $x$ subject to

$$v_0 x \ge \sum_{i\in M} y_i, \qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big) \quad \forall S_i \subseteq N,\ i \in M.$$

Given candidate collections $\{A_{it} : t \in \mathcal T_i\}$ of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for $S_i$ in the collection of nest $i$.

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\hat x, \hat y)$ be an optimal solution of (4), and let $\hat S_i$ solve $\max_{S_i \in \{A_{it}\}} V_i(S_i)^{\gamma_i}(R_i(S_i) - \hat x)$, problem (5), in every nest. If $(\alpha \hat x, \beta \hat y)$ is feasible for (3) for some $\alpha, \beta$, then, with $\hat Z = \Pi(\hat S_1, \dots, \hat S_m)$,

$$\alpha \hat Z \ \ge\ Z^* \ \ge\ \hat Z .$$

The theorem fixes no candidate collection and no value of $\alpha$. Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.

Milestones (§2, pp. 11–12)

1. Problem (2) is equivalent to (3): $Z^*$ is the least $x$ for which some $y$ makes $(x, y)$ feasible for (3).
2. At an optimal solution of (4), the first constraint binds at the maximizers $\hat S_i$ of (5), and $\hat x = \Pi(\hat S_1, \dots, \hat S_m)$.
3. Problem (4) relaxes (3), so $\hat x \le Z^*$.

Companions (§7, pp. 29–30)

• The tighter program (16), which lets each nest's assortment be a fractional vector $z_i \in [0,1]^n$, has every feasible $x$ above $Z^*$.
• Proposition 13: $\hat F_i(x) = \max_{z_i \in [0,1]^n} F_i(z_i \mid x)$ is convex, with subgradient $-(v_{i0} + \sum_j v_{ij}\hat z_{ij}(x))^{\gamma_i}$ at $x$.

Significance

Theorem 1 is the common step behind the paper's four approximation guarantees: the factor $\rho$ or $2\kappa$ of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the $\delta^{2\bar\gamma+1}$ of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, $v_0 = 0$), and a formal proof certifies the framework once for every later instantiation.

Difficulty

The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective $\Pi \le x$ as a linear constraint. Both steps need care where a denominator $v_0 + \sum_i V_i(S_i)^{\gamma_i}$ can vanish. The binding argument for (4) is a perturbation argument: lowering $\hat x$ must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in $x$. The obvious one-line reading of Theorem 1, "$\hat x = \hat Z$ and $\alpha\hat x \ge Z^*$", is correct only once both of these facts are established with their hypotheses. In particular, it is false when $v_0 = 0$ (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of $F_i$ on $[0,1]^n$.

Formalization scope

Nests are a finite type ι and products are Fin n, indexed $0, \dots, n-1$. An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's $x / 0 = 0$ gives $R_i(\emptyset) = 0$. $Z^*$ is $\Pi(S^*)$ for an arbitrary optimal assortment $S^*$; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal $x$, and "$\hat S_i$ solves (5)" means $\hat S_i$ belongs to the collection of nest $i$ and maximizes the objective of (5) over it at $\hat x$.

Standing assumptions and pins. These are $v_0, v_{i0} \ge 0$ and ordered revenues, together with $v_{ij} > 0$, $r_{ij} \ge 0$ and $\gamma_i > 0$. The paper allows zero-weight padding products and $\gamma_i = 0$, but its own conventions fail there. Theorem 1 and the binding milestone add $v_0 > 0$. The page allows $v_0 = 0$, but then Theorem 1 is false: take one nest with $v_{10} = 0$, $\gamma_1 = 1$, $r_{11} = v_{11} = 1$ and candidates $\{\emptyset, \{1\}\}$. Then $\hat x = 1$ and $\hat S_1 = \emptyset$ meet every hypothesis with $\alpha = \beta = 1$, yet $\hat Z = 0 < Z^* = 1$. The equivalence of (2) and (3) and the bound from (16) keep $v_0 \ge 0$, as the page does, and assume at least one nest and one product: with neither and $v_0 = 0$, every $x$ is feasible for (3).

A formalization that assumes the binding equality, the identity $\hat x = \hat Z$, or the inequality $\hat x \le Z^*$ in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.

The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). https://doi.org/10.1287/opre.2014.1256
• D. McFadden, Econometric models of probabilistic choice, in C. Manski, D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981. https://eml.berkeley.edu/~mcfadden/discrete.html
• P. Rusmevichientong, D. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, Technical report, Cornell University, 2010. https://people.orie.cornell.edu/huseyin/publications/publications.html
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993. https://doi.org/10.1002/0471787779

Motivation

Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision $x$ is fixed before an uncertain right-hand side $b$ is revealed, and a second-stage decision $y(b)$ is chosen after it, as a function of $b$. The objective protects against the worst $b$ in an uncertainty set $\mathcal U$. Computing an optimal fully adaptable solution is intractable in general (Feige, Jain, Mahdian and Mirrokni, IPCO 2007), so practitioners restrict the second stage to affine policies $y(b)=Pb+q$, introduced in robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004). An optimal affine policy is computed by a single convex program, but its cost may exceed the adaptive optimum.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) quantify this loss. Earlier, Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved affine policies optimal for a class of one-dimensional multistage problems. The present paper shows that affine policies are optimal when $\mathcal U$ is a simplex (Theorem 1), that they can lose a factor $\Omega(m^{1/2-\delta})$ in general (Theorem 3), and — the subject of this mission — that when the first-stage constraint matrix is nonnegative they never lose more than $3\sqrt m$ (Theorem 4). Nonnegative first-stage matrices occur in network design, facility location, capacity planning and other covering problems.

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$, $d\in\mathbb R^{n_2}_+$, and let $\mathcal U\subseteq\mathbb R^m_+$ be convex, compact and full-dimensional. The problem $\Pi_{Adapt}(\mathcal U)$ is

$$z_{Adapt}(\mathcal U)=\min\; c^Tx+\max_{b\in\mathcal U}d^Ty(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge0,\ \ y(b)\ge0\quad\forall b\in\mathcal U,$$

where the minimum is over first-stage vectors $x$ and arbitrary maps $b\mapsto y(b)$. The problem is assumed feasible. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine second stages $y(b)=Pb+q$, which must still satisfy $Pb+q\ge0$ on $\mathcal U$.

For each coordinate $j$ put $\mu_j=\max\{b_j : b\in\mathcal U\}$ and fix a maximizer $\beta^j\in\mathcal U$ with $\beta^j_j=\mu_j$ (display (38)). The scaled sum of $b$ over an index set $J$ is $\sum_{j\in J}b_j/\mu_j$.

Algorithm $\mathcal A$ (Fig. 1 of the paper) starts with $J_1=\{1,\dots,m\}$ and $b^0=0$. While some $b\in\mathcal U$ has scaled sum over $J_1$ larger than $\sqrt m$, it picks a maximizer $u^k\in\mathcal U$ of that scaled sum, adds $u^k$ to the running vector on the coordinates of $J_1$, and moves to $J_2$ every coordinate $j$ whose running value has reached $\mu_j$. It returns the number of iterations $K$, the vectors $u^1,\dots,u^K$, their sum $\beta=u^1+\dots+u^K$, and the partition $J_1,J_2$.

In the $k$-uncertain variant (60)–(63), only $k$ right-hand sides $b\in\mathcal U\subseteq\mathbb R^k_+$ are uncertain and the remaining $m-k$ are fixed at $b^0$; all data are nonnegative. Its values are $z^k_{Adapt}(\mathcal U)$ and $z^k_{Aff}(\mathcal U)$.

Formalization targets

Goal: Theorem 4

If $A\ge0$ entrywise, then a feasible affine solution exists and

$$z_{Aff}(\mathcal U)\le 3\sqrt m\cdot z_{Adapt}(\mathcal U).$$

Milestones

1. $\mu_j>0$ for every $j$ (after (38)).
2. Lemma 9. For every complete run of Algorithm $\mathcal A$: $\sum_{j\in J_1}b_j/\mu_j\le\sqrt m$ for all $b\in\mathcal U$, and $b_j\le\beta_j$ for all $j\in J_2$ and $b\in\mathcal U$.
3. Lemma 10. Algorithm $\mathcal A$ executes at most $K\le2\sqrt m$ iterations.
4. Feasibility (48)–(55). For any feasible $(x^*,y^*)$, the solution $\tilde x=3\sqrt m\,x^*$, $\tilde y(b)=\sum_{j\in J_1}\frac{b_j}{\mu_j}y^*(\beta^j)+\hat y$ with $\hat y=\frac{2\sqrt m}{K}\sum_{k=1}^Ky^*(u^k)$ is feasible.
5. Cost (56)–(59). If $t$ bounds the worst-case cost of $(x^*,y^*)$, then $3\sqrt m\cdot t$ bounds that of $(\tilde x,\tilde y)$.

Companion results

• Algorithm $\mathcal A$ has a complete run when $\mathcal U$ is compact.
• Lemma 11. $z(\Pi_1)\le z^k_{Adapt}(\mathcal U)$ and $z(\Pi_2)\le z^k_{Adapt}(\mathcal U)$ for the uncertain and deterministic parts of the $k$-uncertain problem.
• Theorem 5. $z^k_{Aff}(\mathcal U)\le(3\sqrt k+1)\cdot z^k_{Adapt}(\mathcal U)$, the paper's $O(\sqrt k)$ bound with its proof's constant.
• Special case (39)–(45). If $\sum_{j=1}^m b_j/\mu_j\le\sqrt m$ on $\mathcal U$, then $z_{Aff}(\mathcal U)\le\sqrt m\cdot z_{Adapt}(\mathcal U)$.

Significance

Theorem 4 is an upper bound on the price of restricting to affine policies, and Theorem 3 of the same paper shows it is tight up to a constant factor: for every $\delta>0$ there are instances with $A\ge0$ where the gap is $\Omega(m^{1/2-\delta})$. Together they settle the order of the approximation ratio of affine policies for covering-type two-stage problems. Theorem 5 refines the bound to $O(\sqrt k)$ when only $k$ of the $m$ right-hand sides are uncertain, which is the regime of many applications. The construction is also the template for the paper's Theorem 6, a $4\sqrt m$-approximation for general $A$ obtained from a single dominating simplex.

The results are proved in the paper. To the knowledge of this mission, none of them has a machine-checked proof. Formalizing them produces a reusable model of two-stage adaptive linear programs with affine policies, a verified analysis of a greedy covering procedure (Algorithm $\mathcal A$), and an explicit-constant version of an $O(\cdot)$ statement.

Difficulty

The obvious attempt scales the fully adaptable solution at the extreme points $\beta^j$ linearly in $b$: $\tilde y(b)=\sum_j (b_j/\mu_j)\,y^*(\beta^j)$. This is feasible at cost factor $\sqrt m$ only when the scaled sums $\sum_j b_j/\mu_j$ stay below $\sqrt m$ on $\mathcal U$ (condition (39)); in general they can reach $m$, and the linear rule then costs a factor $m$. The difficulty is to handle the coordinates where $\mathcal U$ has large scaled mass. Algorithm $\mathcal A$ isolates them, and the delicate point is the iteration count: each round must add scaled mass above $\sqrt m$, while the total scaled mass that can be absorbed before every coordinate leaves $J_1$ is at most $2m$. A formal proof must also track the algorithm's state through its recursion, because the argmax choices are not unique and the statements must hold for every run.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, indices are 0-based, and matrices are Matrix (Fin m) (Fin n) ℝ. Nonnegativity of a matrix is stated entrywise. $z_{Adapt}$ and $z_{Aff}$ are infima of the set of worst-case cost bounds achieved by feasible solutions; the goal and Theorem 5 assert the existence of a feasible affine solution, which rules out the trivializing reading in which $z_{Aff}$ is the infimum of an empty set (Lean's junk value $0$) and the inequality holds for free. The goal does not mention $\mu$, $\beta^j$ or Algorithm $\mathcal A$; these appear only in milestones.

$\mu$ and $\beta^j$ are given with their defining properties ($\mu_j$ is the greatest value of $b_j$ on $\mathcal U$, and $\beta^j\in\mathcal U$ with $\beta^j_j=\mu_j$). Algorithm $\mathcal A$ is encoded as a recursion on a choice sequence $u$, with step 2(d) read as $J_1^k=\{j\in J_1^{k-1}: b^k_j<\mu_j\}$. A complete run requires the loop test and the argmax property at each iteration and the failure of the loop test at the end. The milestones on the constructed policy are stated for every feasible $(x^*,y^*)$ and every cost bound $t$, so that no attainment of the optimum is assumed.

Standing assumptions of (1) carried by the goal: $c,d\ge0$; $\mathcal U\subseteq\mathbb R^m_+$ convex, compact, with nonempty interior; feasibility. Milestones drop the ones they do not use. Theorem 5 carries compactness and full-dimensionality of $\mathcal U$, which §5.1 does not repeat but its proof uses through Theorem 4. Lemma 11 assumes that $z^k_{Adapt}(\mathcal U)$ is finite, since the paper's inequality is between extended reals.

A complete development needs: finite-dimensional linear programming facts (existence of optimal solutions is not needed), compactness arguments for the argmax in Algorithm $\mathcal A$, and manipulation of finite sums over Finset. The model of (1) and the analysis of Algorithm $\mathcal A$ are reusable by the companion mission on Theorem 6. Contributions of proofs of any milestone, and of supporting lemmas about the recursion of Algorithm $\mathcal A$, are welcome.

Selected references

• D. Bertsimas and V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer and A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu and P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010.
• U. Feige, K. Jain, M. Mahdian and V. Mirrokni, Robust combinatorial optimization with exponential scenarios, Lect. Notes Comput. Sci. 4513, 439–453, 2007.

Motivation

Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.

Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy $y(b) = Pb + q$, whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of $m+1$ affinely independent points of $\mathbb R^m_+$. Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.

Setting

Let $A \in \mathbb R^{m\times n_1}$, $B \in \mathbb R^{m\times n_2}$, $c \in \mathbb R^{n_1}_+$, $d \in \mathbb R^{n_2}_+$ and let $\mathcal U \subseteq \mathbb R^m_+$ be an uncertainty set. The problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ is

$$z_{\mathrm{Adapt}}(\mathcal U)=\min\ c^{T}x+\max_{b\in\mathcal U} d^{T}y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U .$$

Here $x$ is the first-stage decision and $y : \mathcal U \to \mathbb R^{n_2}$ is the second-stage policy; all inequalities between vectors are componentwise. The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum restricted to affine policies $y(b) = Pb + q$ with $P \in \mathbb R^{n_2\times m}$ and $q \in \mathbb R^{n_2}$; an affine policy must still satisfy $Pb + q \ge 0$ for every $b \in \mathcal U$. Always $z_{\mathrm{Adapt}}(\mathcal U) \le z_{\mathrm{Aff}}(\mathcal U)$.

The instance $\mathcal I$ of (6) is defined for $\delta > 0$ and an even integer $m > 200/\delta^2$. It has $n_1 = n_2 = m$, $c = 0$, $d = (1,\dots,1)^T$, $A = 0$, and

$$B_{ij}=\begin{cases}1,& i=j,\\ 1/\sqrt m,& i\ne j,\end{cases}\qquad \mathcal U=\operatorname{conv}\{b^0,b^1,\dots,b^{m+2}\},$$

where $b^0 = 0$, $b^j = e_j$ is the $j$-th unit vector for $j = 1,\dots,m$, $b^{m+1}$ has entries $1/\sqrt m$ in its first $m/2$ coordinates and $0$ in the others, and $b^{m+2}$ has $0$ in its first $m/2$ coordinates and $1/\sqrt m$ in the others. Thus $\mathcal U$ is generated by $m+2$ nonzero points. The last two are also extreme points when $m\ge 6$; for $m=2$ or $4$ they lie in the convex hull of $0,e_1,\dots,e_m$.

For a permutation $\tau$ of $\{1,\dots,m\}$, write $x^\tau = (x_{\tau(1)},\dots,x_{\tau(m)})$. A set $U$ is permutation-invariant with respect to $\tau$ if $x \in U \iff x^\tau \in U$ (Definition 2), and $\Gamma$ is the set (10) of permutations with $i \le m/2 \iff \tau(i) \le m/2$.

Formalization targets

Goal: Theorem 2

$$z_{\mathrm{Aff}}(\mathcal U)>(2-\delta)\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for the instance }\mathcal I\text{ of (6), every }\delta>0\text{ and every even }m>200/\delta^2 .$$

Milestones

1. Lemma 1. On $\mathcal I$ there is a feasible fully adaptable solution with worst-case cost $1$, so $z_{\mathrm{Adapt}}(\mathcal U) \le 1$.
2. Lemma 2. The set $\mathcal U$ of (6) is permutation-invariant with respect to every $\tau \in \Gamma$.
3. Lemma 3. There is an optimal affine solution $\hat y(b) = \hat Pb + \hat q$ whose intercept is constant: $\hat q_i = \hat q_j$ for all $i, j$.
4. First Claim of the proof of Theorem 2. For any feasible affine solution with intercept $\hat q \equiv \beta$ and worst-case cost at most $2-\delta$: $\beta \le (2-\delta)/m$.
5. Second Claim. Under the same assumption, $\hat P_{jj} \ge 1 - 2/\sqrt m - 2/m$ for every $j$.
6. Third Claim. Under the same assumption, $\hat P_{ij} \ge -(2-\delta)/m$ for all $i, j$.

Significance

Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach $2$. The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to $m^{1/2-\delta}$ for sets with polynomially many extreme points and prove a matching $O(\sqrt m)$ upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.

The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$, and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.

Difficulty

The upper bound $z_{\mathrm{Adapt}} \le 1$ requires a feasible policy, which can be written down. The lower bound on $z_{\mathrm{Aff}}$ is a statement about all affine policies, an $m^2 + m$ dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of $\Gamma$ and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most $2-\delta$ yields only $z_{\mathrm{Aff}} \ge 2-\delta$, not the strict inequality.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, $Bx$ is B *ᵥ x and $d^Ty$ is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate $i$ is index $i - 1$, so "$i \le m/2$" is (i : ℕ) < m / 2, with natural-number division (exact since $m$ is even). $x^\tau$ is x ∘ τ for τ : Equiv.Perm (Fin m).

$z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are the infima of the sets of real numbers $t$ for which some feasible (respectively feasible affine) solution satisfies $c^Tx + d^Ty(b) \le t$ for all $b \in \mathcal U$. This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value $0$, which is why Lemma 1 also asserts the existence of the feasible solution of cost $1$. Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on $\mathcal U$, as in (1).

The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional $\mathcal U \subseteq \mathbb R^m_+$, feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: $\delta > 0$, $m$ even and $m > 200/\delta^2$. For $\delta \ge 2$ the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most $2-\delta$, which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis $m > 200/\delta^2$. Definition 2 prints "$x \in P \iff x^\tau \in P$"; the formalization reads $P$ as the set $U$.

Replacing $z_{\mathrm{Aff}}$ by the cost of one particular affine policy, stating the goal with $\ge$, or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.

A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in $(x, P, q)$ with infinitely many constraints indexed by $\mathcal U$, reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with $\sqrt m$. Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A (online first 2011; received 31 Oct 2009, accepted 17 Jan 2011). https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444