Optimization

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$, control space $C$ and observation space $Z$; a discount factor $\alpha>0$; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$; a Borel state transition kernel $t(dx'\mid x,u)$; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$; and a horizon $N$. The initial state $x_0$ has distribution $p\in P(S)$, $z_0\sim s_0(\cdot\mid x_0)$, and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$, $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$. The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$, where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$, the cost

$$J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),$$

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$, for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$. The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$, constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$, costs $\hat g_k$ and transitions $\hat t_k$; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$. The initial distribution of $y_0$ is

$$\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).$$

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$.

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$,

$$J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),$$

and a Markov (PSI) policy that is optimal, $\varphi(p)$-optimal or weakly $\varphi(p)$-$\varepsilon$-optimal for (PSI) is respectively optimal, optimal at $p$, or $\varepsilon$-optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$-optimal (PSI) policy is $\varepsilon$-optimal for (ISI). Here $\hat\pi$ is weakly $q$-$\varepsilon$-optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$-optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

1. Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$.
2. Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$.
3. Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$.
4. Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
5. Proposition 10.4: $\varepsilon$-optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$.
6. Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$-average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$-optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$, while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$, so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

• Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$, $(N,\hat N)$, $(D,\hat D)$ are out of scope.
• Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ($\top-\top=\bot$) is never used where both terms can be infinite.
• Spaces and measures. $S$, $C$, $Z$, $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$-algebras; $P(S)$ carries the weak topology and the Giry $\sigma$-algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$; only stages $k<N$ are constrained.
• Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
• Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
• No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

Motivation

Many problems in machine learning and statistics are regularized empirical risk minimization: minimize an average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of $n$ loss terms, one per data point, plus a regularizer $\psi(x)$ such as $\lambda\|x\|_1$. When $n$ is large, a full gradient $\nabla f$ costs $n$ component gradients, so stochastic gradient methods that touch one $f_i$ per step are preferred. Variance-reduced methods (SVRG, SAGA) correct the stochastic gradient with a periodically recomputed full gradient and reach the rates of full-gradient descent at the cost of stochastic steps; accelerated full-gradient methods (Nesterov) improve the rate from $O(1/T)$ to $O(1/T^2)$ on convex problems.

Combining the two directly was open until Allen-Zhu's Katyusha (arXiv:1603.05953, STOC 2017, JMLR 2018). Before it, accelerated stochastic rates were obtained either for special structure (accelerated coordinate and dual methods, which need strong convexity or dual access) or through reductions such as Catalyst and APPA, which wrap a non-accelerated method in an outer proximal-point loop and lose logarithmic factors. Katyusha adds a third momentum term, the Katyusha momentum, that pulls each iterate back to the snapshot point, and obtains the accelerated rate directly. This mission concerns the paper's second main result: the variant Katyusha$^{\mathrm{ns}}$ (Algorithm 2) for objectives that are convex but not strongly convex.

Setting

Problem (1.1) of the paper is

$$\min_{x\in\mathbb R^d} F(x)=f(x)+\psi(x)=\frac1n\sum_{i=1}^n f_i(x)+\psi(x),$$

where $n\ge1$, each component $f_i:\mathbb R^d\to\mathbb R$ is convex and $L$-smooth, $\|\nabla f_i(x)-\nabla f_i(y)\|\le L\|x-y\|$, and the regularizer $\psi$ is convex. A point $x^*$ minimizes $F$.

Katyusha$^{\mathrm{ns}}(x_0,S,L)$ runs $S$ epochs of $m$ iterations each (the paper takes $m=2n$). It keeps three sequences $y_k$, $z_k$ and a snapshot $\widetilde x^s$, all starting at $x_0$, and fixes $\tau_2=\frac12$. Epoch $s$ uses the weight $\tau_{1,s}=\frac{2}{s+4}$ and the step $\alpha_s=\frac{1}{3\tau_{1,s}L}$, computes $\nabla f(\widetilde x^s)$ once, and performs, for $k=sm,\dots,sm+m-1$:

1. the coupling $x_{k+1}=\tau_{1,s}z_k+\tau_2\widetilde x^s+(1-\tau_{1,s}-\tau_2)y_k$;
2. the SVRG estimator $\widetilde\nabla_{k+1}=\nabla f(\widetilde x^s)+\nabla f_i(x_{k+1})-\nabla f_i(\widetilde x^s)$, with $i$ uniform in $\{1,\dots,n\}$, independent across iterations;
3. the mirror step $z_{k+1}=\arg\min_z\{\frac1{2\alpha_s}\|z-z_k\|^2+\langle\widetilde\nabla_{k+1},z\rangle+\psi(z)\}$;
4. the gradient step (Option I) $y_{k+1}=\arg\min_y\{\frac{3L}2\|y-x_{k+1}\|^2+\langle\widetilde\nabla_{k+1},y\rangle+\psi(y)\}$.

