Linear Optimization

Motivation

Many decision problems in operations research are solved in two stages: a model predicts the unknown cost vector of a linear optimization problem from features, and the predicted costs are then passed to a solver. The smart predict-then-optimize (SPO) loss of Elmachtoub and Grigas measures the quality of a prediction by the excess true cost of the decision it induces, rather than by the prediction error itself. El Balghiti, Elmachtoub, Grigas and Tewari study how well the empirical SPO loss generalizes. Their margin-based bounds (Theorems 4 and 5 of the paper) require a geometric condition on the feasible region, the strength property, and a way to compute the distance to degeneracy that enters the margin loss.

Section 5 of the paper verifies this condition in the two cases that matter in practice. For strongly convex regions it is Theorem 7 (mission III of this series). This mission covers the other case, §5.2: feasible regions that are polytopes given by a list of points, which includes the unit simplex of multiclass classification and the feasible regions of shortest-path, assignment and other combinatorial problems written as convex hulls.

Setting

Let $E$ be a finite-dimensional real vector space (the paper's $\mathbb R^d$) with a norm $\|\cdot\|$. A cost vector $\hat c$ is a linear functional on $E$; its value at $w$ is written $\hat c^\top w$, and its dual norm is $\|\hat c\|_*=\max_{\|w\|\le1}\hat c^\top w$.

The feasible region is a polytope with a known convex hull representation: pairwise distinct points $v_1,\dots,v_K\in E$ and

$$S=\mathrm{conv}\{v_1,\dots,v_K\}.$$

Redundant points (points that are convex combinations of the others) are allowed. For a cost vector $\hat c$, $P(\hat c)$ is the problem $\min_{w\in S}\hat c^\top w$, and an optimization oracle $w^*$ is any map with $w^*(\hat c)\in\arg\min_{w\in S}\hat c^\top w$ for every $\hat c$.

• The degenerate set $\mathcal C^\circ$ is the set of cost vectors $\hat c$ for which $P(\hat c)$ has more than one optimal solution.
• The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$.
• $S$ has the strength property with parameter $\mu>0$ if

$$\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all } w\in S\text{ and all }\hat c.$$

• The negative normal cone at $v_j$ is $\mathcal K_j=-N_S(v_j)=\{\hat c:\hat c^\top(w-v_j)\ge0\ \text{for all } w\in S\}$, the cost vectors for which $v_j$ is optimal.
• The diameter is $\Delta(S)=\sup_{w_1,w_2\in S}\|w_1-w_2\|$.

Formalization targets

Goal: Theorem 8, strength claim (p. 25)

If $S=\mathrm{conv}\{v_1,\dots,v_K\}$ is not a singleton, then for every oracle $w^*$, $S$ has the strength property with parameter

$$\mu=\frac{2}{\Delta(S)}>0 .$$

Milestones, in attack order

1. Eq. (9) (p. 24): each cone is described by finitely many inequalities,

$$\mathcal K_j=\{\hat c:\hat c^\top(v_i-v_j)\ge0\ \text{for all } i=1,\dots,K\}.$$

2. Proposition 2 (p. 25): $P(\hat c)$ has a unique optimal solution if and only if $\hat c\in\mathrm{int}(\mathcal K_j)$ for some $j$; hence

$$\mathcal C^\circ=\mathbb R^d\setminus\bigcup_{j=1}^K\mathrm{int}(\mathcal K_j).$$

3. Diameter (p. 25, the sentence before Theorem 8): $\Delta(S)=\max_{i,j}\|v_i-v_j\|$.
4. Theorem 8, eq. (10) (p. 25): for every oracle and every $\hat c$,

$$\nu_S(\hat c)=\min_{j:\,v_j\ne w^*(\hat c)}\frac{\hat c^\top(v_j-w^*(\hat c))}{\|v_j-w^*(\hat c)\|}.$$

Significance

The result. Formula (10) turns the distance to degeneracy, defined as an infimum over an infinite non-convex set, into a minimum of $K$ explicit ratios that needs one oracle call. This makes the margin SPO loss of the paper computable for polytopes. The strength claim, combined with the paper's Theorems 4 and 5, yields margin-based generalization bounds for the SPO loss over any polytope with a known vertex list, with a dependence on the hypothesis class through its multivariate Rademacher complexity rather than through a Natarajan dimension. For the unit simplex it recovers known margin bounds for multiclass classification (Example 8).

Formalizing it. The results are proved in the paper; to our knowledge none of them is machine-checked. A formalization produces, beyond the four statements, a Lean account of the normal fan of a polytope presented by a point list, its interplay with uniqueness of linear-optimization solutions, and distances to its boundary measured in a dual norm. These are standard facts of polyhedral theory that Mathlib does not yet state in this form.

