Optimization

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

• 1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
• 1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
• 2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
• 2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

$$\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}$$

with $x\in\mathbb{R}^n$, $E\in\mathbb{R}^{p\times n}$, $A=(a_{ij})\in\mathbb{R}^{m\times n}$, and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$, $u_j\in\mathbb{R}\cup\{+\infty\}$. For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$, $j\in J_i$. Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$, write $b_i^+=b_i+\delta\max[1,|b_i|]$.

• $x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$.
• In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$, where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$, $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$.
• $x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$.

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$, has variables $x_j$, $y_{ij}$, $z_{ij}$ and constraints $Ex=e$, $Ax\le b$, $\ell\le x\le u$, $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$, and

$$\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.$$

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$, besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$.

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$,

$$\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.$$

Milestones

1. The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$.
2. Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$,

$$\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.$$

3. $x$ is reliable iff it is feasible for (∗) (p. 417).
4. (∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
5. Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$, $z_{ij}=0$ (p. 420).
6. Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$, $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$, suffices to extend $x$ to (RC) (p. 420).
7. The ratio $\alpha_i(x)/\beta_i(x)$, $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$, is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$, with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$.

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$, not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

• Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
• The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$. Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
• The hypotheses $\epsilon>0$, $\delta>0$, $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
• Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$, $x_i-y_{ij}$ and $y_j$, $y_{ij}$; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed "$\sqrt{\mathrm{card}(J_i)}$" omits.
• Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$, never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
• The numerical remarks of the paper (0.92, 5.24, $10^{-6}$, "at least 30") and the NETLIB case study are not formalized.
• Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
• D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Statistical learning theory asks when a rule that sees only an i.i.d. sample $z_1,\dots,z_m$ from an unknown distribution $D$ can return a hypothesis whose expected loss is close to the best possible. In supervised classification the classical answer is uniform convergence: learnability holds exactly when empirical risks converge to expected risks uniformly over the hypothesis class, and then empirical risk minimization (ERM) learns. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) showed that in Vapnik's broader General Learning Setting this picture breaks down. Their motivating example is stochastic convex optimization in a Hilbert space: minimizing an expected convex, Lipschitz objective over a bounded convex set from samples. This problem underlies regularized linear prediction, kernel methods and online-to-batch conversions, and the paper shows (§4.1) that in infinite dimension uniform convergence can fail and the plain empirical minimizer can fail to converge, while the problem is still learnable.

This mission formalizes the positive half of that example: Tikhonov-regularized ERM learns every such problem, with an explicit bound holding with probability $1-\delta$ (Theorem 3, p. 2644), through the stability of strongly convex empirical minimization (Theorem 2).

Setting

Let $Z$ be a measurable space of instances and $E$ a real Hilbert space. A stochastic convex optimization problem consists of a nonempty, closed, convex, bounded set $\mathcal H\subseteq E$ and an objective $f:E\times Z\to\mathbb R$ such that for every $z$ the map $h\mapsto f(h;z)$ is convex and $L$-Lipschitz on $\mathcal H$, each $f(h;\cdot)$ is measurable, and $|f(h;z)|\le C$ on $\mathcal H\times Z$. For a distribution $D$ on $Z$ define the risk and optimal risk

$$F(h)=\mathbb E_{z\sim D}[f(h;z)],\qquad F^*=\inf_{h\in\mathcal H}F(h),$$

and for a sample $S=(z_1,\dots,z_m)\sim D^m$ the empirical risk $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$. A function $g$ is $\lambda$-strongly convex on $\mathcal H$ if $g-\frac\lambda2\|\cdot\|^2$ is convex there. The regularized empirical minimizer is

$$\hat h_\lambda\in\operatorname*{arg\,min}_{h\in\mathcal H}\Big(F_S(h)+\frac\lambda2\|h\|^2\Big).\tag{5}$$

For the general part, a learning rule $A$ maps samples to hypotheses; it is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-\inf_hF_S(h)]\le\varepsilon_{\mathrm{erm}}(m)$, consistent with rate $\varepsilon_{\mathrm{cons}}$ if $\mathbb E[F(A(S))-F^*]\le\varepsilon_{\mathrm{cons}}(m)$, and uniform-RO stable with rate $\varepsilon_{\mathrm{stable}}$ if replacing any one sample point changes the loss at any test point by at most $\varepsilon_{\mathrm{stable}}(m)$ on average over the replaced index (Definition 4).

Formalization targets

Goal: Theorem 3

If $\|h\|\le B$ on $\mathcal H$, $L,B>0$, $\delta\in(0,1)$, $m\ge1$ and $\lambda=\sqrt{16L^2/(\delta B^2m)}$, then with probability at least $1-\delta$ over $S\sim D^m$

$$F(\hat h_\lambda)-F^*\ \le\ 4\sqrt{\frac{L^2B^2}{\delta m}}\Big(1+\frac8{\delta m}\Big).$$

The constants are the paper's.

Milestones, in the order the proof uses them

1. Quadratic growth at a minimizer of a $\lambda$-strongly convex $g$: $g(h')-g(h)\ge\frac\lambda2\|h'-h\|^2$ (§4.2, p. 2644).
2. Eq. (6): if $f(\cdot;z)$ is $\lambda$-strongly convex and $L$-Lipschitz, empirical minimizers of $S$ and of $S^{(i)}$ satisfy $|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)$ for all $z$ (p. 2645).
3. Theorem 8: a uniform- or average-RO stable AERM is consistent with rate $\varepsilon_{\mathrm{stable}}+\varepsilon_{\mathrm{erm}}$ and generalizes with rate $\varepsilon_{\mathrm{stable}}+2\varepsilon_{\mathrm{erm}}+2C/\sqrt m$ (p. 2649).
4. $\mathbb E_{S\sim D^m}[F(\hat h_S)-F^*]\le 4L^2/(\lambda m)$ for the strongly convex empirical minimizer (p. 2645).
5. Theorem 2: with probability $1-\delta$, $F(\hat h_S)-F^*\le 4L^2/(\delta\lambda m)$ (p. 2644).
6. Theorem 2 applied to $r(h;z)=\frac\lambda2\|h\|^2+f(h;z)$: with probability $1-\delta$, $\frac\lambda2\|\hat h_\lambda\|^2+F(\hat h_\lambda)\le\inf_h\big(\frac\lambda2\|h\|^2+F(h)\big)+4(L+\lambda B)^2/(\delta\lambda m)$ (p. 2645).

