Convex Optimization

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$, $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$; $g_f(x)$ denotes an arbitrary subgradient at $x$, chosen once for each $x$. Let $M^*$ be the set of minimum points of $f$, assumed nonempty; for $x \in E_n$, $x^*(x)$ is the point of $M^*$ nearest to $x$.

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,$$

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

$$(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.$$

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$, asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$.

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$, $\sigma \ge \sqrt2$, $h_1 \ge \|x_0 - x^*\|/\sigma$, and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$, then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

$$\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots$$

Milestones

1. Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$,

$$\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .$$

2. Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
3. Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$.
4. Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$,

$$\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},$$

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$. 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$, the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$.

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$. The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$, so the iterates must be shown to stay in $Y$, and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$, $h_1$ being the chosen initial step (the book's "$k = 0, 1, 2, \dots$" in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$, never through $x/0 = 0$; the bounds are asserted for every $k$, which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$. The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$. In (2.16) the ratio is $1/(2\cos\varphi)$, as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$, which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$. In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$, nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
• J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
• L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

Motivation

Stochastic quasigradient (SQG) methods minimize an expectation $F(x)=E_\omega f(x,\omega)$ over a constraint set $X\subseteq\mathbb R^n$ when neither $F$ nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with $\rho_s\to0$, $\sum\rho_s=\infty$, $\sum\rho_s^2<\infty$. Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.

Timeline:

• 1951: Robbins and Monro, stochastic approximation with programmed steps.
• 1976: Ermoliev, Methods of Stochastic Programming: the SQG projection method and its a.s. convergence through stochastic quasi-Féjer sequences.
• 1983: Mirzoakhmedov and Uryasev (Zh. Vychisl. Mat. i Mat. Fiz., cited as [7] in Ch. 18 and [14] in Ch. 17): Cesàro convergence of the weighted mean with $\rho_s\to0$ and $\sum\rho_s=\infty$ only, under the two measurability regimes. Chapter 17 states it as Theorem (ii); Chapter 18 as Theorem 1.
• 1988: Uryasev, Ch. 18, applies it to the adaptive rule (18.5) (Theorem 2).
• 1992: Polyak and Juditsky, averaging of iterates for smooth stochastic approximation, with optimal asymptotic variance.

Setting

Let $X\subseteq\mathbb R^n$ be nonempty, convex and compact, $C_1=\max_{x,y\in X}\|x-y\|$ its diameter, and $F$ convex on an open convex set $U\supseteq X$, with subdifferential $\partial F(x)$. The projection $\pi_X(y)$ is the point of $X$ nearest to $y$. On a probability space, the SQG method generates

$$x^{s+1}=\pi_X(x^s-\rho_s\xi^s),\qquad s=0,1,\dots\qquad(18.2)$$

from $x^0\in X$, where the direction $\xi^s$ is a stochastic quasigradient: $E(\xi^s\mid B_s)=F_x(x^s)+b^s$ with $F_x(x^s)\in\partial F(x^s)$, a bias $b^s$, and $B_s$ the $\sigma$-algebra induced by $(x^0,\dots,x^s,\xi^0,\dots,\xi^{s-1})$.

The adaptive stepsize rule of the chapter is, for fixed $a>1$, $\delta>0$ and $\rho_0>0$,

$$\rho_{s+1}=\rho_s\,a^{\langle\xi^{s+1},\,x^s-x^{s+1}\rangle-\delta\rho_s}\qquad(18.5).$$

The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are

$$\bar x^s=\sum_{\ell=0}^s\rho_\ell x^\ell\Big/\sum_{\ell=0}^s\rho_\ell\qquad(18.6).$$

The sequence $x^s$ is Cesàro convergent when $\bar x^s$ converges to the solution set.

Chapter 17 (Pflug) uses the same method for $f(x)=E_P\,q(x,\xi)$ over a closed convex $S\subseteq\mathbb R^k$, with $Y=\nabla q(X_n,\xi_n)$ from i.i.d. $\xi_n$ and stepsizes adapted to $\sigma(\xi_0,\dots,\xi_{n-1})$.

Formalization targets

Goal: Theorem 2 of Chapter 18

Under $\sup_s\|\xi^s\|<C_2$ (18.15), $\limsup\|b^s\|\le\bar b$ (18.16) and $\delta>C_2\limsup_s\inf_{h\in\partial F(x^s)}\|\xi^s-h\|$ (18.17), almost surely,

$$\limsup_{s\to\infty}\Big(F(\bar x^s)-\min_{x\in X}F(x)\Big)\le\bar b\,C_1,$$

and if $b^s\to0$ a.s., then $F(\bar x^s)\to\min_XF$ and all accumulation points of $\bar x^s$ are minimizers, almost surely.

Milestones

1. Chapter 17, Theorem (i): $\sum\rho_n=\infty$ and $\sum\rho_n^2<\infty$ a.s. imply $X_n\to x^*$ a.s.
2. Chapter 17, Theorem (ii): for convex $f$ and bounded $S$, $\rho_n\to0$ and $\sum\rho_n=\infty$ a.s. imply $\bar X_n\to x^*$ a.s.
3. Chapter 18, Theorem 1: for any stepsizes with $\rho_s>0$, $E\rho_s^2<\infty$, $\rho_s\to0$, $\sum\rho_s=\infty$ and measurability condition (1) or (2), $\limsup F(\bar x^s)-F(x^*)\le\bar bC_1$ a.s.
4. Chapter 18, Corollary: with $b^s\to0$, the accumulation points of $\bar x^s$ are solutions.
5. Eq. (18.18): $\|x^{s+1}-x^s\|\le\|\rho_s\xi^s\|\le\rho_sC_2$.
6. Proof of Theorem 2, step 1: the adaptive steps satisfy $\sum\rho_s=\infty$.
7. Proof of Theorem 2, step 2: under (18.17), $\rho_s\to0$.
8. End of step 2: $\rho_s\to0$ implies $\rho_{s+1}/\rho_s\to1$.

Significance

Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only $\rho_s\to0$ and $\sum\rho_s=\infty$. It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to $1$.

The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).

