The OR Formalization Drive

Motivation

Least squares fits a linear model $Ax \simeq b$ by minimizing $\|Ax - b\|$, and its solution can be extremely sensitive to errors in the data $(A, b)$ when $A$ is ill-conditioned. The standard remedy is Tikhonov regularization (ridge regression): minimize $\|Ax - b\|^2 + \mu\|x\|^2$, whose solution $x = (A^\top A + \mu I)^{-1}A^\top b$ is stable but depends on a parameter $\mu > 0$ that must be chosen by some external rule.

El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed instead to take the uncertainty in $(A, b)$ seriously: the robust least-squares (RLS) solution minimizes the worst-case residual over all perturbations $[\Delta A\ \Delta b]$ of Frobenius norm at most $\rho$. Their Theorem 3.1 shows that for $\rho = 1$ this worst-case residual equals $\|Ax - b\| + \sqrt{\|x\|^2 + 1}$ and that its minimization is the second-order cone program (15). Theorem 3.2, the subject of this mission, reads off the optimal solution: it is a Tikhonov-regularized solution, and the regularization parameter is not a free choice but is fixed by the data. This gives a principled answer to the question of how to choose $\mu$, and it is the reason the paper describes RLS as "a Tikhonov regularization procedure" with "a rigorous way to compute the regularization parameter" (abstract, p. 1035).

A closely related model for least squares with bounded data uncertainty was developed at the same time by Chandrasekaran, Golub, Gu and Sayed; the paper notes that their preliminary draft (its reference [5]) gives a solution to the unstructured RLS problem similar to that of §3.2 (pp. 1036–1037).

Setting

Throughout, $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^n$, $x \in \mathbb R^m$, and every vector norm is Euclidean, $\|v\| = \sqrt{\sum_i v_i^2}$. For $x \in \mathbb R^m$, $[x; 1] \in \mathbb R^{m+1}$ is $x$ with a coordinate $1$ appended, so $\|[x;1]\| = \sqrt{\|x\|^2 + 1}$.

The SOCP (15) is the problem, in the variables $x \in \mathbb R^m$ and $\lambda, \tau \in \mathbb R$,

$$\text{minimize } \lambda \quad\text{subject to}\quad \|Ax - b\| \le \lambda - \tau,\qquad \|[x;1]\| \le \tau.$$

A triple $(x, \lambda, \tau)$ is optimal for (15) if it is feasible and $\lambda \le \lambda'$ for every feasible $(x', \lambda', \tau')$. Its dual, derived in the paper from the general second-order cone duality of §2.1, is the problem in $z \in \mathbb R^n$, $u \in \mathbb R^m$, $v \in \mathbb R$

$$\text{maximize } b^\top z - v \quad\text{subject to}\quad A^\top z + u = 0,\quad \|z\| \le 1,\quad \|[u; v]\| \le 1.$$

The minimum-norm solution of $Ax = b$ is a solution $x$ with $\|x\| \le \|y\|$ for every other solution $y$; when $Ax = b$ is consistent it is $A^\dagger b$, with $A^\dagger$ the Moore–Penrose pseudoinverse.

In the Lean development these objects are IsSOCPFeasible, IsSOCPOptimal, IsDualFeasible, dualObjective, IsDualOptimal and IsMinNormSolution, in the namespace RobustLS.Tikhonov, with the Euclidean norm eucNorm.

Formalization targets

Goal: Theorem 3.2 with the identity for $\mu$

Let $(x, \lambda, \tau)$ be optimal for (15) and set $\mu = (\lambda - \tau)/\tau$. Then

$$x = \begin{cases} (\mu I + A^\top A)^{-1}A^\top b & \text{if } \mu > 0,\\ A^\dagger b & \text{else,}\end{cases}\qquad\text{and}\qquad \mu = \frac{\|Ax - b\|}{\sqrt{\|x\|^2 + 1}}.$$

By Theorem 3.1 (the subject of the companion mission I of this series), the $x$-part of an optimal point of (15) is the RLS solution for $\rho = 1$, so this is formula (17) of the paper. The identity for $\mu$ is the final display of the paper's proof and is the claim in the mission's title.