Significance

The result. Theorem 3 shows that every convex, Lipschitz, bounded stochastic optimization problem over a bounded subset of a Hilbert space is learnable at rate $O(LB/\sqrt{\delta m})$, with no dimension dependence and no uniform convergence. Together with the counterexamples of §4.1 it separates learnability from uniform convergence and from ERM, and it motivates the paper's general characterization: a problem is learnable if and only if it admits a uniform-RO stable asymptotic empirical risk minimizer (Theorem 7). Theorem 8 is the sufficiency half of that characterization and is reused wherever stability arguments give generalization bounds.

Formalizing it. The results are proved in the paper; to our knowledge none has a machine-checked proof. The closest platform material is the textbook treatment in Understanding Machine Learning, chapter 13 (Shalev-Shwartz and Ben-David): Corollary 13.9 (UnderstandingML.convex_lipschitz_bounded_learnable), Corollary 13.6 (rlm_lipschitz_stable) and Lemma 13.5 (strongly_convex_lemma). Those are stated in $\mathbb R^d$, bound the risk in expectation, use the regularizer $\lambda\|w\|^2$ over all of $\mathbb R^d$, and have different constants; the present mission works in an arbitrary Hilbert space, over a constraint set $\mathcal H$, with high-probability bounds and the paper's constants. Its definitions of learning rules, AERM, consistency and replace-one stability in the General Learning Setting are reusable by the other missions of this series.

Difficulty

The obvious route, bounding $\sup_{h\in\mathcal H}|F(h)-F_S(h)|$, is unavailable: §4.1 exhibits problems of exactly this type in which that supremum stays bounded away from zero for every sample size. Any successful argument therefore has to rely on a property of the learning rule rather than of the class $\mathcal H$, and the plain empirical minimizer does not have it: §4.1 shows it can stay a constant away from $F^*$ at every sample size. A second difficulty is purely formal: the regularization parameter $\lambda$ depends on $\delta$ and $m$, so the regularized minimizer changes with them, and all expectations involve a data-dependent hypothesis in a possibly non-separable Hilbert space, where measurability is not automatic.

Formalization scope

Lean conventions, fixed for every item:

• $E$ is a real inner product space with CompleteSpace E, never assumed finite-dimensional; $\mathcal H$ is Hset : Set E, and all infima, suprema, strong convexity and Lipschitz conditions are taken on Hset only. $F^*$ is ⨅ h : Hset, F h.
• Samples are Fin m → Z, $D^m$ is Measure.pi, $S^{(i)}$ is Function.update S i z', and $m\ge1$ throughout.
• The paper's standing loss bound $|f|\le B$ (p. 2637) is named $C$, because Theorem 3 uses $B$ for the norm bound $\|h\|\le B$. $L>0$ and $B>0$ are implicit in Theorem 3's choice of $\lambda$ and are stated.
• Strong convexity is Mathlib's StrongConvexOn Hset λ, which is the paper's definition.
• Minimizers are selections $S\mapsto\hat h_S\in\mathcal H$ satisfying the minimization property; the theorems hold for every such selection, hence for the minimizer, which is unique by strong convexity.
• Measurability, not discussed in the paper, is the series' single standing convention: each $f(h;\cdot)$ is measurable and the selection makes $(S,z)\mapsto f(\hat h_S;z)$ jointly measurable; for Theorem 8, the rule is measurable in the same sense and $S\mapsto\inf_hF_S(h)$ is measurable.
• "With probability at least $1-\delta$" is the bound $D^m\{\text{failure}\}\le\delta$ with $0<\delta<1$.

No statement of the paper is corrected: all printed constants were checked against the proofs and are reproduced exactly.

A formalization in which the expected excess risk is a Bochner integral of a non-measurable or non-integrable function, or in which $F^*$ is an infimum over all of $E$ or over an unbounded family, would make the bounds trivially true; the measurability hypotheses, the bound $|f|\le C$ and the infimum over the nonempty set $\mathcal H$ rule this out.