Difficulty

The obstacle is that $\nu_S$ is a distance to the degenerate set, and that set is neither convex nor given by inequalities: it is a union of lower-dimensional pieces of the normal fan, so no projection formula applies, and its description depends on which points of the representation are redundant. Relating a dual-norm ball around $\hat c$ to the finitely many inequalities of eq. (9) is where the argument needs care. A Euclidean shortcut is not available: the norm is arbitrary, and the numerator of (10) and the distance $\nu_S$ are measured in different norms. A second trap is the oracle: at a degenerate $\hat c$ it may return a point that is not among the $v_j$, and (10) must still hold.

Formalization scope

• $E$ is a finite-dimensional real normed space; cost vectors are elements of StrongDual ℝ E, whose operator norm is the dual norm. Interiors and distances in the cost space use that norm.
• The polytope is v : Fin K → E, injective, with $S$ = convexHull ℝ (Set.range v). Nonemptiness, compactness and convexity of $S$ (the paper's §2 standing assumptions) follow from this representation; Proposition 2 and the diameter identity add $K\ge1$, which is that nonemptiness.
• "Not a singleton" is S.Nontrivial. Without it $\mathcal C^\circ=\emptyset$, $\nu_S\equiv0$ and the strength property holds for free; with it, $0\in\mathcal C^\circ$ and $\nu_S$ is a genuine distance. The goal's parameter $2/\Delta(S)$ is stated to be positive, so the Lean conventions $\mathrm{diam}=0$ on unbounded or one-point sets and $2/0=0$ cannot trivialize it.
• The oracle is arbitrary: every theorem quantifies over all maps $w$ with $w(\hat c)\in\arg\min_S\hat c$, never a fixed selection.
• $\nu_S$ is Metric.infDist to $\mathcal C^\circ$; $\Delta(S)$ is Metric.diam, correct here because $S$ is bounded. Minima and maxima over finite index sets are stated with IsLeast/IsGreatest, so no junk value of min' or sInf enters.
• Reusable infrastructure: the negative normal cones and normal fan of a point-list polytope, the characterization of unique optima of linear optimization over a polytope, and the dual-norm distance to the boundary of a polyhedral cone. Contributions of any of these as standalone lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022 (Mathematics of Operations Research, 2023). https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2009. https://doi.org/10.1007/978-3-642-02431-3

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$, dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$. Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$, a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$, and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

• $\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

$$R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.$$

• A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$, read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$. It is valid if every $s\in R_f(W)$ satisfies it.
• $V$ is the affine hull of $(f+W)\cap\mathbb Z^q$, and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$. A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$.
• $\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
• Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$. Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$, for some $\rho>0$, $\lambda\in\mathbb R^\ell$.
• A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$, inclusionwise maximal with these properties.
• For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$: the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$, $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$, and $\rho_K(r)=\sup_{y\in\hat K}ry$. For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$.

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$.

Formalization targets

Goal: Theorem 3 (p. 6)

1. Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$.
2. Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

$$\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1$$

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$.

Milestones

In the order in which the proof on pp. 15–21 uses them:

• Lemma 23 (a sublinear valid inequality below any valid one)
• Lemma 26 (invariance under equivalence)
• Claims 1 and 2 in the proof of Theorem 3
• Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$-sublevel set $K$)
• Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$)
• Remark 29 ($\rho_K=\max_ia_ir$ for tight rows)
• Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
• Claim 7 ($\psi_B$ below a nonnegative sublinear $\psi''$)
• Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$. It also says that for irrational $W$, where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$. For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$, adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$, so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$. This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

• Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
• Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$.
• Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$, to $W$ for $K$.
• $\psi_B$. It is defined as $\rho_{B-f}$, independent of any description of $B$.

The paper is imprecise in three places, and the formalization departs from the page in each:

1. Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$, $a_2=1/2$, $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$. It is stated with the tightness the paper arranges before using it.
2. The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$, for example for $\psi\equiv0$. Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
3. Claims 5 and 7 invoke Corollary 20 in $f+W$, although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
• A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
• V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
• K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let labels take the values $y\in\{-1,+1\}$. The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$. A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$.

Metric (Definition 2). For a weight $\kappa>0$,

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .$$

Changing a label costs $\kappa$; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$, $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$. The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$.

Data. Training samples $(\hat x_i,\hat y_i)$, $i=1,\dots,N$, define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$.

Worst- and best-case risks.

$$\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].$$

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$, a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$, $s,r,t\in\mathbb R^N$, program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$,