Milestones (in the order of the paper's proof, p. 1041)

1. Both (15) and its dual have optimal points.
2. If $\lambda = \tau$ at the optimum, then $Ax = b$ and $\lambda = \tau = \sqrt{\|x\|^2 + 1}$.
3. In that case $x$ is the minimum-norm solution of $Ax = b$, $x = A^\dagger b$.
4. Eq. (18): for $\lambda > \tau$, primal and dual optimal values coincide,

$$\|Ax - b\| + \|[x;1]\| = \lambda = b^\top z - v = -(Ax-b)^\top z - [x^\top\ 1]\begin{bmatrix} -A^\top z\\ v\end{bmatrix}.$$

5. The dual optimal point is $z = -(Ax - b)/\|Ax - b\|$, $[u; v] = -[x; 1]/\sqrt{\|x\|^2 + 1}$.
6. Substituting into $A^\top z + u = 0$: $x = (A^\top A + \mu I)^{-1}A^\top b$ with $\mu = (\lambda - \tau)/\tau = \|Ax - b\|/\sqrt{\|x\|^2 + 1}$.

A further item states Remark 3.1: for $\lambda > \tau$, $x$ is the unique minimizer of the weighted residual $\big\|[A; I; 0]y - [b; 0; 1]\big\|_\Theta$ with $\Theta = \mathbf{diag}((\lambda-\tau)I, \tau I, \tau)$ and $\|r\|_\Theta = \|\Theta^{-1/2} r\|$.

Significance

The result. Theorem 3.2 turns a robust optimization problem into a familiar linear-algebra object. It says that the robust solution always lies on the Tikhonov path $\{(A^\top A + \mu I)^{-1}A^\top b : \mu > 0\}$ or at its endpoint $A^\dagger b$, and it identifies the point on the path through a fixed-point equation relating $\mu$ to the residual and the size of the solution. The paper builds on this in §3.3 (a one-dimensional search for $\mu$ via the SVD) and in §6 (continuity of the RLS solution in the data), and Remark 3.1 is the template for the weighted least-squares interpretation of the structured and linear-fractional problems in §5.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of second-order cone duality for a concrete program, the characterization of the optimal dual point by equality in the Cauchy–Schwarz inequality, and the minimum-norm characterization of $A^\dagger b$, all in terms of explicit Euclidean norms on Fin k → ℝ.

Difficulty

The paper's proof rests on strong duality for (15) ("both primal and dual problems are strictly feasible"), which it cites from the SOCP literature rather than proving; Mathlib has no second-order cone duality, so this step is the main gap. The degenerate case $\lambda = \tau$ also needs care: there $\|Ax - b\| = 0$, the residual term is not differentiable at the optimum, and the conclusion changes from a regularized inverse to a pseudoinverse. A statement that only handles the case $Ax \ne b$, or that assumes the matrix $A^\top A + \mu I$ invertible without deriving it from $\mu > 0$, misses part of the theorem.

Formalization scope

• Normalization. The paper states Theorem 3.2 for $\rho = 1$ ("we take $\rho = 1$ in what follows", p. 1039) and obtains general $\rho$ by the scaling $\varphi(A, b, \rho) = \rho\,\varphi(A/\rho, b/\rho, 1)$. Only the $\rho = 1$ statement is formalized.
• The RLS solution. The perturbation model is not used here: all statements are about optimal points of (15). That the $x$-part of such a point is the RLS solution is Theorem 3.1 (mission I), and it is recalled in prose only.
• Norms. Vectors are Fin k → ℝ; the Euclidean norm is the explicit eucNorm v = √(∑ vᵢ²) (Mathlib's ‖·‖ on Fin k → ℝ is the sup norm). Stacked vectors $[x;1]$ and $[u;v]$ are indexed by Fin m ⊕ Unit.
• Optimality. "Optimal point" means feasible with objective no worse than every feasible point; the minimum and maximum are therefore attained by definition, and milestone 1 guarantees they exist.
• Pseudoinverse. Mathlib has no matrix pseudoinverse, so $A^\dagger b$ is stated as the minimum-norm solution of $Ax = b$, which is how the proof uses it. The branch "else" is $\neg(\mu > 0)$.
• Inverse. $(\mu I + A^\top A)^{-1}$ is Mathlib's Matrix.inv; it is used only where $\mu > 0$, where the matrix is positive definite. $\tau \ge 1$ at every feasible point, so $\mu$ is well defined without an extra hypothesis.
• No trivialization. The goal quantifies over optimal points of (15) over the whole feasible set, not over feasible points, and milestone 1 shows the hypothesis is satisfiable for every $(A, b)$, including $n = 0$ or $m = 0$.
• Weighted norm. For Remark 3.1, $\|r\|_\Theta$ for the diagonal $\Theta$ is written as $\sqrt{\sum_i r_i^2/\theta_i}$, which equals $\|\Theta^{-1/2}r\|$ for positive weights.

Contributions welcome: second-order cone (or general conic) weak and strong duality for finite-dimensional programs, the equality case of Cauchy–Schwarz in the explicit-norm form used here, and a Moore–Penrose pseudoinverse for real matrices with its minimum-norm property. The platform's ConvexOptimization.conic_slater_strong_duality may help with the duality step.

Selected references

• L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• S. Chandrasekaran, G. H. Golub, M. Gu and A. H. Sayed, A new linear least-squares type model for parameter estimation in the presence of data uncertainties, cited as submitted to SIAM J. Matrix Anal. Appl. (reference [5] of the paper).
• A. N. Tikhonov and V. Y. Arsenin, Solutions of Ill-Posed Problems, Wiley, New York, 1977 (reference [43] of the paper).
• Y. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra Appl. 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

Motivation

A correlated equilibrium (Aumann 1974) is a joint distribution over the players' strategy profiles such that no player gains by deviating from the strategy the distribution recommends to them. It is the equilibrium notion that learning dynamics in repeated games most naturally reach, and a basic question in learning in games is which simple rules, played repeatedly, drive the empirical distribution of play to the set of correlated equilibria.

Foster and Vohra (1997) answer this with a hypothesis on forecasts instead of a particular algorithm. Each player forecasts the other's next move and best-responds to the forecast. They only require the forecasts to be calibrated in the sense of Dawid (1982): among the rounds in which a player forecast a given probability vector, the empirical frequencies of the opponent's moves must approach that vector. Their Theorem 1 says that this already forces the empirical joint distribution of play to approach the set of correlated equilibria. The paper uses this to argue that Bayesian players under a common prior, whose forecasts are calibrated by Dawid's theorem, end up playing a correlated equilibrium. That is an alternative to Aumann's (1987) derivation of correlated equilibrium from common priors and rationality.

Timeline:

• Aumann (1974, 1987) introduces correlated equilibrium and derives it from Bayesian rationality.
• Dawid (1982) proposes calibration as a minimal requirement on probability forecasts.
• Foster and Vohra (1997) prove Theorem 1 (this mission) and show that calibrated forecasts exist once the forecaster may randomize.
• Hart and Mas-Colell (2000) give regret matching, an adaptive procedure with the same limit set.

Setting

A finite two-player game $G$ has strategy sets $S(1) = \{0, \dots, m-1\}$ and $S(2) = \{0, \dots, n-1\}$ and payoff matrices $u_1, u_2 : S(1) \times S(2) \to \mathbb{R}$, which the players maximize. A joint distribution $D$ is a nonnegative $m \times n$ matrix with entries summing to $1$. It is a correlated equilibrium if

$$\sum_{x,y} D(x,y)\, u_1(\Phi(x), y) \le \sum_{x,y} D(x,y)\, u_1(x,y) \quad \text{for all } \Phi : S(1) \to S(1),$$

and symmetrically for player 2. The set of correlated equilibria is $\pi(G)$.

The game is played in rounds $s = 0, 1, 2, \dots$. In round $s$ player 1 issues a forecast $f_1(s)$, a probability vector over $S(2)$, and player 2 issues a forecast $f_2(s)$ over $S(1)$. Each player then plays a best response to its forecast, $x(s) = R_1(f_1(s))$ and $y(s) = R_2(f_2(s))$. Here $R_1$ and $R_2$ are best-reply functions: $R_1(p)$ maximizes $\sum_y p_y u_1(\cdot, y)$ for every probability vector $p$, and $R_1$ is a fixed function of the forecast alone. This is the paper's standing assumption of a stationary, deterministic tie-breaking rule.

For a forecast sequence $f$ and the opponent's plays $z$, $N(p,t)$ counts the rounds among the first $t$ in which $f$ forecast $p$. $\rho(p,j,t)$ is the fraction of those rounds in which the opponent played $j$, and $0$ if there are none. The forecast is calibrated with respect to $z$ if for every $j$

$$\sum_p |\rho(p,j,t) - p_j|\, \frac{N(p,t)}{t} \longrightarrow 0 \qquad (t \to \infty).$$

The empirical joint distribution $D_t(x,y)$ is the fraction of the first $t$ rounds in which player 1 played $x$ and player 2 played $y$.

Formalization targets

Goal: Theorem 1

If $f_1$ is calibrated with respect to $y$ and $f_2$ is calibrated with respect to $x$, then

$$\min_{D \in \pi(G)} \ \max_{x \in S(1),\, y \in S(2)} |D_t(x,y) - D(x,y)| \longrightarrow 0 \qquad (t \to \infty).$$

The goal fixes no rate and no particular forecasting method: it asserts only convergence of $D_t$ to the set $\pi(G)$, for every calibrated forecast.

Milestones: the steps of the proof (pp. 44–45)

1. $D_t$ lies in the simplex for $t \ge 1$.
2. For each $x \in S(1)$, the set $M_b(x)$ of mixtures to which $x$ is a best response is closed and convex.
3. The mixtures $M_p(x)$ at which player 1 actually plays $x$ satisfy $M_p(x) \subseteq M_b(x)$.
4. The identity writing $D_t(x,y)$ as a forecast-weighted term plus a calibration error.
5. Calibration makes the error term vanish.
6. The weighted average of the forecasts at which player 1 plays $x$ lies in $M_b(x)$.
7. For a convergent subsequence $D_{t_i} \to D$, every row of $D$ with positive mass, normalized, lies in $M_b(x)$.
8. Every subsequential limit of $D_t$ is a correlated equilibrium.

Further result: matching pennies (p. 46)

With the constant forecast $(1/2, 1/2)$ and the non-stationary tie-break "heads on even rounds, tails on odd rounds", both forecasts are calibrated and every play is a best reply, yet $D_t$ does not approach $\pi(G)$. The stationarity assumption cannot be dropped.

Significance

The result. Theorem 1 separates what learning needs from how it is achieved. Any forecasting procedure that is calibrated, combined with myopic best responses, yields correlated equilibrium behaviour in the long run. The paper's Theorem 3 constructs a randomized calibrated forecaster, so the theorem gives an uncoupled learning procedure for correlated equilibrium, one that needs no knowledge of the opponent's payoffs. The converse direction, that every correlated equilibrium arises this way for almost every game, is the paper's Theorem 2 (a separate mission of this series).

Formalizing it. The theorem is proved in the paper and has no machine-checked proof on Prove2Me or, to the knowledge of this mission, elsewhere. The platform's existing correlated-equilibrium results (the Algorithmic Game Theory swap-regret development, AGT.swap_regret_correlated_equilibrium) reach correlated equilibrium through swap regret of mixed strategies, a different hypothesis and a different object. This mission adds a formal notion of calibration and the convergence argument, both reusable for the paper's Theorems 2 and 3 and for later work on calibration and learning.

Difficulty

The obvious reading of calibration is that each player's forecast converges to the opponent's empirical distribution; if that held, best responses to it would give convergence. It does not hold. Calibration constrains the opponent's frequencies only conditionally on the forecast issued, and the forecasts need not converge at all. What must be shown is a statement about the conditional distributions of the joint play given each strategy of player 1, while the set of forecasts issued keeps growing. Rows of the limit with zero mass carry no conditional distribution. The "min → 0" form also asks for more than a property of limit points: it is a uniform statement about all large $t$.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; forecasts are real vectors required to be probability vectors in every round.
• A correlated equilibrium is the joint-distribution form of p. 44 (the correlated strategy on a finite probability space is represented by its law). It is the $\varepsilon = 0$, two-player, payoff (not cost) instance of the published AGT.IsCorrelatedEquilibrium, restated rather than imported.
• The stationary deterministic tie-break is modelled by arbitrary best-reply functions $R_i$ of the forecast. They do not depend on the round, and the statements quantify over all of them, which includes the lowest-index rule.
• Forecasts are sequences $f_i : \mathbb{N} \to \mathbb{R}^k$. The theorem uses only the realized forecasts, and every sequence is realized by a rule reading the round number from the history.
• Rounds are indexed from $0$: "the first $t$ rounds" are $0, \dots, t-1$. $D_0 = 0$ by Lean's division convention; only $t \ge 1$ and limits are used.
• The calibration sum runs over the forecasts issued in the first $t$ rounds, which is the paper's sum over all $p$ with its zero terms removed. $\rho(p,j,t) = 0$ when $N(p,t) = 0$, as on the page.
• "min … → 0" is stated as: for every $\varepsilon > 0$, eventually some $D \in \pi(G)$ is within $\varepsilon$ of $D_t$ in every coordinate. The two forms are equivalent because $\pi(G)$ is compact and nonempty. The formalization avoids an infimum over $\pi(G)$, which Lean would evaluate to $0$ on an empty set.
• A statement that drops the best-reply property, the probability-vector condition on forecasts, or the stationarity of $R_i$ is not Theorem 1: the matching pennies example shows the last one is essential. Swapping the calibration hypotheses (player 1's forecast calibrated against player 1's own plays) type-checks when $m = n$ and is not the theorem.
• Only the two-player case is claimed. The paper says the results "generalize easily to the $n$-person case" without proof.

Proofs of any milestone, and reusable lemmas about calibration scores and compactness of the simplex of joint distributions, are welcome.

Selected references

• D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997) 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• R. J. Aumann, Correlated equilibrium as an expression of Bayesian rationality, Econometrica 55 (1987) 1–18. https://doi.org/10.2307/1911154
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982) 605–610. https://doi.org/10.1080/01621459.1982.10477856
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