Contributions welcome: proofs of the milestones in order, and in particular a reusable replace-one identity $\mathbb E[F_S(A(S))]=\frac1m\sum_i\mathbb E[f(A(S^{(i)});z'_i)]$ under Measure.pi, and Markov's inequality in the form used for high-probability bounds.

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Stochastic Convex Optimization, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/018.pdf
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, chapter 13. https://doi.org/10.1017/CBO9781107298019
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

Motivation

A Markov decision process (MDP) is solved by dynamic programming once its transition probabilities are known. In practice they are estimated from data, and the optimal policy of an MDP can be sensitive to estimation error: a policy computed from point estimates may perform much worse under the true transition matrices. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) study the robust version of the problem, in which the controller minimises the worst-case expected cost when the transition matrices are only known to lie in given uncertainty sets, and motivate it with aircraft routing under uncertain weather.

Earlier work on MDPs with uncertain transition probabilities includes Satia and Lave (1973) and White and Eldeib (1994), which treat interval and set-valued transition models, and Givan, Leach and Dean (1997) on bounded-parameter MDPs. The robust Bellman recursion under a rectangularity assumption was obtained independently by Iyengar (Columbia technical report 2002, published as Robust dynamic programming, Math. Oper. Res. 30(2), 2005). This mission targets the finite-horizon result of Nilim and El Ghaoui: Theorem 1, which shows that the robust problem is solved by a recursion of the same shape as the nominal one and that the associated min–max game has a value.

Setting

The states form a finite set $\mathcal X=\{1,\dots,n\}$, the decision horizon is $T=\{0,1,\dots,N-1\}$, and the action set $\mathcal A$ is finite, nonempty and the same in every state. Costs are $c_t(i,a)\ge0$ for $t\in T$, and there is a terminal cost $c_N(i)$. The system starts in a given state $i_0$.

Write $\Delta_n=\{p\in\mathbb R^n_+ : p^{\mathsf T}\mathbf 1=1\}$ for the probability simplex. For every action $a$ and state $i$, a nonempty set $\mathcal P_i^a\subseteq\Delta_n$ describes the possible $i$-th rows of the transition matrix under $a$. No convexity or closedness is assumed. The rectangular uncertainty property says the uncertainty set of the matrix $P^a$ is the product $\mathcal P^a=\mathcal P_1^a\times\cdots\times\mathcal P_n^a$.

A controller policy $\pi=(\mathbf a_0,\dots,\mathbf a_{N-1})$ consists of maps $\mathbf a_t:\mathcal X\to\mathcal A$, and $\Pi=\mathcal A^{nN}$ is the set of such policies. A policy of nature $\tau=(P_t^a)_{a\in\mathcal A,t\in T}$ picks, for every stage, action and state, a row $p_i^a(t)\in\mathcal P_i^a$. The admissible set is $\mathcal T=(\bigotimes_a\mathcal P^a)^N$, so nature may change the matrices from stage to stage. The expected total cost is

$$C_N(\pi,\tau)=\mathbf E\Big(\sum_{t=0}^{N-1}c_t(i_t,\mathbf a_t(i_t))+c_N(i_N)\Big),$$

where the state $i_t$ evolves as a Markov chain with transition matrix $P_t^{\mathbf a_t(i)}$ from state $i$. The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v)=\sup\{p^{\mathsf T}v : p\in\mathcal P\}$. The robust recursion (7) starts from $v_N=c_N$ and sets

$$v_t(i)=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\big),$$

and for a fixed $\pi$ the evaluation recursion (10) starts from $v_N^\pi=c_N$ and sets $v_t^\pi(i)=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v_{t+1}^\pi)$.

Formalization targets

Goal: Theorem 1 (Robust Dynamic Programming)

$$\min_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0(i_0)=\sup_{\tau\in\mathcal T}\min_{\pi\in\Pi}C_N(\pi,\tau),$$

together with three further statements. First, $\sup_{\tau}C_N(\pi,\tau)=v_0^\pi(i_0)$ for every $\pi$. Second, every policy that chooses actions attaining the minimum in (7) (rule (8)) achieves $v_0(i_0)$ in the worst case. Third, every nature policy whose rows attain the suprema $\sigma_{\mathcal P_i^a}(v_{t+1})$ (rule (9)) forces the value $v_0(i_0)$ on every controller.

Milestones

1. Lemma 1: a problem $\max q^{\mathsf T}v_0$ subject to $v_t\le g_t(v_{t+1})$ with monotone $g_t$ and $q\ge0$ is solved by the recursion $v_t=g_t(v_{t+1})$.
2. Support functions of nonempty subsets of $\Delta_n$ are componentwise nondecreasing.
3. The constraint maps of problems (15) and (16) are componentwise nondecreasing.
4. Eq. (14): for fixed $\pi$ and fixed matrices, $C_N(\pi,\tau)$ is the value of a linear program.
5. Eq. (16): $\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0^\pi(i_0)$.
6. Eq. (15): $\sup_{\tau\in\mathcal T}\min_{\pi}C_N(\pi,\tau)=v_0(i_0)$.

Significance

Theorem 1 shows that, under rectangular uncertainty, robustness costs one inner optimisation per state and action: the expected continuation cost $p^{\mathsf T}v_{t+1}$ of nominal dynamic programming is replaced by the support function $\sigma_{\mathcal P_i^a}(v_{t+1})$. The equality of the min–max and max–min values says that it does not matter whether nature commits before or after the controller. The optimal controller policy remains deterministic and Markov. The later sections of the paper build on this recursion. They cover the discounted infinite-horizon case, the gap between stationary and time-varying uncertainty, and the computation of $\sigma$ for likelihood and entropy models, which the other missions of this series formalize.

The result is proved in the paper, and independently by Iyengar. It has no machine-checked proof that this mission is aware of. A formal proof yields a reusable development: a finite-horizon MDP with a forward-defined expected cost, the link between that expectation and backward linear programs, and the finite-horizon robust Bellman equation for arbitrary nonempty uncertainty sets.

Difficulty

The nominal Bellman recursion is standard. The robust statement is harder than "apply the nominal recursion under the worst matrix", because no single worst matrix need exist. The sets $\mathcal P_i^a$ are neither closed nor convex, so the suprema in $\sigma$ need not be attained, and $\mathcal T$ is not compact. Minimax theorems for convex–concave or compact games therefore do not apply. The expected cost is defined forward, as an expectation over a Markov chain, while the recursions run backward, and connecting the two is part of the work. The max–min side needs nature policies that come within any tolerance of the value simultaneously at every stage, state and action.

Formalization scope

• States are Fin n and stages Fin N. Values $v_0,\dots,v_N$ are indexed by natural numbers, and only $t\le N$ is meaningful. Vectors are Fin n → ℝ with the componentwise order.
• The model is a structure holding the costs ($c_t\ge0$), the terminal cost (no sign assumed), and the row sets. Every row set must be nonempty and contained in stdSimplex ℝ (Fin n). Nonemptiness is implicit in the paper: without it $\mathcal T$ is empty, and a real supremum over an empty index is $0$.
• Rectangularity is built in: a nature policy is a function $\tau(t,a,i)$ with $\tau(t,a,i)\in\mathcal P_i^a$. Nature does not observe the realised trajectory, and stationary nature ($\mathcal T_s$) is not the set used here.
• $C_N$ is defined by the forward state distribution, not by a backward recursion. Defining it backward would make the evaluation statements hold by definition, which is the trivializing formalization this choice rules out.
• $\sigma_{\mathcal P}$ is the real sSup of $\{p^{\mathsf T}v\}$. This is the true supremum because the set is nonempty and bounded above by $\max_j v_j$.
• Maxima over nature are suprema: ⨆ τ in the goal and IsLUB in the milestones, because the row sets need not be closed. Minima over the finite nonempty $\Pi$ and over $\mathcal A$ are ⨅. The argmax rule (9) is stated only for nature policies attaining the row suprema. The argmin rule (8) is stated for every attaining policy.
• The terminal value $v_N=c_N$ is not printed in Theorem 1. It is taken from the proof and from Step 1 of the paper's algorithm (p. 785). The composition $g_1\circ\cdots\circ g_N$ in Lemma 1 is read as $g_0\circ\cdots\circ g_{N-1}$.
• Not included: Corollary 1 (the sequential game) and the accuracy part of Theorem 2. Contributions of either as additional theorems on these definitions are welcome.