Difficulty

The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls $\|x^s-x^*\|^2$ and needs $\sum\rho_s^2\|\xi^s\|^2<\infty$, which is exactly what is not available here. The averaged analysis has to show that the martingale term $\sum_\ell\rho_\ell\langle\xi^\ell-E(\xi^\ell\mid B_\ell),x^*-x^\ell\rangle$ is $o(\sum_\ell\rho_\ell)$ almost surely, and that $\sum_\ell\rho_\ell^2\|\xi^\ell\|^2$ is $o(\sum_\ell\rho_\ell)$, when the stepsizes are themselves random. Under condition (2) of Theorem 1, $\rho_s$ is not even measurable with respect to the $\sigma$-algebra of the conditional expectation. So $E(\rho_s\xi^s\mid B_s)\ne\rho_sE(\xi^s\mid B_s)$, and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither $\sum\rho_s=\infty$ nor $\rho_s\to0$ is given, and both must be derived path by path.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Sequences are indexed from $0$. Chapter 17 is shifted by one against the page: its $X_n,\xi_n,\mathcal F_n$, $n\ge1$, become indices $n-1$. Conditional expectations are Mathlib's condExp with respect to the history $\sigma$-algebras of the definition file. Every $\limsup$ bound is written out as "for every $\varepsilon>0$, eventually $\dots\le\dots+\varepsilon$", or in (18.17) as a bound $L$ with $C_2L<\delta$. Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.

Readings of the page, each recorded in the item's Formalization Note:

• (18.17) prints $C_1$. The proof's estimate gives $(C_2C_s-\delta)\rho_s$, and only $C_2$ is invariant under rescaling of $\mathbb R^n$, so $C_2$ is stated.
• (18.5) has two forms that agree only without projection. The proof uses the second, $a^{\langle\xi^{s+1},x^s-x^{s+1}\rangle-\delta\rho_s}$, which is stated.
• (18.8) prints $F_s(x^s)$ for $F_x(x^s)$. (18.11) prints $E\rho_s^s$, read as $E\rho_s^2<\infty$.
• Theorem 2's "$F(x^s)-\min z\in XF(x)\to0$" is read as $F(\bar x^s)-\min_XF\to0$.
• The end of step 2 prints $\rho_{s+1}/\rho_s\to0$, read as $\to1$.
• Chapter 17, assumption (ii) prints $\|\nabla f(x)\|\le A+B\|x-x^*\|^2$. The proof uses $\|\nabla f(x)\|^2$, and the printed form makes part (i) false, so the squared form is stated. $\mathrm{Var}(Y_x)\le C$ is read as $E\|Y_x-EY_x\|^2\le C$.
• The Corollary adds lower semicontinuity of $F$ on $X$, without which it fails.
• $x^0\in X$ is assumed, and $\rho_0$ in Theorem 2 is a fixed positive number.

No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.

A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the $\delta$ of (18.17) is the $\delta$ of the rule.

Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.

Selected references

• G. Ch. Pflug, Stepsize Rules, Stopping Times and their Implementation in Stochastic Quasigradient Algorithms, in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer 1988, Ch. 17. https://doi.org/10.1007/978-3-642-61370-8
• S. Uryasev, Adaptive Stochastic Quasigradient Procedures, ibid., Ch. 18. https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, Stochastic Quasigradient Methods, ibid., Ch. 6. https://doi.org/10.1007/978-3-642-61370-8
• F. Mirzoakhmedov and S. P. Uryasev, Adaptive step size control for stochastic optimization algorithm, Zh. Vychisl. Mat. i Mat. Fiz. 23(6) (1983) 1314–1325 (in Russian); cited in the volume above, no online copy linked.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• B. T. Polyak and A. B. Juditsky, Acceleration of Stochastic Approximation by Averaging, SIAM J. Control Optim. 30 (1992) 838–855. https://doi.org/10.1137/0330046

Motivation

Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.

Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$, $c \in \mathbb{R}^n$. The primal problem is to maximize $c^Tx$ subject to $Ax + w = b$, $x, w \ge 0$; the dual is to minimize $b^Ty$ subject to $A^Ty - z = c$, $y, z \ge 0$. A primal–dual point is a quadruple $(x, w, y, z)$ with $x, z \in \mathbb{R}^n$, $w, y \in \mathbb{R}^m$; it is strictly positive, $(x, w, y, z) > 0$, if every component is. Write $X, W, Y, Z$ for the diagonal matrices of $x, w, y, z$ and $e$ for the all-ones vector. The norms are $\|v\|_1 = \sum_j |v_j|$ and $\|v\|_\infty = \max_j |v_j|$.

At a point $(x, w, y, z)$ the three measures of progress are the primal infeasibility $\rho = b - Ax - w$, the dual infeasibility $\sigma = c - A^Ty + z$, and the complementarity $\gamma = z^Tx + y^Tw$. Fix parameters $0 < \delta < 1$ and $0 < r < 1$. One iteration of the method, from a strictly positive point, sets $\mu = \delta\gamma/(n+m)$, takes any solution $(\Delta x, \Delta w, \Delta y, \Delta z)$ of the Newton system

$$A\Delta x + \Delta w = \rho, \quad A^T\Delta y - \Delta z = \sigma, \quad Z\Delta x + X\Delta z = \mu e - XZe, \quad W\Delta y + Y\Delta w = \mu e - YWe,$$

computes the step length

$$\theta = r\left(\max_{i,j}\left\{\left|\tfrac{\Delta x_j}{x_j}\right|, \left|\tfrac{\Delta w_i}{w_i}\right|, \left|\tfrac{\Delta y_i}{y_i}\right|, \left|\tfrac{\Delta z_j}{z_j}\right|\right\}\right)^{-1} \wedge 1 \qquad (18.7)$$

(with $\theta = 1$ when all ratios vanish), and moves to $(x + \theta\Delta x, w + \theta\Delta w, y + \theta\Delta y, z + \theta\Delta z)$. This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts $^{(k)}$ denote the quantities at the $k$-th iterate, and $\theta^{(k)}$ is the step length computed there.