At the end of the epoch the new snapshot is the average $\widetilde x^{s+1}=\frac1m\sum_{j=1}^m y_{sm+j}$. The output is $\widetilde x^S$. Throughout, $D_k=F(y_k)-F(x^*)$ and $\widetilde D^s=F(\widetilde x^s)-F(x^*)$.

Formalization targets

Goal: Theorem 4.1 with the constants of its proof

$$\mathbb E\big[F(\widetilde x^S)\big]-F(x^*)\le\frac{16\,\big(F(x_0)-F(x^*)\big)}{(S+3)^2}+\frac{12\,L\,\|x_0-x^*\|^2}{m\,(S+3)^2}\qquad(S\ge0,\ m\ge1).$$

The paper states $O\big(\frac{F(x_0)-F(x^*)}{S^2}+\frac{L\|x_0-x^*\|^2}{mS^2}\big)$; the explicit form above is what its proof in Appendix C.1 establishes.

Milestones, in the order of the proof

1. Lemma 2.7 for $\sigma=0$: the one-iteration inequality coupling $D_k$, $\mathbb E[D_{k+1}]$, $\widetilde D$ and the distances $\|z_k-x^*\|^2$, $\mathbb E\|z_{k+1}-x^*\|^2$.
2. (C.1): Lemma 2.7 summed over one epoch.
3. (C.2): the epoch inequality for $s\ge1$, after inserting the average snapshot and $\alpha_s=1/(3\tau_{1,s}L)$.
4. (C.3): the same for the base epoch $s=0$.
5. The parameter inequalities $\frac1{\tau_{1,s}^2}\ge\frac{1-\tau_{1,s+1}}{\tau_{1,s+1}^2}$ and $\frac{\tau_{1,s}+\tau_2}{\tau_{1,s}^2}\ge\frac{\tau_2}{\tau_{1,s+1}^2}$.
6. (C.4): the bound telescoped over $S$ epochs.

Significance

Theorem 4.1 gives the accelerated $O(1/S^2)$ rate for non-strongly convex composite finite sums with a direct method: $\varepsilon$ error after $O\big(\frac{n\sqrt{F(x_0)-F(x^*)}}{\sqrt\varepsilon}+\frac{\sqrt{nL}\,\|x_0-x^*\|}{\sqrt\varepsilon}\big)$ stochastic gradient evaluations, a factor $S$ better than the $O(1/S)$ of non-accelerated variance-reduced methods such as SAGA (Remark 4.2). The non-strongly convex case covers $\ell_1$-regularized and unregularized convex losses, where no strong-convexity parameter is available to tune a linear-rate method.

The result is proved in the paper; no machine-checked proof of Katyusha or Katyusha$^{\mathrm{ns}}$ is known to exist. The mission produces a formal statement of the algorithm and its rate with explicit constants, and a formal chain of the paper's intermediate inequalities. A SAGA mission on this platform states SAGA's non-accelerated $O(1/k)$ rate for the same problem class, so the two results become directly comparable in Lean.

Difficulty

Each step uses only convexity, smoothness and the optimality of proximal points, but the steps interlock. The variance of $\widetilde\nabla_{k+1}$ cannot be bounded by $F(\widetilde x)-F(x^*)$ as in SVRG's analysis without losing acceleration; the paper's bound (Lemma 2.4) leaves a linear term $\langle\nabla f(x_{k+1}),\widetilde x-x_{k+1}\rangle$ that is cancelled only by the specific weight $\tau_2=\frac12$ of the Katyusha momentum (Lemmas 2.6–2.7). Without strong convexity the per-epoch inequalities do not contract, so the proof must telescope across epochs with epoch-dependent weights $\tau_{1,s}$: the coefficients of $D_{sm+j}$ produced by epoch $s$ must dominate those consumed by epoch $s+1$, and the snapshot term $m\widetilde D^s$ must be charged to the previous epoch's iterates. Getting the boundary epoch $s=0$ (whose snapshot is $x_0$) and the last epoch right is where the constants come from.

Formalization scope