Selected references

• A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• C. C. White, H. K. Eldeib, Markov Decision Processes with Imprecise Transition Probabilities, Operations Research 42(4):739–749, 1994. https://doi.org/10.1287/opre.42.4.739
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

High-dimensional statistics studies estimation when the number of parameters $p$ is comparable to, or larger than, the number of observations $n$. The standard estimators in this regime are regularized M-estimators: minimise an empirical loss plus a penalty that encodes structure, such as the Lasso ($\ell_1$ penalty, sparse vectors), the group Lasso (block norms, group sparsity) and nuclear-norm regularization (low-rank matrices). Before 2009 each of these estimators came with its own consistency proof. Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731; Statistical Science 27(4), 2012, doi:10.1214/12-STS400) isolated two properties that these proofs share, decomposability of the regularizer and restricted strong convexity of the loss, and proved one deterministic theorem from them. The Lasso rates of Bickel, Ritov and Tsybakov (arXiv:0801.1095), rates under $\ell_q$-sparsity, and group-sparse and low-rank rates then follow as corollaries. The framework is the organising principle of Chapter 9 of Wainwright's textbook High-Dimensional Statistics (Cambridge University Press, 2019).

Setting

Let $E$ be a finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and induced error norm $\|\cdot\|$. Given a loss $\mathcal L:E\to\mathbb R$, a regularizer $\mathcal R:E\to\mathbb R$ and a constant $\lambda_n>0$, program (1) is

$$\hat\theta_{\lambda_n}\in\arg\min_{\theta\in E}\{\mathcal L(\theta)+\lambda_n\mathcal R(\theta)\}.$$

For a subspace $S$ write $u_S$ for the orthogonal projection of $u$ onto $S$, and $S^\perp$ for the orthogonal complement.

• Decomposability. For subspaces $\mathcal M\subseteq\overline{\mathcal M}$, the norm $\mathcal R$ is decomposable with respect to $(\mathcal M,\overline{\mathcal M}^\perp)$ if $\mathcal R(\theta+\gamma)=\mathcal R(\theta)+\mathcal R(\gamma)$ for all $\theta\in\mathcal M$ and $\gamma\in\overline{\mathcal M}^\perp$. Example: the $\ell_1$-norm with $\mathcal M=\overline{\mathcal M}=\{\theta:\theta_j=0\ \forall j\notin S\}$.
• Dual norm. $\mathcal R^*(v)=\sup_{\mathcal R(u)\le1}\langle u,v\rangle$.
• Subspace compatibility constant. $\Psi(\overline{\mathcal M})=\sup_{u\in\overline{\mathcal M}\setminus\{0\}}\mathcal R(u)/\|u\|$; for the $\ell_1$-norm on an $s$-dimensional coordinate subspace, $\Psi=\sqrt s$.
• The set $\mathbb C$. For a point $\theta^*\in E$,

$$\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)=\{\Delta\mid\mathcal R(\Delta_{\overline{\mathcal M}^\perp})\le3\mathcal R(\Delta_{\overline{\mathcal M}})+4\mathcal R(\theta^*_{\mathcal M^\perp})\}.$$

• Restricted strong convexity (RSC). With the Taylor error $\delta\mathcal L(\Delta,\theta^*)=\mathcal L(\theta^*+\Delta)-\mathcal L(\theta^*)-\langle\nabla\mathcal L(\theta^*),\Delta\rangle$, the loss satisfies RSC with curvature $\kappa_{\mathcal L}>0$ and tolerance $\tau_{\mathcal L}(\theta^*)$ if $\delta\mathcal L(\Delta,\theta^*)\ge\kappa_{\mathcal L}\|\Delta\|^2-\tau^2_{\mathcal L}(\theta^*)$ for every $\Delta\in\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$.

The conditions of the paper's main theorem are (G1): $\mathcal R$ is a norm, decomposable with respect to $(\mathcal M,\overline{\mathcal M}^\perp)$ with $\mathcal M\subseteq\overline{\mathcal M}$; and (G2): $\mathcal L$ is convex, differentiable and satisfies RSC. The Lean development lives in the namespace UnifiedMEstimator.General, with these objects named IsNormFn, IsDecomposable, dualNorm, compat, setC, taylorErr, RSC and IsOptimal.

Formalization targets

Goal: Theorem 1 (p. 10), tolerance term corrected

Under (G1) and (G2), if $\lambda_n>0$ and $\lambda_n\ge2\mathcal R^*(\nabla\mathcal L(\theta^*))$, then every optimal solution of program (1) satisfies

$$\|\hat\theta_{\lambda_n}-\theta^*\|^2\le9\,\frac{\lambda_n^2}{\kappa_{\mathcal L}^2}\,\Psi^2(\overline{\mathcal M})+\frac{2\tau_{\mathcal L}^2(\theta^*)+4\lambda_n\mathcal R(\theta^*_{\mathcal M^\perp})}{\kappa_{\mathcal L}}.$$

The bound holds for every pair $(\mathcal M,\overline{\mathcal M})$ over which $\mathcal R$ decomposes, and for every optimum, not only a distinguished one.