Formalization targets

Goal: Theorem 18.1 with the explicit constant

If $t > 0$, $M$ is real, and for all $k \le K$ one has $\theta^{(k)} \ge t$, $\|x^{(k)}\|_\infty \le M$, $\|y^{(k)}\|_\infty \le M$, then for all $k \le K$, with $\tilde t = t(1-\delta)$,

$$\|\rho^{(k)}\|_1 \le (1-t)^k\|\rho^{(0)}\|_1, \qquad \|\sigma^{(k)}\|_1 \le (1-t)^k\|\sigma^{(0)}\|_1, \qquad \gamma^{(k)} \le (1-\tilde t)^k \left(\gamma^{(0)} + \frac{M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)}{\delta t}\right).$$

Milestones

The one-step identities for the infeasibilities, $\tilde\rho = (1-\theta)\rho$ (18.8) and $\tilde\sigma = (1-\theta)\sigma$ (18.9); the one-step complementarity estimate

$$\tilde\gamma \le (1 - (1-\delta)\theta)\gamma + M\|\rho\|_1 + M\|\sigma\|_1 \qquad (18.10)$$

under $\|x\|_\infty, \|y\|_\infty \le M$; and the recursion $\gamma^{(k)} \le (1-\tilde t)\gamma^{(k-1)} + M(1-t)^{k-1}(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ (18.11). Two unnumbered statements complete the picture: every iteration has $0 < \theta \le 1$ and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies $|b^Ty - c^Tx| \le \gamma + \|\sigma\|_1\|x\|_\infty + \|\rho\|_1\|y\|_\infty$ (§18.5.3).

Significance

Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor $1 - t$ per iteration while the complementarity, and hence (by the duality-gap estimate) the gap $b^Ty - c^Tx$, falls only by $1 - \tilde t$. The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.

All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.

Difficulty

The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term $\theta^2(\Delta y^T\rho - \sigma^T\Delta x)$ that has no sign. Bounding it requires relating the size of the step $\theta\Delta$ to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon $K$ is what makes the statement non-trivial.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, $A$ is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case $\theta = 1$ when all ratios vanish, since Lean's r / 0 = 0 would otherwise give $\theta = 0$. An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current $+\ \theta \cdot$ direction. The hypotheses $0 < \delta < 1$, $0 < r < 1$ (pp. 272–273) are stated in every theorem; $M$ is an arbitrary real number and $K$ a natural number. As in the book, the hypotheses of Theorem 18.1 range over $k \le K$, so the iteration from index $K$ is part of the data.

Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant $\bar M < \infty$". Because $K$ is fixed, that existential is satisfied trivially by $\max_{k \le K}\gamma^{(k)}/(1-\tilde t)^k$, and a statement with $\exists \bar M$ would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): $\bar M = \gamma^{(0)} + M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)/(\delta t)$. Eq. (18.11) is stated with the book's $\tilde M = M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ written out.

The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 18, pp. 269–283. https://doi.org/10.1007/978-1-4614-7630-6
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

Motivation

Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges, as the simplex method does. The methods used in practice are path-following methods: they track a curve, the central path, that runs through the interior of the feasible region and ends at an optimal solution. Before any such method can be analysed, the curve has to exist. This mission formalizes Chapter 17 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014), which defines the central path through the logarithmic barrier problem and proves that it exists exactly when the primal and the dual problem both have strictly positive feasible points.

The chapter's results have a short history. Barrier methods for nonlinear programming go back to Fiacco and McCormick (1968). Interest in interior-point methods for linear programming began with Karmarkar (1984), whose projective algorithm does not mention a central path; the connection between Karmarkar's method and the primal–dual central path was found by Megiddo (1989), with central points traced back to Huard (1967) and an extended study of the path by Bayer and Lagarias (1989). The chapter is the textbook entry point to this line of work and the foundation for the path-following algorithm of Chapter 18.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ and $c \in \mathbb{R}^n$. The primal linear program is to maximize $c^T x$ subject to $Ax \le b$, $x \ge 0$; its dual is to minimize $b^T y$ subject to $A^T y \ge c$, $y \ge 0$. With slack variables $w \in \mathbb{R}^m$ and $z \in \mathbb{R}^n$ they read (17.1)