Least squares fits a model $Ax \approx b$ as if the data $(A, b)$ were exact. In practice they are measured, rounded or estimated, and the least-squares solution can be very sensitive to such errors. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to treat the errors as deterministic, unknown but bounded, and to choose $x$ minimizing the worst-case residual over all admissible data. For unstructured perturbations of $[A\ b]$ bounded in Frobenius norm this leads to a second-order cone program (missions I and II of this series).

In many applications the perturbations have a known structure: a Toeplitz matrix stays Toeplitz, a parameter enters several entries at once, or only some entries are uncertain. An unstructured bound then over-estimates the worst case. The paper's §4 treats perturbations that are affine in a parameter vector $\delta$ bounded in Euclidean norm, and shows that the resulting structured robust least-squares (SRLS) problem is still solved exactly, now by a semidefinite program (SDP). This model of uncertainty (an ellipsoid of affinely parametrized data) is the one later adopted as the basic uncertainty set of robust optimization; see Ben-Tal and Nemirovski, Math. Oper. Res. 23(4), 1998.

Setting

Vectors carry the Euclidean norm $\|v\| = \sqrt{v^Tv}$. Given matrices $A_0, A_1, \dots, A_p \in \mathbb{R}^{n\times m}$ and vectors $b_0, b_1, \dots, b_p \in \mathbb{R}^n$, define for every $\delta \in \mathbb{R}^p$