Milestones

1. Lemma 1 (p. 7): under the dual-norm condition on $\lambda_n$, the error $\hat\Delta=\hat\theta_{\lambda_n}-\theta^*$ lies in $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$. This milestone links an existing platform statement of the same lemma (Wainwright, Proposition 9.13).
2. Section 2.4, p. 10, first display: if $\theta^*\in\mathcal M$ and $\Delta\in\mathbb C$, then $\mathcal R(\Delta)\le4\Psi(\overline{\mathcal M})\|\Delta\|$.

Further statements

• Corollary 1 (p. 11): if $\theta^*\in\mathcal M$ and $\tau_{\mathcal L}(\theta^*)=0$, then $\|\hat\theta_{\lambda_n}-\theta^*\|\le3\lambda_n\Psi(\overline{\mathcal M})/\kappa_{\mathcal L}$ and $\mathcal R(\hat\theta_{\lambda_n}-\theta^*)\le12\lambda_n\Psi^2(\overline{\mathcal M})/\kappa_{\mathcal L}$.
• Section 2.4, p. 10, second display: a lower bound $\delta\mathcal L\ge\kappa_1\|\Delta\|^2-\kappa_2 g\,\mathcal R^2(\Delta)$ on the unit ball gives curvature $\kappa_1-16\kappa_2\Psi^2(\overline{\mathcal M})g$ on $\mathbb C$ when $\theta^*\in\mathcal M$.
• Example 1 (p. 5) and the value $\Psi(\mathcal M(S))=\sqrt{|S|}$ (p. 9): the $\ell_1$-norm instance, which shows that the hypotheses of the goal can be met.

Significance

Theorem 1 reduces a consistency proof for a new regularized estimator to two checks: that the regularizer decomposes over a pair of subspaces adapted to the model, and that the loss is curved on the set $\mathbb C$, together with a bound on $\mathcal R^*(\nabla\mathcal L(\theta^*))$ that is usually a concentration inequality. The paper derives from it the $s\log p/n$ Lasso rate under restricted eigenvalue conditions, rates for weakly sparse ($\ell_q$-ball) vectors, and group-Lasso rates; companion papers use it for low-rank matrix estimation, matrix completion and generalized linear models. Because the bound holds for every pair $(\mathcal M,\overline{\mathcal M})$, it gives an explicit trade-off between an estimation error and an approximation error $\mathcal R(\theta^*_{\mathcal M^\perp})$.

The theorem is proved in the paper's supplementary appendix. No machine-checked proof of it is known. On Prove2Me, Wainwright's textbook restatement (Theorem 9.19, HighDimStat.Decomposability.thm9_19_general_bound) is a related but different statement: its RSC condition is local, on a ball, with a tolerance proportional to $\mathcal R^2(\Delta)$, and it has extra side conditions and a different bound. A formal proof of the present goal certifies the deterministic core that every corollary of the paper relies on.

Difficulty

The obvious argument compares the objective at $\hat\theta$ and at $\theta^*$ and applies RSC to the error. RSC, however, is available only on the set $\mathbb C$, not on all of $E$: in high dimensions the loss is flat in many directions, so strong convexity fails. The work is to show first that the error lies in $\mathbb C$ (Lemma 1, which rests on decomposability and the choice of $\lambda_n$), and then to relate the regularizer to the error norm through the projections onto $\overline{\mathcal M}$ and $\overline{\mathcal M}^\perp$. The distinction between $\mathcal M$ and $\overline{\mathcal M}$ matters throughout: the compatibility constant is taken on the larger space $\overline{\mathcal M}$, while the approximation error projects $\theta^*$ onto the complement of the smaller one. The bound comes from a quadratic inequality in $\|\hat\Delta\|$, and the constants depend on how its terms are split.

Formalization scope

Representation. The parameter space is an arbitrary finite-dimensional real inner product space E (equivalently $\mathbb R^p$ with any inner product, as the paper allows); matrices are covered by the same abstraction. Subspaces are Submodule ℝ E, projections are Submodule.starProjection, and the gradient is Mathlib's gradient, under the hypothesis that $\mathcal L$ is differentiable. The dual norm and $\Psi$ are real suprema (sSup). They equal the paper's quantities because $\mathcal R$ is required to be a genuine norm (nonnegative, definite, absolutely homogeneous, subadditive) and $E$ is finite-dimensional; $\Psi(\{0\})=0$. The tolerance is a real number $\tau$ entering as $\tau^2$; RSC contains $\kappa>0$ and is quantified over exactly $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ for the same pair and point as the decomposability. Every statement is for every optimal solution of program (1). The data $Z_1^n$ are fixed and absorbed into $\mathcal L$, and $\theta^*$ is an arbitrary point: the paper's requirement that $\theta^*$ minimise the population risk is never used by the theorem and is dropped.

Corrections of the printed statements.

1. Display (22) prints the tolerance term as $\frac{\lambda_n}{\kappa_{\mathcal L}}\cdot2\tau^2_{\mathcal L}(\theta^*)$. As printed the statement is false: for $E=\mathbb R$, $\mathcal R=|\cdot|$, $\mathcal M=\overline{\mathcal M}=\mathbb R$, $\mathcal L(\theta)=(\max(0,|\theta|-1))^2$, $\theta^*=0.9$, $\lambda_n=0.01$, $\kappa_{\mathcal L}=1/2$, $\tau^2_{\mathcal L}=10$, the optimum is $0$ and $\|\hat\Delta\|^2=0.81$ exceeds the printed bound $0.4036$. The goal states $2\tau^2_{\mathcal L}(\theta^*)/\kappa_{\mathcal L}$; the two forms agree when $\tau_{\mathcal L}=0$, and the constants $9$ and $4$ are the paper's.
2. Corollary 1's (25a) prints $\|\hat\theta-\theta^*\|\le9\lambda_n^2\Psi^2(\overline{\mathcal M})/\kappa_{\mathcal L}$, which fails for $\mathcal L(\theta)=(\theta-0.002)^2$, $\theta^*=0.001$, $\lambda_n=0.004$ on $\mathbb R$; the mission states $3\lambda_n\Psi(\overline{\mathcal M})/\kappa_{\mathcal L}$. Its "$\mathbb C(\mathcal M,\overline{\mathcal M},\theta^*)$" is read as $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$.