$$Ax + w = b,\ x, w \ge 0 \qquad\text{and}\qquad A^T y - z = c,\ y, z \ge 0.$$

For a vector $\xi$, $\xi > 0$ means that every component is strictly positive. The primal feasible region has nonempty interior when some $(\bar x, \bar w)$ satisfies $A\bar x + \bar w = b$ with $\bar x > 0$, $\bar w > 0$; the dual feasible region has nonempty interior when some $(\bar y, \bar z)$ satisfies $A^T \bar y - \bar z = c$ with $\bar y > 0$, $\bar z > 0$.

For a parameter $\mu > 0$, the barrier function (17.7) is

$$f(x, w) = c^T x + \mu \sum_{j=1}^n \log x_j + \mu \sum_{i=1}^m \log w_i ,$$

and the barrier problem (17.2) is to maximize $f(x, w)$ subject to $Ax + w = b$, over the domain $x > 0$, $w > 0$ where the logarithms are finite. A solution of the barrier problem is a point of that domain at which $f$ attains its maximum over the domain.

Writing $X, Z, Y, W$ for the diagonal matrices carrying $x, z, y, w$ and $e$ for the all-ones vector, the primal–dual central-path system (17.6) is

$$Ax + w = b, \qquad A^T y - z = c, \qquad XZe = \mu e, \qquad YWe = \mu e,$$

with $x, w, y, z > 0$. The last two equations say $x_j z_j = \mu$ and $y_i w_i = \mu$ for all $j$ and $i$. The set of its solutions $(x_\mu, w_\mu, y_\mu, z_\mu)$, $\mu > 0$, is the primal–dual central path.

The chapter also uses one fact from nonlinear programming: for the problem "maximize $f(x)$ subject to $g_i(x) = 0$, $i = 1, \dots, m$", a critical point is a feasible $x^*$ with $\nabla f(x^*) = \sum_i y_i \nabla g_i(x^*)$ for some Lagrange multipliers $y_i$ (17.3), and $H_f(x^*)$ is the Hessian of $f$ at $x^*$.

Formalization targets

Goal: Theorem 17.2 (p. 265)

For each fixed $\mu > 0$,

$$\exists\, (x, w) \text{ solving the barrier problem} \iff \big(\exists\, \bar x, \bar w > 0 : A\bar x + \bar w = b\big) \wedge \big(\exists\, \bar y, \bar z > 0 : A^T\bar y - \bar z = c\big).$$

Both directions are part of the goal. The statement fixes no constants and no rate; it asserts only when the barrier problem is solvable.

Milestones

1. Theorem 17.1 (p. 261), second-order sufficiency under linear constraints: if the constraints are linear, a critical point $x^*$ with $\xi^T H_f(x^*)\xi < 0$ for every $\xi \ne 0$ satisfying $\xi^T \nabla g_i(x^*) = 0$ for all $i$ is a local maximum on the feasible set.
2. Exercise 10.7 (p. 150): if the primal is feasible and its feasible set $\{x : Ax \le b,\ x \ge 0\}$ is bounded, then there are $y > 0$, $z > 0$ with $A^T y - z = c$.
3. Corollary 17.3 (p. 266): if the primal feasible set (or the dual feasible set) has nonempty interior and is bounded, then for each $\mu > 0$ the system (17.6) has exactly one solution with $x, w, y, z > 0$.

The corollary is stronger than the goal in one direction (it adds uniqueness and the dual variables) and weaker in another (it assumes boundedness).

Significance

The result itself. Theorem 17.2 gives an exact criterion for the barrier problem to be solvable for a fixed $\mu$, and Corollary 17.3 turns it into the statement that the central path is a well-defined curve $\mu \mapsto (x_\mu, w_\mu, y_\mu, z_\mu)$ for all $\mu > 0$. Every path-following method, including the one analysed in Chapter 18 of the same book, targets points on this curve; without existence and uniqueness the "target" of an iteration is undefined. The system (17.6) is also the starting point of the primal–dual Newton step.