$$\mathbf A(\delta) = A_0 + \sum_{i=1}^p \delta_i A_i, \qquad \mathbf b(\delta) = b_0 + \sum_{i=1}^p \delta_i b_i .$$

For $\rho \ge 0$ and $x \in \mathbb{R}^m$ the structured worst-case residual is

$$r_S(\mathbf A, \mathbf b, \rho, x) = \max_{\|\delta\| \le \rho} \|\mathbf A(\delta)x - \mathbf b(\delta)\|,$$

and $x$ is an SRLS solution if it minimizes $r_S(\mathbf A, \mathbf b, \rho, \cdot)$ over $\mathbb{R}^m$. The paper takes $\rho = 1$ throughout §4 and writes $r_S(\mathbf A, \mathbf b, x)$.

For fixed $x$ let $M(x) = [A_1x - b_1\ \cdots\ A_px - b_p] \in \mathbb{R}^{n\times p}$ and

$$F = M(x)^TM(x), \qquad g = M(x)^T(A_0x - b_0), \qquad h = \|A_0x - b_0\|^2 .$$

Since $\mathbf A(\delta)x - \mathbf b(\delta) = (A_0x - b_0) + M(x)\delta$, the squared residual at $\delta$ is the quadratic function $h + 2g^T\delta + \delta^TF\delta$. Finally, for scalars $\lambda, \tau$,

$$\mathcal F(\lambda, \tau) = \begin{bmatrix} \lambda - \tau - h & -g^T \\ -g & \tau I - F \end{bmatrix}.$$

Formalization targets

Goal: Theorem 4.2

With $p \ge 1$ and $\rho = 1$, consider the SDP in $(\lambda, \tau, x)$

$$\text{minimize } \lambda \quad \text{subject to} \quad \begin{bmatrix} \lambda - \tau & 0 & (A_0x - b_0)^T \\ 0 & \tau I & M(x)^T \\ A_0x - b_0 & M(x) & I \end{bmatrix} \succeq 0. \tag{32}$$

The goal states that (a) for all $x$ and $\lambda$, some $\tau$ makes $(\lambda, \tau, x)$ feasible if and only if $r_S(\mathbf A, \mathbf b, x)^2 \le \lambda$; and (b) $(\lambda, \tau, x)$ is optimal for (32) if and only if $x$ is an SRLS solution, $\lambda = r_S(\mathbf A, \mathbf b, x)^2$, and $(\lambda, \tau, x)$ is feasible. This is the precise content of the paper's "the SRLS can be solved by computing an optimal solution of (32)".

Milestones