Trivializations ruled out. A regularizer predicate weaker than a norm would let the real suprema collapse to the junk value $0$ and make the $\lambda_n$ condition or the $\Psi$ term free; RSC over all of $E$ would be classical strong convexity, and RSC over the cone without the $4\mathcal R(\theta^*_{\mathcal M^\perp})$ slack would make the goal false; decomposability without $\mathcal M\subseteq\overline{\mathcal M}$ or with the bars misplaced changes the theorem. None of these is used. The $\ell_1$ example and a checked one-dimensional instance show that all hypotheses of the goal can hold simultaneously.

Infrastructure and contributions. A complete development needs: Hölder's inequality for a norm and its dual norm, boundedness of the two suprema in finite dimension, the decomposability inequality $\mathcal R(\theta^*+\Delta)-\mathcal R(\theta^*)\ge\mathcal R(\Delta_{\overline{\mathcal M}^\perp})-\mathcal R(\Delta_{\overline{\mathcal M}})-2\mathcal R(\theta^*_{\mathcal M^\perp})$, the first-order characterization of convexity, and the solution of a scalar quadratic inequality. The dual-norm and compatibility-constant lemmas are reusable for every decomposable-regularizer mission. Proofs of the milestones, of the goal, and of the $\ell_1$ instance are all welcome.

Selected references

• S. N. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A Unified Framework for High-Dimensional Analysis of M-Estimators with Decomposable Regularizers, Statistical Science 27(4), 2012, 538–557. arXiv:1010.2731v3, doi:10.1214/12-STS400
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous Analysis of Lasso and Dantzig Selector, Annals of Statistics 37(4), 2009, 1705–1732. arXiv:0801.1095
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 9. doi:10.1017/9781108627771

Motivation

Many real-world disjunctive models are not unions of polyhedra in a single shared space, but unions of polyhedra in different spaces linked by a logical implication: some action affecting one set of entities has consequences for another. Balas's treatment of such models (§17 of the book, following [17]) reduces to understanding a single auxiliary object attached to each polytope in isolation: its dominant, the set of points that dominate (coordinatewise) some feasible point. Dominants and their duals, blockers, have a long history in combinatorial optimization — blocking-pair theory for covering and packing polyhedra traces to Fulkerson (D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194, https://doi.org/10.1007/BF01584085) — but this chapter develops a self-contained, constructive theory tailored to polytopes inside the unit cube, culminating in an exact, facet-complete description of the dominant for an arbitrary such polytope.

Setting

For a polyhedron $P \subseteq \mathbb{R}^n_+$, the dominant is $P^+ := P + \mathbb{R}^n_+ = \{y \ge 0 : y \ge x \text{ for some } x \in P\}$, and the blocker is $P^* := \{\pi \in \mathbb{R}^n_+ : \pi x \ge 1 \text{ for all } x \in P\}$ — the covering inequalities valid for $P$. (The blocker is not the reverse polar of 02b-polarity: restricting to the nonnegative orthant is essential and changes the object.) For $x^* \in \mathbb{R}^n_+$, the upper-separation value is $\alpha_P(x^*) := \min\{\pi x^* : \pi \in P^*\}$; a violated covering inequality for $x^*$ exists exactly when $\alpha_P(x^*) < 1$. A polytope $P \subseteq [0,1]^n$ is upper monotone (with respect to $[0,1]^n$) if $P = P^+ \cap [0,1]^n$ — the natural "closure" condition under which the theory of this chapter applies cleanly.

For $S \subseteq N := \{1,\dots,n\}$, write $a(S) := \sum_{j\in S} a_j$. Given $P \subseteq \mathbb{R}^n$ and a coordinate subset $S$, the projection $P^S$ keeps only the $S$-coordinates, letting the rest range freely. $I^S$ is the set of valid inequalities $\pi x \ge 1$ of $P^S$ with $\pi_j > 0$ exactly on $S$, tight at $|S|$ linearly independent points of $P^S$.

Formalization targets

Proposition 13.1. For an upper monotone $P = \bigcap_i P_i$ (each $P_i$ a single inequality in $[0,1]^n$), $P^+ = \bigcap_i P_i^+$.

Theorem 13.3. For $P = \{x \in [0,1]^n : ax \ge 1\}$ ($a \ge 0$) upper monotone,

$$P^+ = \Big\{x \ge 0 : \sum_{j\in S} \frac{a_j x_j}{1-a(N\setminus S)} \ge 1 \text{ for every } S\subseteq N \text{ with } 1-a(N\setminus S)>0\Big\}.$$

Theorem 13.5. For the same $P$ and any $x^* \ge 0$, with $x^*_q$ the greatest coordinate value $x^*_j$ satisfying $a(N\setminus S(x^*_j))<1$ and $x^*_j \le g(x^*_j)$: $S(\alpha_P) = S(x^*_q)$ and $\alpha_P = g(x^*_q)$, an explicit, computable value.

Theorem 13.7 (goal). For an arbitrary polytope $P \subseteq [0,1]^n$ (not necessarily upper monotone):

$$P^+ = \{x \ge 0 : \pi x \ge 1 \text{ for every } S \subseteq N \text{ and } \pi \in I^S\},$$

and every one of these inequalities is facet-defining for $P^+$.

Corollary 13.8. Every facet-defining inequality of $P^+$ has at most $\dim(P)+1$ nonzero coefficients.

The targets move from the intersection-distributivity fact (13.1) through an explicit, exponentially-large but fully closed-form facet system for the single-inequality case (13.3) and its constructive, polynomial evaluation recipe (13.5) to the fully general facet characterization (13.7, requiring no monotonicity assumption at all) and its immediate corollary on facet sparsity (13.8).