$$1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .$$

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$, $\varepsilon\ge0$, $N\ge1$, all samples and every weight vector $\hat\beta$, both programs attain their minima $v$ and $w$, and

$$\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .$$

The identities hold for each fixed $\hat\beta$, so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then for any sample-dependent $\hat\beta$

$$\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,$$ $$\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .$$

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$. Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$. The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$.

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$, $\text{false}\mapsto-1$; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$, and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$.

The following choices differ from a literal reading of the page:

• The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$. This fails on the hyperplane $\langle\beta,x\rangle=0$, where $f_\beta(x)=-1$ is correct for $y=-1$. The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
• The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, as a hypothesis, and "with probability $1-\eta$" is read as "with probability at least $1-\eta$". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$, restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

Motivation

Subgradient optimization maximizes a concave function that is not differentiable by stepping along an arbitrary subgradient with a prescribed sequence of step sizes. It became a standard tool of integer programming after Held and Karp used it to compute the Lagrangian 1-tree bound for the traveling-salesman problem (Held & Karp 1971). Held, Wolfe and Crowder then tested it on the assignment problem, a traveling-salesman relaxation and a multicommodity flow problem (Held, Wolfe & Crowder 1974).

The method has one practical defect that the paper names at the start of its Section 6: it contains no test of optimality. The value $w(\pi^j)$ approaches the maximum, but at no finite step does the method say that the maximum has been reached, or what the maximum is. Section 6 of the paper supplies such a test for the case where $w$ is a minimum of finitely many affine functions. The finitely many subgradients produced by the iterates define a small linear program, the core problem, and from some iteration on this linear program already solves the full dual linear program. Its optimal value is therefore the exact maximum of $w$, obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.

Timeline:

• 1967–1969: Poljak proves that the subgradient iterates satisfy $w(\pi^j)\to\max w$ when the step sizes tend to zero and have divergent sum (Poljak 1967; Poljak 1969).
• 1971: Held and Karp apply the method to the 1-tree bound (Held & Karp 1971).
• 1974: Held, Wolfe and Crowder prove that the core problem $P(J,J^*)$ solves the dual linear program (Theorem 6.3) and give a sufficient condition for bounded iterates (Theorem 6.1).
• 1996–1999: primal recovery from subgradient iterates is developed further, by convex combinations of the subgradients with weights derived from the step sizes (Sherali & Choi 1996; Larsson, Patriksson & Strömberg 1999).

Setting

Fix $n\ge0$ and write $E^n=\mathbb R^n$ with the Euclidean inner product $\pi\cdot v$. The data are $K\ge1$ scalars $c_k$ and vectors $v_k\in E^n$, and

$$w(\pi)=\min\{c_k+\pi\cdot v_k : k=1,\dots,K\}.\qquad(2.2)$$

The function $w$ is assumed bounded above, the paper's standing assumption. An index $k$ attains the minimum at $\pi$ if $c_k+\pi\cdot v_k=w(\pi)$.

A run of the subgradient algorithm consists of a starting point $\pi^0\in E^n$, step sizes $t_j>0$ and indices $k(j)$ such that $k(j)$ attains the minimum at $\pi^j$, and

$$\pi^{j+1}=\pi^j+t_j\,v_{k(j)}\qquad(j=0,1,\dots).\qquad(2.6)$$

No rule for choosing among several minimizing indices is imposed. Write $v^j=v_{k(j)}$ and $c^j=c_{k(j)}$. The step-size conditions are

$$t_j\to0,\qquad \sum_{j=0}^\infty t_j=\infty.\qquad(2.7)$$

The dual linear program of $\max w$ is

$$\min\Big\{\sum_k c_ky_k : y_k\ge0,\ \sum_ky_k=1,\ \sum_ky_kv_k=0\Big\}.\qquad(6.1)$$

For integers $J<J^*$ the core problem $P(J,J^*)$ has one variable $y_j$ for each iteration $j\in[J,J^*]$:

$$\min\Big\{\sum_{j=J}^{J^*}c^jy_j : y_j\ge0,\ \sum_{j=J}^{J^*}y_j=1,\ \sum_{j=J}^{J^*}y_jv^j=0\Big\}.$$

An index chosen at several iterations contributes several identical columns. A point $y$ of $P(J,J^*)$ is sent to the point $\bar y_k=\sum\{y_j : J\le j\le J^*,\ k(j)=k\}$ of (6.1). This aggregation preserves feasibility and objective value.

Formalization targets

Goal: Theorem 6.3 (p. 82)

Assume $w$ is bounded above, $(t_j,\pi^j,k(j))$ is a run satisfying (2.7), and $\{\pi^j\}$ is bounded. Then