1. Lemma 2.1 (S-procedure), in two items: the multiplier condition is sufficient for every $p$; for $p = 1$ it is also necessary when $F_1(\zeta_0) > 0$ for some $\zeta_0$.
2. Eq. (28): $r_S(\mathbf A, \mathbf b, x)^2 = \max_{\delta^T\delta \le 1} [1;\delta]^T \begin{bmatrix} h & g^T \\ g & F\end{bmatrix} [1;\delta]$.
3. Eq. (29): for $\lambda \ge 0$, that quadratic form is $\le \lambda$ on the unit ball if and only if $\mathcal F(\lambda, \tau) \succeq 0$ for some $\tau$.
4. Theorem 4.1, first assertion: $r_S(\mathbf A, \mathbf b, x)^2 = \min\{\lambda : \exists \tau,\ \mathcal F(\lambda, \tau) \succeq 0\}$, the minimum attained.
5. §4.2, Schur-complement step: the matrix of (32) is positive semidefinite if and only if $\mathcal F(\lambda, \tau)$ is.

Significance

The result shows that a min–max problem over a nonconvex worst case (the inner problem maximizes a convex quadratic over a ball) is equivalent to a single convex SDP whose size is linear in $n$, $m$ and $p$, and hence solvable in polynomial time by interior-point methods. It covers as special cases the unstructured problem of §3, least squares with uncertainty in selected entries, and Toeplitz or otherwise patterned perturbations. The exactness contrasts with the next section of the paper, where the linear-fractional and $\ell_\infty$-bounded versions are in general only bounded from above, or shown NP-hard.

The result is proved in the paper; to the best of current knowledge it has not been formalized. The platform already has the one-constraint S-procedure (ConvexOptimization.s_procedure, proved, in a different sign and block convention); this mission adds the robust least-squares objects, the reduction to the S-procedure, the Schur-complement step, and the optimal-solution correspondence of Theorem 4.2. The worst-case residual and SDP (32) definitions are reusable by later robust-regression missions.

Difficulty

The obvious approach is to compute the inner maximum directly. The function $\delta \mapsto h + 2g^T\delta + \delta^TF\delta$ is convex, so its maximum over the unit ball is attained on the boundary, but it is not given by any closed-form expression in general, and maximizing a convex function is not a convex problem. Exactness therefore rests on the lossless S-procedure for one quadratic constraint, a nonconvex duality statement that fails for two or more constraints; the sufficient direction alone only yields an upper bound.

A second point is passing from "for fixed $x$" (Theorem 4.1) to "optimal over $x$" (Theorem 4.2): $\mathcal F(\lambda, \tau)$ is quadratic in $x$, and only the Schur-complement lift (32) is jointly affine in $(\lambda, \tau, x)$. The correspondence of optimal solutions must then be checked in both directions, including that the optimal $\lambda$ is the squared residual and not the residual.

Formalization scope

• Data are A0 : Matrix (Fin n) (Fin m) ℝ, A : Fin p → Matrix (Fin n) (Fin m) ℝ, b0 : Fin n → ℝ, b : Fin p → Fin n → ℝ; A i is the paper's $A_{i+1}$ (0-based index). Vectors live in Fin k → ℝ with the Euclidean norm written out as $\sqrt{\sum_i v_i^2}$, never Mathlib's sup norm.
• The maximum defining $r_S$ is sSup of the set of attained residuals over the closed ball; for $\rho \ge 0$ this set is nonempty and bounded, so sSup is the true maximum. The theorems use $\rho = 1$, as the paper does; the paper derives general $\rho$ by scaling and that is not stated here.
• Block matrices are Matrix.fromBlocks in the printed order (scalar block first: Unit ⊕ Fin p; for (32), (Unit ⊕ Fin p) ⊕ Fin n). "$\succeq 0$" is Mathlib's PosSemidef, which includes symmetry; all matrices here are symmetric by construction.
• $p \ge 1$ is assumed in (29), Theorem 4.1 and Theorem 4.2, although the paper does not state it: for $p = 0$ the block $\tau I$ is empty, $\tau$ is unconstrained, every $\lambda$ is feasible and both SDPs lose their meaning. Eq. (28), Lemma 2.1 and the Schur-complement step hold for every $p$ and are stated without it.
• Optimality in (32) is stated as feasibility plus $\lambda \le \lambda'$ for every feasible $(\lambda', \tau', x')$. A formalization that only proves existence of some feasible $\tau$, or only an inequality between the optimal values, is weaker than Theorem 4.2 and does not close the goal.
• Theorem 4.1's second and third assertions (the one-dimensional reformulation (30)–(31) and the worst-case perturbation) are not included: they use the notion "$(F, g)$-controllable", which the paper does not define.
• Useful infrastructure: Mathlib's Schur-complement lemmas (Matrix.PosSemidef.fromBlocks₂₂ and relatives in LinearAlgebra.Matrix.SchurComplement); the platform's ConvexOptimization.s_procedure and ConvexOptimization.single_constraint_quadratic_strong_duality with their definitions ConvexOptimization_quadraticForms, included as reference items. A bridge lemma between the platform's block convention and this mission's is a welcome contribution, as is a general-$\rho$ version.

Selected references

• L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994 (the S-procedure, p. 24). https://doi.org/10.1137/1.9781611970777
• A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• I. Pólik and T. Terlaky, A Survey of the S-Lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

Motivation

An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form $P = \{x \in \mathbb{R}^n : Ax \le b\}$ whose constraint matrix $A$ has entries $0, +1, -1$, but whose objective vector $w$ is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of $w$.

Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace $w$ by an integral objective $\tilde w$ whose entries have $O(n^3)$ bits and which has exactly the same optimal solutions and the same optimal dual bases as $w$ over every such polyhedron. Any algorithm that is polynomial in $n$ and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.