Significance

Theorem 13.7 is a rare case in polyhedral combinatorics of a complete and exact facet description obtained for the dominant of an arbitrary polytope, not merely a valid relaxation or an algorithmic separation oracle — every facet is accounted for, and every listed inequality is genuinely a facet, not merely valid. Corollary 13.8's support bound is the mechanism that makes Theorem 13.10 (not part of this mission) tractable: it lets the facets of a dominant built from a disjunction of polytopes in different spaces be characterized purely in terms of each factor's own low-dimensional facets, avoiding an exponential blowup in the combined space.

Both directions are proved in the source (Balas's own treatment, following the joint framework of [17]) but have no counterpart on this platform: nothing existing treats dominants, blockers, or upper monotonicity. This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.7 is to state only the validity half of the claim (every inequality from $I^S$ is valid for $P^+$) and treat "facet-defining" as a decoration — after all, Proposition 13.1's polar-style validity argument generalizes easily. But the theorem's actual force is the converse: not merely that these inequalities suffice to describe $P^+$, but that none of them is redundant, and no other facet exists. The book's own converse proof needs a genuine perturbation argument (splitting a facet candidate with fewer than $|S|$ independent tight points into two distinct valid inequalities averaging back to it, contradicting facetness) — this is where the real content lives, and a formalization that only captures the forward direction would understate the theorem substantially.

For Theorem 13.5, the difficulty is that $S(\alpha)$ and $g(\alpha)$ are themselves defined in terms of $\alpha$, so "the largest $x^*_j$ satisfying [a condition stated in terms of $S(x^*_j)$ and $g(x^*_j)$]" is a genuinely self-referential extremal characterization, not a closed-form formula one could simply plug into — hence its faithful statement (via IsGreatest over an explicit, self-referential candidate set) rather than an unwound algebraic expression.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default. Dominant/Blocker are given their own names (not reusing, even informally, 02b-polarity's polar/reverse-polar vocabulary), per BRIEF.md's explicit warning that the nonnegativity restriction makes these different objects. PolyDim/IsFacet are restated from 02b-polarity/11a-intersection-cuts (affine dimension via Module.finrank of vectorSpan, faces via IsExtreme), since Chapter 2 already pins these down precisely for this series and Chapter 13's own facet claims use the same notion. IsUpperMonotone is stated exactly as Definition 4 (P = P⁺ ∩ [0,1]ⁿ), not paraphrased as coordinatewise monotonicity, per BRIEF.md's explicit warning that these are different conditions.

IsInIS (membership in $I^S$) uses LinearIndependent ℝ directly for the "|S| linearly independent points" hypothesis, matching the book's own wording; since every such point satisfies $\pi x=1$, a linear dependence among them is automatically an affine dependence (the coefficients of any nontrivial linear relation among them must sum to zero), so this is not a weakening of the more familiar "affinely independent" reading a reader might otherwise expect. A trivializing formalization to rule out explicitly: describing Theorem 13.7's $P^+$ using only the validity half of the claim (dropping "each of these inequalities is facet-defining for $P^+$") — this mission states both conjuncts, since the facet-exactness is the theorem's genuine content beyond a Farkas-style validity certificate.

This mission depends on no other chunk's Lean definitions; it restates the affine-dimension/facet vocabulary of 02b-polarity/11a-intersection-cuts only informally, per the series convention. Corollary 13.6 (an $O(n)$-time algorithmic claim for computing $\alpha_P$) is out-of-cone per BRIEF.md: it is fully quantified, not a veto-V3 case, but is a computational-complexity statement outside this mission's polyhedral-characterization scope.

Selected references

• D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194. https://doi.org/10.1007/BF01584085
• E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs (for the broader monotonization-of-polyhedra context cited by this chapter's introduction), European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.1–13.2. https://doi.org/10.1007/978-3-030-00148-3

Motivation

The lift-and-project cut-generating LP (CGLP) is the workhorse of the book's cutting-plane machinery, but its number of variables grows with $q$, the number of terms in the disjunction — a real computational cost for disjunctions with many terms. An alternative representation of the same disjunctive hull, built from vertices and extreme rays rather than from a dual LP, trades this away: its number of variables is fixed at $n$ regardless of $q$, at the price of a constraint set that is generally exponential in size (T. H. Kim, V-polyhedral disjunctive cuts, PhD thesis and papers with E. Balas; the underlying representation traces to the classical Minkowski–Weyl theorem for polyhedra). This mission formalizes the chapter's capstone: the V-polyhedral, lift-and-project, and generalized-intersection-cut families — three representations that look structurally different — coincide exactly.

Setting

A disjunctive set in V-polyhedral (vertex-ray) form is $F := \bigcup_{h\in Q} P^h$, $P^h := \mathrm{conv}\,V^h + \mathrm{cone}\,R^h$, where $V^h$/$R^h$ are the (finite) sets of vertices and extreme rays of the $h$-th disjunct. The conic hull of a set $S$ is the set of all finite nonnegative combinations of its elements. For a reference point $x_F \in F$, the disjunctive cone $C_{x_F}$ is the homogenization, at $x_F$, of the translated disjunctive system: $(x',x_0') \in \mathbb{R}^n \times \mathbb{R}_+$ with $Ax' + (Ax_F-b)x_0' \ge 0$ and $\bigvee_h(D^hx' + (D^hx_F-d^h_0)x_0' \ge 0)$.

For a relaxation $\tilde P^h$ of each disjunct with $P^h \subseteq \tilde P^h \subseteq C(x^h)$ (the LP cone at the disjunct's own optimum $x^h$), write $\tilde V^h$, $\tilde R^h$ for its vertices and rays, and $C := \mathrm{conv}(\bigcup_h \tilde V^h) + \mathrm{cone}(\bigcup_h \tilde R^h)$ for the single combined polyhedron they generate. The associated L&P cut-generating LP is

$$\alpha = u^h \tilde D^h, \qquad \beta \le u^h \tilde d^h_0 \quad (h\in Q), \qquad \textstyle\sum_{h\in Q} u^h e = 1, \qquad u^h \ge 0.$$

Formalization targets

Proposition 12.1. $\alpha x \ge \beta$ is valid for $F$ if and only if $\alpha p \ge \beta$ for every $p \in V^h$ and $\alpha r \ge 0$ for every $r \in R^h$, over every $h \in Q$.

Proposition 12.3. For a cut $\alpha x \ge \beta$ tight at $x_F$ ($\alpha x_F = \beta$) and $x \in F$: $\alpha x < \beta$ if and only if $\alpha(x - x_F) < 0$ for the corresponding point $(x - x_F, 1)$ of $C_{x_F}$.

Theorem 12.4. If $(\alpha,\beta)$ satisfies $\alpha p \ge \beta$ for every $p \in \tilde V^h$ and $\alpha r \ge 0$ for every $r \in \tilde R^h$ (over every $h$), and the mixed-integer feasible set $P_I$ lies in the combined polyhedron $C$, then $\alpha x \ge \beta$ is valid for $P_I$.

Theorem 12.5 (goal). $(\alpha,\beta)$ is valid for the combined vertex-ray system if and only if there exists a multiplier $u = \{u^h\}_{h\in Q}$ making it simultaneously a feasible solution of the CGLP above and a generalized intersection cut from

$$S := \{x \in \mathbb{R}^n : u^h \tilde D^h x \le u^h \tilde d^h_0,\ h \in Q\}.$$

The targets move from the elementary generator-validity fact (12.1) and its algorithmic companion (12.3, which the iterative cut-generation procedure of §12.1 uses to search only adjacent extreme points) through the same validity criterion generalized to a relaxed system (12.4) to the three-way unification (12.5) that is the entire point of introducing the V-polyhedral representation in the first place.

Significance

Theorem 12.5 explains why the V-polyhedral approach is worth having at all: it produces exactly the same cuts as the lift-and-project CGLP, so nothing is lost by switching representations, while the computational cost profile is reversed (the book's own estimate, not part of this mission's targets, shows the V-polyhedral approach at least $q^3$ times cheaper for a $q$-term disjunction using $\tilde P^h = C(x^h)$). This matters directly for disjunctions with many terms — split disjunctions used one or two at a time throughout most of the earlier chapters — which the CGLP approach makes increasingly expensive as $q$ grows, but which the V-polyhedral approach handles without a growing variable count.

Both directions are proved in the source (this book's own §12, citing the underlying V-polyhedral cut idea to Balas's joint work with T. H. Kim, and the GIC-to-L&P equivalence to §11.4's own Theorem 11.5) but have no formalized counterpart on this platform: nothing existing treats V-polyhedral representations, disjunctive cones, or a three-way cut-family equivalence. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 12.5 is to state only "the V-polyhedral cuts and the L&P cuts coincide" and treat the GIC leg as a footnote, since the book's own two-line proof dispatches the GIC equivalence by citing an earlier theorem rather than re-deriving it. But the theorem's actual claim is a three-way equivalence with a specific, described $S$ built from the very multipliers that solve the CGLP — dropping the GIC leg, or defining $S$ independently of those multipliers, would understate what is being asserted (the book's own remark following the theorem stresses that the GIC-defining points and the V-polyhedral vertices are typically different points that nonetheless yield equivalent cuts, which is exactly the content a two-way statement would erase).

For Theorem 12.4, the subtlety is that $C$ (the combined polyhedron) is not the union $\bigcup_h \tilde P^h$ but its convex hull — a strictly larger set in general — so validity for $C$'s generators is a priori a stronger requirement than validity for each $\tilde P^h$ separately; the theorem's force is that this stronger validity is still exactly what is needed (and obtained) to conclude validity for $P_I$.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index Q left as a general type for Propositions 12.1/12.3 (so the same Ph/DisjSet definitions serve any finite disjunction) and specialized to [Fintype Q] where a finite sum over disjuncts is needed (Theorem 12.4's combined polyhedron, the CGLP of Theorem 12.5). V^h/R^h (Proposition 12.1) and Ṽ^h/R̃^h (Theorem 12.4) are formalized with the same underlying definitions (Ph, IsVPolyhedralValid) applied to different vertex/ray data, per BRIEF.md's explicit warning that these are distinct objects — not by duplicating the definitions under two names. "Is a generalized intersection cut from $S$" (IsGICFromS) is formalized via the exact characterization Theorem 11.4's own remark in 11a-intersection-cuts gives for the GIC family (valid outside $S$'s interior, and a genuine cut), rather than by re-deriving the underlying extreme-ray construction — a trivializing formalization this mission rules out would instead drop this leg's dependence on the same multiplier u that witnesses the CGLP leg, decoupling S from the solution it is supposed to come from.

This mission depends on no other chunk's Lean definitions; it restates 02a-convex-hull's vertex/extreme-point vocabulary, 11a-intersection-cuts's cut apparatus, and 11b-monoidal-strengthening's disjunctive-cut conventions only informally, per the series convention. Theorem 12.2 (the extreme-ray/edge correspondence underlying the "adjacent vertices only" search strategy) was not drafted this pass — see HARD.md — since a faithful, non-circular formalization of "edge of a polytope incident with a point" needs face-lattice machinery beyond what any earlier chunk in this series has built. The ConicHull/DisjunctiveCone/CombinedC definitions are reusable by any later mission touching V-polyhedral cut generation.

Selected references

• E. Balas and T. H. Kim, Cutting planes from extended LP formulations, Mathematical Programming 156 (2016), 587–606. https://doi.org/10.1007/s10107-015-0885-2
• E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
• A. Kazachkov, Non-Recursive Cut Generation, PhD dissertation, Carnegie Mellon University, 2018 (cited by Balas for the relaxation-based V-polyhedral cut generator of §12.2).
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 12. https://doi.org/10.1007/978-3-030-00148-3