The Lean development works on EuclideanSpace ℝ (Fin d) with components indexed by Fin n ($n\ge1$). Gradients are given functions $\nabla f_i$ tied to $f_i$ by HasGradientAt; $L$-smoothness is the Lipschitz bound on them with $L>0$; convexity is ConvexOn ℝ Set.univ. $f$ and $\nabla f$ are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The regularizer $\psi$ is real-valued and convex, so extended-valued regularizers such as indicator functions of constraint sets are not covered. The two arg-min steps are evaluated through a map $P$ assumed to return a proximal point of $\psi$ (the published SAGA.Convex.IsProxPoint) for every positive step; for real-valued convex $\psi$ such points exist and are unique, so the hypothesis is satisfiable. $x^*$ is assumed to minimize $F$ (without strong convexity a minimizer need not exist). Randomness is modelled by finite sequences of indices: the expectation is the uniform average over all index sequences (SAGA.Convex.expectIdx), with the $Sm$ indices split into epochs by Mathlib's finProdFinEquiv.

Conventions committed to:

• Explicit constants for O(·). The goal's $O(\cdot)$ is instantiated as $16\,(F(x_0)-F(x^*))/(S+3)^2+12L\|x_0-x^*\|^2/(m(S+3)^2)$: the proof bounds $\widetilde D^S$ by $\frac{2\tau_{1,S-1}^2}{m}$ times the right-hand side of (C.4), which equals $2m\,(F(x_0)-F(x^*))+\frac{3L}2\|x_0-x^*\|^2$, with $\tau_{1,S-1}=\frac2{S+3}$. The bound holds trivially at $S=0$, so the goal is stated for all $S$.
• Epoch length. $m\ge1$ is a parameter (the algorithm sets $m=2n$); every statement holds for every $m\ge1$.
• Option I only; the unused input $\sigma$ and Option II are not modelled.
• Lemma 2.7 is stated for $\sigma=0$ with the paper's implicit side conditions $\alpha>0$, $0<\tau_1\le\frac12$.
• (C.2) is stated for an epoch $s\ge1$ whose snapshot is the average of given previous iterates; (C.1) and (C.3) are stated from an arbitrary epoch start state, which is the paper's "the randomness in the first $s-1$ epochs is fixed".
• The typo $\|z_{Sm}-z^*\|^2$ in (C.4) is read as $\|z_{Sm}-x^*\|^2$.

A trivializing formalization is ruled out: the prox map, the gradients and $x^*$ are all tied to $\psi$, $f_i$ and $F$ by hypotheses that a quadratic instance satisfies, and the expectation averages over every index sequence rather than a chosen one. The iteration count stated "in other words" after Theorem 4.1 is not a target.

Contributions welcome: proofs of the milestones in any order; general lemmas about proximal points of convex functions (the three-point inequality behind Lemma 2.5) and the co-coercivity of convex $L$-smooth functions (behind Lemma 2.4) are reusable beyond this mission.

Selected references

• Z. Allen-Zhu, Katyusha: The First Direct Acceleration of Stochastic Gradient Methods, STOC 2017; JMLR 18(221), 2018. arXiv:1603.05953v6. https://arxiv.org/abs/1603.05953
• A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NeurIPS 2014. https://arxiv.org/abs/1407.0202
• R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NeurIPS 2013. https://papers.nips.cc/paper/4937
• Y. Nesterov, Introductory Lectures on Convex Programming, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

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

Motivation

Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision $x$ is fixed before an uncertain parameter is revealed, and a second-stage decision $y(b)$ is chosen after the parameter $b$ is observed, so that the second stage may depend on $b$ arbitrarily. The objective is the worst case over an uncertainty set $\mathcal U$ of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.

Optimizing over all functions $y(\cdot)$ is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in $b$ with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) $y(b)=Pb+q$; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.

Timeline of the relevant results:

• 2004. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduce affinely adjustable robust counterparts and show that the best affine policy is tractable for many uncertainty sets (doi:10.1007/s10107-003-0454-y).
• 2010. Bertsimas, Iancu and Parrilo prove that affine policies are optimal for a class of multistage robust problems with one-dimensional uncertainty per stage and box uncertainty sets (doi:10.1287/moor.1100.0444).
• 2012. Bertsimas and Goyal, the source of this mission, prove that an affine policy is optimal for model (1) whenever $\mathcal U$ is a simplex (Theorem 1), and show that this exactness breaks down for slightly larger sets (doi:10.1007/s10107-011-0444-4).

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$ and $d\in\mathbb R^{n_2}_+$. The problem $\Pi_{Adapt}(\mathcal U)$ of model (1) 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\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U,$$