Setting

For $x \in \mathbb{R}^n$ write $\|x\|_\infty = \max_j |x(j)|$ and $\|x\|_1 = \sum_j |x(j)|$; $\operatorname{sign}$ takes the values $-1, 0, +1$.

Decomposition. Fix a positive integer $N$. A decomposition of $w \in \mathbb{R}^n$ is an expression

$$w = \sum_{i=1}^k \lambda_i v_i, \qquad \lambda_i > 0,\ v_i \in \mathbb{Z}^n.$$

It satisfies condition (iii) if for $i = 2, \dots, k$ the vector $v_i$ is nonzero and $\lambda_i/\lambda_{i-1} \le 1/(N\|v_i\|_\infty)$: the coefficients decrease so quickly that each term is negligible against the previous one.

Preprocessing. Given a rational $w$ and $N$, the paper's preprocessing algorithm finds a decomposition with $k \le n$, condition (iii), and the size bound (ii)' $\|v_i\|_\infty \le 2^{n^2+n}N^n$, and outputs

$$\tilde w = \sum_{i=1}^k M^{k-i} v_i, \qquad M = 2^{n^2+n} N^{n+1}.$$

Linear programs. Let $A$ be an $m \times n$ matrix with entries in $\{0, \pm 1\}$ and $b \in \mathbb{R}^m$. The primal program is $\max\{wx : Ax \le b\}$ and the dual program is $\min\{yb : yA = w,\ y \ge 0\}$. A point $\bar x \in P$ is $w$-maximal if $w\bar x = \max(wx : x \in P)$. A dual basis is a maximal set of row indices of $A$ whose rows are linearly independent; it determines at most one $y$ with $yA = w$ supported on it (the basic dual solution), and it is an optimal dual basis if that $y$ exists and is optimal for the dual program.

Formalization targets

Goal — Theorem 4.2 (p. 58)

For every $w \in \mathbb{Q}^n$, with $N = (n+1)! + 1$, there is $\tilde w \in \mathbb{Z}^n$ with

$$\|\tilde w\|_\infty \le 2^{4n^3} N^{n(n+2)}$$

such that for every $0, \pm1$ matrix $A$ with $n$ columns and every $b$: (i) $x \in P$ is $w$-maximal if and only if it is $\tilde w$-maximal; (ii) a set of rows of $A$ is an optimal dual basis for $w$ if and only if it is one for $\tilde w$. The vector $\tilde w$ depends on $w$ only, not on $A$ or $b$.

Milestones

1. Dirichlet's theorem (p. 52): for $N \ge 1$ and $\alpha \in \mathbb{R}^n$ there are $p \in \mathbb{Z}^n$ and $1 \le q \le N^n$ with $|q\alpha(i) - p(i)| < 1/N$ for all $i$.
2. Theorem 3.1 (p. 53): every $w \in \mathbb{R}^n$ has a decomposition with $k \le n$, $\|v_i\|_\infty \le N^n$ and condition (iii).
3. Lemma 3.2 (pp. 54–55): under condition (iii), for integral $b$ with $\|b\|_1 \le N - 1$, $\operatorname{sign}(b \cdot w) = \operatorname{sign}(b \cdot v_j)$ for the smallest $j$ with $b \cdot v_j \ne 0$, and $b \cdot w = 0$ if there is no such $j$.
4. Theorem 3.3 (p. 56): the preprocessed $\tilde w$ satisfies $\|\tilde w\|_\infty \le 2^{4n^3}N^{n(n+2)}$ and $\operatorname{sign}(w \cdot b) = \operatorname{sign}(\tilde w \cdot b)$ for all integral $b$ with $\|b\|_1 \le N-1$.
5. The case $N = n+1$ (p. 55): an integral $\tilde w$ with $\|\tilde w\|_\infty \le 2^{4n^3}(n+1)^{n(n+2)}$ and $\tilde w(X) \le \tilde w(Y) \iff w(X) \le w(Y)$ for all subsets $X, Y$ of coordinates.
6. Lemma 4.1 (i) (p. 57): if $\operatorname{sign}(w' \cdot h) = \operatorname{sign}(w'' \cdot h)$ for all integral $h$ with $\|h\|_1 \le (n+1)!$, then $w'$ and $w''$ have the same maximizers over $\{Ax \le b\}$ for every $0, \pm1$ matrix $A$.
7. Lemma 4.1 (ii) (p. 57): under the same hypothesis, a dual basis is optimal for $w'$ if and only if it is optimal for $w''$.

Significance

The result gives a general reduction: whenever a class of polyhedra with $0, \pm1$ constraint matrices admits an optimization algorithm that is polynomial in $n$ and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with $O(n^3)$-bit entries that orders all subset sums identically.

All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.

Difficulty

The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants $2^{n^2+n}N^n$ and $2^{4n^3}N^{n(n+2)}$. The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular $0, \pm1$ submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling $w$ to an integer vector by a common denominator, preserves every sign but gives no bound on $\|\tilde w\|_\infty$ in terms of $n$; the bound is the content of the theorem. Likewise, rounding each coordinate of $w$ separately to a fixed precision does not preserve the sign of $w \cdot b$ when $w \cdot b$ is tiny but nonzero.

Formalization scope

Vectors are functions on Fin n: the input $w$ is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and $A$ is a Matrix (Fin m) (Fin n) ℤ with every entry in $\{-1, 0, 1\}$, cast to $\mathbb{R}$; $b \in \mathbb{R}^m$ is unrestricted. Decompositions are indexed by $i \in \{1, \dots, k\} \subseteq \mathbb{N}$ as in the paper. $\|b\|_1$ is always the explicit sum $\sum_j |b(j)|$, compared with $N - 1$ in $\mathbb{Z}$; $\|v\|_\infty$ of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with $v_i \ne 0$, which the paper's quotient presupposes; without $v_i \ne 0$ Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.

Two formalizations would make the goal trivial and are excluded: dropping the bound on $\|\tilde w\|_\infty$ (a multiple of $w$ then works), and letting $\tilde w$ depend on $A$ and $b$ (the goal states $\exists \tilde w$ before $\forall A, b$). The $0, \pm1$ assumption on $A$ is part of every Section 4 statement.

A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for $0, \pm 1$ matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.

Selected references

• A. Frank and É. Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987) 49–65. https://doi.org/10.1007/BF02579200
• A. K. Lenstra, H. W. Lenstra Jr. and L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34(2) (1986) 250–256. https://doi.org/10.1287/opre.34.2.250
• M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• J. W. S. Cassels, An Introduction to the Theory of Numbers (title as printed in the paper's reference [2]), Springer, Berlin, 1971; cited in the paper as [2, Sect. 1.10] for Dirichlet's theorem.

Motivation

Many convex sets that appear in optimization have complicated descriptions in their own space but simple descriptions as projections of higher-dimensional sets. A polytope with exponentially many facets can be the shadow of a polyhedron with polynomially many; the unit disk is the projection of a slice of the cone of $2\times 2$ positive semidefinite matrices. Such a representation, a lift, turns linear optimization over the original set into a linear or semidefinite program over the lifted one, so the size of the smallest lift measures how hard the set is for conic optimization.

For polytopes and polyhedral lifts, Yannakakis (Yannakakis 1991) showed that the minimal size of a lift equals the nonnegative rank of the polytope's slack matrix. This turned questions about extended formulations into questions about matrix factorizations, and it is the basis of the lower bounds of Fiorini, Massar, Pokutta, Tiwary and de Wolf (2012) for the cut, stable set and traveling salesman polytopes. Lift-and-project hierarchies (Sherali–Adams, Lovász–Schrijver, Lasserre) all produce lifts to nonnegative orthants or positive semidefinite cones, so a criterion for the existence of a lift is also a criterion for when such a hierarchy can succeed.

Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 38(2), 2013) extended Yannakakis' theorem from polytopes and polyhedral cones to arbitrary convex bodies and arbitrary closed convex cones. Their Theorem 2.4 is the target of this mission.