$$\forall J\ \exists J^*>J:\quad P(J,J^*)\text{ has a solution, and every solution of }P(J,J^*)\text{ aggregates to a solution of (6.1)}.$$

The goal states existence of $J^*$, which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large $J^*$. That stronger form is not the goal. Feasibility of $P(J,J^*)$ (Lemma 6.2) or the inequality $\mathrm{Value}[P(J,J^*)]\ge\mathrm{Value}[(6.1)]$, which holds for every feasible $P(J,J^*)$, is not a formalization of the goal. The content is optimality in (6.1).

Milestones

1. Eq. (2.10): if $\pi^*$ maximizes $w$ and $k$ attains the minimum at $\pi$, then $w^*-w(\pi)\le v_k\cdot(\pi^*-\pi)$.
2. §6, p. 80 (display): under (2.6), (2.7) and $w$ bounded above, $\lim_j w(\pi^j)=\max w=w(\pi^*)$ for some $\pi^*$. The iterates are not assumed bounded.
3. Theorem 6.1: if every $\pi\ne0$ has some $\pi\cdot v_k<0$, every run satisfying (2.7) is bounded.
4. Eq. (6.1): (6.1) has a solution, and its optimal value equals $\max w$.
5. Lemma 6.2: for any $J$ there is $J^*>J$ with $P(J,J^*)$ feasible, for bounded runs.

Significance

Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving $P(J,J^*)$ for growing $J^*$ produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence $\max w$. In the Lagrangian applications, where (6.1) is the linear relaxation of a combinatorial problem, this yields both the bound and a primal solution of the relaxation. The theorem is the ancestor of the primal-recovery results listed in the timeline.

The mission produces a machine-checked version of the paper's Section 6, together with the input the paper takes on citation: Poljak's convergence theorem for divergent-series step sizes, specialized to piecewise-linear concave functions. Neither Poljak's theorem nor Theorem 6.3 is in Mathlib. The pieces are reusable: the convergence theorem applies to every Lagrangian dual solved by subgradient steps, and the duality between $\max w$ and (6.1) is linear-programming duality for a minimum of affine functions.

Difficulty

The inequality $\operatorname{Value}P(J,J^*)\ge\operatorname{Value}(6.1)$ is immediate, since aggregation maps feasible points to feasible points with the same objective. All of the content lies in the reverse inequality. That inequality ties a finite linear program to the limit of an infinite sequence, and it must hold for an arbitrary choice among tied minimizing indices. The iterates themselves need not converge, and under (2.7) the values $w(\pi^j)$ are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of $w$, fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of $P(J,J^*)$ also needs its own argument, and it fails without the boundedness hypothesis.

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and $w$ is the finite minimum Finset.univ.inf'. A run is the predicate IsSubgradientRun c v t π k: positive steps, a minimizing index at every step, and update (2.6). It is not a function of $\pi^0$, so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to $+\infty$. Iterates are indexed from $j=0$. Boundedness is Bornology.IsBounded (Set.range π). The variables of $P(J,J^*)$ are a function on $\mathbb N$ of which only the values at $J\le j\le J^*$ enter. Optimality of $y$ in either linear program means feasibility plus an objective no larger than that of every feasible point. Suprema are never taken over unbounded sets: every maximum of $w$ is stated as attained at an explicit $\pi^*$.

A statement that only asserts feasibility of $P(J,J^*)$, or only $\operatorname{Value}P\ge\operatorname{Value}(6.1)$, is not the theorem. The goal requires that the solutions of $P(J,J^*)$ be optimal for (6.1).

Theorem 6.1 is printed for the step rule (2.8), but its proof uses $w(\pi^j)\to w^*$, the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.

A complete development needs:

• linear-programming duality for (6.1), including attainment;
• the convergence theorem for divergent-series step sizes;
• existence of a maximizer of a bounded-above minimum of finitely many affine functions;
• basic facts on convex hulls of finitely many vectors in $E^n$.

The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.

Selected references

• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• B. T. Poljak, A general method of solving extremum problems, Soviet Mathematics Doklady 8 (1967) 593–597.
• B. T. Poljak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9 (1969) 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
• H. D. Sherali, G. Choi, Recovery of primal solutions when using subgradient optimization methods to solve Lagrangian duals of linear programs, Operations Research Letters 19 (1996) 105–113. https://doi.org/10.1016/0167-6377(96)00019-3
• T. Larsson, M. Patriksson, A.-B. Strömberg, Ergodic, primal convergence in dual subgradient schemes for convex programming, Mathematical Programming 86 (1999) 283–312. https://doi.org/10.1007/s101070050090