Formalizing it. These results are classical and proved in the book; none is formalized in the $Ax \le b$, $x \ge 0$ form used here. The platform has the converse fact in the standard form $Ax = b$, $x \ge 0$ (a solution of the central-path conditions minimizes the barrier, Introduction to Linear Optimization), but not existence. A formal proof of Theorem 17.2 and Corollary 17.3 produces a reusable existence theorem for the central path that downstream missions on path-following and self-dual methods can import.

Difficulty

The "if" direction of Theorem 17.2 is an existence claim on a set that is neither closed nor bounded: the domain $x > 0$, $w > 0$ is open, and the feasible region itself may be unbounded, so the obvious appeal to "a continuous function on a compact set attains its maximum" does not apply directly. The example "maximize $0$ subject to $x \ge 0$" (p. 264), whose barrier $\mu \log x$ has no maximum, shows that the dual hypothesis cannot be dropped. The "only if" direction, which the book calls trivial and does not prove, needs first-order conditions at a maximizer over a relatively open set.

Theorem 17.1 needs a second-order Taylor expansion with a remainder that is $o(\|\xi\|^2)$ uniformly along the constraint subspace, not along individual lines. Exercise 10.7 is a theorem of the alternative and is not a consequence of weak duality alone. Uniqueness in Corollary 17.3 requires the positivity of the solution: the equations $x_j z_j = \mu$, $y_i w_i = \mu$ admit sign-flipped solutions.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; $A$ is a Matrix (Fin m) (Fin n) ℝ. The book's primal–dual pair in $Ax \le b$, $x \ge 0$ form with slacks is used throughout; there are no explicit constants in this chapter.

Conventions committed to:

• "Nonempty interior" means a feasible point with every component strictly positive, as the proof of Theorem 17.2 says. The topological interior of $\{(x, w) : Ax + w = b,\ x, w \ge 0\}$ in $\mathbb{R}^{n+m}$ is empty whenever $m \ge 1$; reading the theorem that way would make its right-hand side always false for $m \ge 1$, and that reading is ruled out.
• The barrier problem is posed over $x > 0$, $w > 0$ explicitly; Real.log returns $0$ at nonpositive arguments and is never evaluated there.
• Solutions of (17.6) are required to be strictly positive, as in Exercise 17.3 (p. 267).
• "Bounded" is Bornology.IsBounded of the feasible set in $\mathbb{R}^n$ (resp. $\mathbb{R}^m$).
• In Theorem 17.1 the constraints are $Gx = \beta$; $f$ is differentiable near $x^*$ with derivative differentiable at $x^*$, and $\xi^T H_f(x^*) \xi$ is the second Fréchet derivative applied to $(\xi, \xi)$. The local maximum is relative to the feasible set.

Infrastructure a complete development needs: attainment of maxima on compact sets (IsCompact.exists_isMaxOn in Mathlib), first-order conditions on relatively open sets, a theorem of the alternative for Exercise 10.7, and concavity facts about the logarithm. A second-order sufficient condition under affine constraints is not in Mathlib and is reusable beyond linear programming. Proofs of any milestone, including the "only if" half of the goal separately, are welcome contributions.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 17 and Exercise 10.7. https://doi.org/10.1007/978-1-4614-7630-6
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968. https://doi.org/10.1137/1.9781611971316
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4 (1984), 373–395. https://doi.org/10.1007/BF02579150
• N. Megiddo, Pathways to the optimal set in linear programming, in Progress in Mathematical Programming, Springer, 1989, 131–158. https://doi.org/10.1007/978-1-4613-9617-8_8
• D. A. Bayer and J. C. Lagarias, The nonlinear geometry of linear programming I, II, Transactions of the AMS 314 (1989), 499–526 and 527–581. https://doi.org/10.1090/S0002-9947-1989-1005525-6