Timeline:

• 1991, Yannakakis: polytopes, polyhedral lifts, nonnegative factorizations of the slack matrix.
• 2012, Fiorini, Massar, Pokutta, Tiwary, de Wolf: superpolynomial lower bounds on polyhedral lifts via nonnegative rank; a positive semidefinite analogue for polytopes.
• 2011/2013, Gouveia, Parrilo, Thomas: convex bodies and general closed convex cones (Theorem 2.4), with psd rank as the semidefinite analogue of nonnegative rank.

Setting

Throughout, $\mathbb R^k$ carries the Euclidean inner product $\langle\cdot,\cdot\rangle$.

A convex body is a set $C \subseteq \mathbb R^n$ that is convex, compact, and contains the origin in its interior. Its polar is

$$C^\circ = \{\, y \in \mathbb R^n : \langle x, y\rangle \le 1 \text{ for all } x \in C \,\}.$$

A point $p \in C$ is an extreme point if $p = (p_1+p_2)/2$ with $p_1,p_2\in C$ forces $p_1 = p_2 = p$; $\operatorname{ext}(C)$ is the set of extreme points. The slack operator of $C$ is

$$S_C : \operatorname{ext}(C)\times\operatorname{ext}(C^\circ) \to \mathbb R, \qquad S_C(x,y) = 1 - \langle x,y\rangle .$$

It is nonnegative, and for a polytope it is the slack matrix: rows indexed by vertices, columns by facet normals.

Let $K \subseteq \mathbb R^m$ be a full-dimensional closed convex cone: closed, convex, closed under nonnegative scaling, with nonempty interior. Its dual is $K^* = \{y : \langle x,y\rangle \ge 0 \ \forall x\in K\}$.

• A $K$-lift of $C$ is $Q = K\cap L$, where $L\subseteq\mathbb R^m$ is an affine subspace and $\pi:\mathbb R^m\to\mathbb R^n$ is a linear map with $C = \pi(K\cap L)$. The lift is proper if $L$ meets the interior of $K$ (Definition 2.1).
• $S_C$ is $K$-factorizable if there are maps, not necessarily linear, $A:\operatorname{ext}(C)\to K$ and $B:\operatorname{ext}(C^\circ)\to K^*$ with $S_C(x,y) = \langle A(x), B(y)\rangle$ for all $(x,y)$ (Definition 2.2).

In Lean these are IsConvexBody, IsClosedConvexCone, HasLift, HasProperLift and SlackFactorizable in the namespace ConeLifts.Factorization, together with the series' shared ConeLifts.Shared.polar and ConeLifts.Shared.dualCone.

Formalization targets

Goal: Theorem 2.4

For $n \ge 1$, a convex body $C\subseteq\mathbb R^n$ and a full-dimensional closed convex cone $K\subseteq\mathbb R^m$:

$$\bigl(C \text{ has a proper } K\text{-lift} \Rightarrow S_C \text{ is } K\text{-factorizable}\bigr) \;\wedge\; \bigl(S_C \text{ is } K\text{-factorizable} \Rightarrow C \text{ has a } K\text{-lift}\bigr).$$