where inequalities between vectors are componentwise. A pair $(x,y)$ satisfying the constraints is feasible; its worst-case cost is $c^Tx+\max_{b\in\mathcal U}d^Ty(b)$. A feasible pair is optimal when its worst-case cost equals $z_{Adapt}(\mathcal U)$, and an affine policy is a second stage of the form $y(b)=Pb+q$ with $P\in\mathbb R^{n_2\times m}$, $q\in\mathbb R^{n_2}$, still required to be nonnegative on $\mathcal U$. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine policies.

A simplex in $\mathbb R^m$ is the convex hull

$$\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$$

of $m+1$ affinely independent points, that is, points for which $b^1-b^{m+1},\dots,b^m-b^{m+1}$ are linearly independent. The proof works with the $m\times m$ matrix $Q=[(b^1-b^{m+1})\cdots(b^m-b^{m+1})]$, the matrix $Y=[(y^*(b^1)-y^*(b^{m+1}))\cdots(y^*(b^m)-y^*(b^{m+1}))]$ of display (2), and the affine rule $\tilde y(b)=YQ^{-1}(b-b^{m+1})+y^*(b^{m+1})$. In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.

Formalization targets

Goal: Theorem 1

If $\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$ with affinely independent $b^j\in\mathbb R^m_+$ and $\Pi_{Adapt}(\mathcal U)$ is feasible, then there exist $\hat x$, $P\in\mathbb R^{n_2\times m}$ and $q\in\mathbb R^{n_2}$ such that

$$(\hat x,\ \hat y),\qquad \hat y(b)=Pb+q\ \ (b\in\mathcal U),$$

is an optimal solution of $\Pi_{Adapt}(\mathcal U)$, optimal among all (not only affine) two-stage solutions. In particular $z_{Aff}(\mathcal U)=z_{Adapt}(\mathcal U)$.

Milestones

The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:

1. $Q$ is invertible (PDF p. 6).
2. For $b=\sum_j\alpha_jb^j$ with $\sum_j\alpha_j=1$: $Q^{-1}(b-b^{m+1})=(\alpha_1,\dots,\alpha_m)^T$ (PDF p. 6).
3. $\tilde y\big(\sum_j\alpha_jb^j\big)=\sum_j\alpha_j\,y^*(b^j)$ (PDF pp. 6–7).
4. Displays (3)–(5): for any feasible $(x^*,y^*)$, the pair $(x^*,\tilde y)$ is feasible and every bound on the worst-case cost of $(x^*,y^*)$ also bounds that of $(x^*,\tilde y)$ (PDF p. 7).

Significance

The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix $A$ and $B$ and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with $m+3$ extreme points the best affine policy can already be worse by a factor $2-\delta$, and that on sets with exponentially many extreme points the gap can be $\Omega(m^{1/2-\delta})$; Section 6 uses a dominating simplex, on which affine policies are exact, to build an $O(\sqrt m)$-approximation for general $\mathcal U$. The theorem also says that on a simplex the whole adaptive problem reduces to $m+1$ scenario copies of a linear program.

Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.

Difficulty

Two steps are not routine to formalize. First, the paper starts from "an optimal solution $x^*,y^*(b)$", that is, it assumes the minimum in (1) is attained. Over arbitrary functions $y(\cdot)$ this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of $m+1$ points to invertibility of the $m\times m$ matrix $Q$, and the identity $Q^{-1}(b-b^{m+1})=\alpha$ requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing $z_{Aff}$ and $z_{Adapt}$ as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.

Formalization scope

Vectors in $\mathbb R^m$ are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at $1$, Lean's at $0$: $b^j$ is v (j-1) and $b^{m+1}$ is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of $\mathcal U$ is the hypothesis that all $m+1$ vertices are nonnegative (the page writes $j=1,\dots,m$, a slip for $m+1$). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values $z_{Adapt}$ and $z_{Aff}$ are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.

The goal must not be replaced by $z_{Aff}(\mathcal U)\le z_{Adapt}(\mathcal U)$, by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention $Q$, $Y$ or the interpolant.

A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. doi:10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. doi:10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010. doi:10.1287/moor.1100.0444
• A. Bemporad, F. Borrelli, M. Morari, Min–max control of constrained uncertain discrete-time linear systems, IEEE Trans. Autom. Control 48(9), 1600–1606, 2003. doi:10.1109/TAC.2003.816984