The two implications are not an equivalence: the forward one assumes properness, and the lift produced by the converse may be improper.

Milestones

In the order the paper's proof uses them:

1. (§2, p. 3) $C = \operatorname{conv}(\operatorname{ext} C)$ and $C^\circ = \operatorname{conv}(\operatorname{ext} C^\circ)$.
2. (proof, p. 4) For every $c\in\operatorname{ext}(C^\circ)$, $\max\{\langle c,x\rangle : x\in C\} = 1$, attained.
3. (proof, p. 4) If $C = \pi(K\cap L)$, $L = w_0 + L_0$ and $w_0\in\operatorname{int}K$, then for $c \in \operatorname{ext}(C^\circ)$

$$1 = \min\{\langle w_0, z\rangle : z - \pi^*(c)\in K^*,\ z\in L_0^\perp\},$$

with the minimum attained. 4. (proof, p. 5) For $L = \{(x,z) : 1-\langle x,y\rangle = \langle z, B(y)\rangle\ \forall y\in\operatorname{ext}(C^\circ)\}$ and its projection $L_K$ to $\mathbb R^m$: $0\notin L_K$. 5. (proof, p. 5) If $B$ maps into $K^*$, $z\in K$ and $(x,z)\in L$, then $x\in C$. 6. (proof, p. 5) For each $z\in K\cap L_K$ there is a unique $x_z$ with $(x_z,z)\in L$.

Significance

The result. Theorem 2.4 makes the existence of a lift of a convex body to a given cone a purely algebraic question about its slack operator. Every lower bound on lift size in the paper and its successors goes through it: the nonnegative-rank bounds for polytopes (Section 4 of the paper), the proof that the stable set polytope of an $n$-vertex graph has no lift to $\mathcal S^n_+$ (Section 5), and the later psd-rank literature. It also puts Yannakakis' theorem and its semidefinite analogue under a single statement.

Formalizing it. The theorem is proved on paper; no machine-checked version is known to exist. Formalizing it requires conic strong duality with dual attainment under a Slater condition, which Mathlib does not have, and finite-dimensional Krein–Milman for the polar body. The companion missions of this series (nonnegative-rank lower bounds; stable set polytopes and psd lifts) use the correspondence as their entry point.

Difficulty

The converse half is elementary once the extreme points of $C^\circ$ are known to generate it. The forward half is not: $B(c)$ must be an element of $K^*$ that certifies $\langle c, x\rangle \le 1$ on $C$ through the lift. A separating functional gives this certificate on $\pi(K\cap L)$, but writing it as $z - \pi^*(c)$ with $z \perp L_0$, $z - \pi^*(c)\in K^*$ and $\langle w_0,z\rangle = 1$ exactly is conic duality with a zero gap and an attained dual optimum. For closed convex cones the gap can be positive or the dual unattained unless a constraint qualification holds; this is why properness is assumed. Weak duality alone gives only $\ge 1$, and a dual sequence approaching $1$ does not yield a factor. The paper notes (p. 5) that, since the proof uses strong duality, it is not obvious how to remove properness for a general closed convex cone.

Formalization scope

Conventions fixed by the Lean statements:

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k); every pairing, in $S$, in $K^*$ and in the factorization, is its inner product.
• The polar is one-sided, $\langle x,y\rangle\le 1$; Mathlib's absolute polar is not used.
• A convex body is compact, convex, with $0$ in its interior. The paper's "full-dimensional convex body in $\mathbb R^n$" is read as including $n\ge 1$: for $n = 0$, $C = \{0\}$ has the proper $\mathbb R^m$-lift $\{0\}$ while $S_C(0,0) = 1$ cannot factor through $K^* = \{0\}$, so the forward half is false there. The goal and milestones 2–3 assume $1\le n$.
• $K$ is closed, convex, contains $0$ and is closed under nonnegative scaling; full-dimensionality is (interior K).Nonempty. Pointedness is not assumed.
• $L$ is a Mathlib AffineSubspace and $\pi$ a linear map; the lift condition is the set equality $C = \pi(K\cap L)$.
• $A, B$ are total functions $\mathbb R^n\to\mathbb R^m$ constrained only on $\operatorname{ext}(C)$, resp. $\operatorname{ext}(C^\circ)$, which is equivalent to maps out of the extreme points. They are not required to be linear or continuous.
• Milestone 3 is the second, substituted form of the paper's dual ($z = M^{\mathsf T}y$), stated with L.directionᗮ and LinearMap.adjoint π; minima and maxima are stated with IsLeast/IsGreatest, so attainment is part of every claim.

Trivializing readings are excluded: $\pi$ is linear, not an arbitrary function (with an arbitrary function every set is a "lift"); $L$ is an affine subspace, not an arbitrary set; and $B$ takes values in $K^*$, not $K$, which for a cone that is not self-dual would be a different and generally false statement.

Needed infrastructure: finite-dimensional Krein–Milman in the form $C = \operatorname{conv}(\operatorname{ext} C)$ for compact convex sets (Mathlib has the closure form); the bipolar theorem $(C^\circ)^\circ = C$ for closed convex $C\ni 0$ with the one-sided polar; compactness of $C^\circ$ when $0\in\operatorname{int} C$; and conic linear programming duality with a Slater point, including dual attainment. The last two are reusable well beyond this mission. Proofs of individual milestones, and of these general facts as separate lemmas, are welcome.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2, doi:10.1287/moor.1120.0575
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. doi:10.1016/0022-0000(91)90024-Y
• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Linear vs. semidefinite extended formulations: exponential separation and strong lower bounds, STOC 2012. arXiv:1111.0837

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