Convex Optimization

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$, where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$, defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$, and $1\le n<m$. For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$, $W=\mathrm{diag}(w)$, $W^\alpha=\mathrm{diag}(w_i^\alpha)$, and $A_s=S^{-1}A$. For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$.

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$, and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .$$

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$, with $G(s)=\mathrm{diag}(g(s))$, $G'(s)$ the Jacobian of $g$ at $s$, and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$:

1. Size: $\|g(s)\|_1\le c_1$;
2. Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$;
3. Step consistency: $c_r\ge1$ and for all $r\ge c_r$, $y\in\mathbb R^m$: $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$;
4. Uniformity: $\|g(s)\|_\infty\le2$.

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$,

$$\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).$$

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

$$\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},$$

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$, and the resulting $g$ is a weight function with

$$c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .$$

Milestones: the three bullets of Theorem 1

• Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$.
• Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$.
• Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$.

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$-iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$-sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$. The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$, and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$) and $A^\top W^\alpha A$ (which defines $g$). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$, $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$-norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$, and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$, and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

• Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$).
• $1\le n<m$. $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
• Reading of $\alpha$: the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$, giving $\alpha\in(0,1)$.
• Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$, while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$).
• The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$.
• $g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$. Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and consider the linear program

$$\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .$$

The slack of a point $x$ is $s(x)=Ax-b$, and the interior is $S^0=\{x : Ax>b\}$, the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$, the weighted penalized objective is

$$f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .$$

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$.

Write $S_x=\mathrm{diag}(s(x))$, $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and the centrality are

$$\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.$$

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$, and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$.

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .$$

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$), and uniformity $\|\vec g(s)\|_\infty\le2$.

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$, let $x^{(old)}\in S^0$, $s^{(old)}=s(x^{(old)})$, and

$$x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$, then $x^{(new)}\in S^0$ and

$$\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$, the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$, $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$,

$$\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,$$

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$, and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$:

$$\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.$$

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$, $c_r$ and $\sqrt{c_1}$. The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$, $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$, which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$, $\frac1{4}$, $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$, so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$: without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$, while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$, and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

1. Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$, $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
2. Size as an upper bound. Definition 4's "$c_1(\vec g)=\|\vec g(s)\|_1$" is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
3. Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$.
4. Lemma 3's $r$ ranges over $r\ge0$, and $\gamma(x,w)$ means $\gamma(s(x),w)$.
5. Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
6. Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$, equal to $0$ for $m=0$).
7. The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$, spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
• Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Minimizing a smooth function over a closed convex set $\Omega\subseteq\mathbb R^n$ on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization: box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical projected gradient method of Goldstein and of Levitin and Polyak is simple and needs only gradients and projections, but with constant or Armijo-type step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients: the projected gradient direction; the Barzilai–Borwein (spectral) step length $\alpha_{k+1}=\langle s_k,s_k\rangle/\langle s_k,y_k\rangle$, an inverse Rayleigh quotient of the average Hessian along the last step; and the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last $M$ objective values instead of the current one. The method is widely used in practice, and its analysis is the template for many later nonmonotone projected methods.

Timeline:

• 1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
• 1976: Bertsekas analyses the Armijo rule along the projection arc.
• 1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
• 1988: Barzilai and Borwein propose the two-point step size; Raydan (1993, 1997) proves convergence for quadratics and combines it with nonmonotone search in the unconstrained case.
• 2000: Birgin, Martínez and Raydan define SPG1 and SPG2 for convex constraints (SIAM J. Optim. 10(4)).
• 2003: the same authors publish the convergence proof that Theorem 2.1 refers to, in the inexact setting (IMA J. Numer. Anal. 23).

Setting

Let $\Omega\subseteq\mathbb R^n$ be nonempty, closed and convex, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $f$ have continuous partial derivatives on an open set $U\supseteq\Omega$ and write $g(x)=\nabla f(x)$. The orthogonal projection $P(z)$ is the unique point of $\Omega$ nearest to $z$. The scaled projected gradient is $g_t(x)=P(x-t\,g(x))-x$ for $x\in\Omega$, $t>0$. A point $\bar x$ is a constrained stationary point if $\langle g(\bar x),x-\bar x\rangle\ge0$ for all $x\in\Omega$.

The parameters are an integer $M\ge1$, reals $0<\alpha_{\min}<\alpha_{\max}$, a sufficient-decrease constant $\gamma\in(0,1)$ and safeguards $0<\sigma_1<\sigma_2<1$. Algorithm SPG2 starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$ and at iteration $k=0,1,\dots$:

1. Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$, stop: $x_k$ is stationary.
2. Backtracking. Set $d_k=P(x_k-\alpha_k g(x_k))-x_k$ and $\lambda=1$. While

$$f(x_k+\lambda d_k)\le\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})+\gamma\lambda\langle d_k,g(x_k)\rangle\qquad(3)$$

fails, replace $\lambda$ by any $\lambda_{\rm new}\in[\sigma_1\lambda,\sigma_2\lambda]$. When (3) holds, $\lambda_k=\lambda$ and $x_{k+1}=x_k+\lambda_kd_k$. 3. Spectral step. With $s_k=x_{k+1}-x_k$, $y_k=g(x_{k+1})-g(x_k)$, $b_k=\langle s_k,y_k\rangle$: $\alpha_{k+1}=\alpha_{\max}$ if $b_k\le0$, else $\alpha_{k+1}=\min\{\alpha_{\max},\max\{\alpha_{\min},\langle s_k,s_k\rangle/b_k\}\}$.

In Lean the projection is a function P with the predicate IsProjOnto Ω P, $g_t$ is scaledProjGrad P f t, stationarity is IsConstrainedStationary Ω f, the maximum in (3) is nonmonotoneRef f x M k, and an infinite run is IsSPG2Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.1, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG2 and every accumulation point $\bar x$ of $(x_k)$,

$$\langle g(\bar x),x-\bar x\rangle\ge0\qquad\text{for all }x\in\Omega.$$

The statement fixes no parameter values and assumes neither convexity of $f$ nor a bounded level set.

Milestones

• Lemma 2.1 (ii). For $\bar x\in\Omega$ and $t\in(0,\alpha_{\max}]$: $g_t(\bar x)=0$ iff $\bar x$ is a constrained stationary point.
• Lemma 2.1 (i). For $x\in\Omega$ and $t\in(0,\alpha_{\max}]$:

$$\langle g(x),g_t(x)\rangle\le-\tfrac1t\|g_t(x)\|_2^2\le-\tfrac1{\alpha_{\max}}\|g_t(x)\|_2^2.$$

• Theorem 2.1, first clause (SPG2 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence reaches a step satisfying (3). The step is stated for an arbitrary reference value $R\ge f(x)$, which covers the maximum in (3).
• Section 2, p. 4. The iterates remain in $\Omega_0=\{x\in\Omega:f(x)\le f(x_0)\}$.

Significance

Theorem 2.1 is the global convergence guarantee for SPG2. It holds without monotone decrease of $f$ and without any restriction on the spectral step beyond the safeguards. These are the two features that make the method fast in practice, and together they mean that no classical monotone projected-gradient argument applies directly. The same statement underlies the convergence claims of the SPG software (ACM TOMS Algorithm 813) and of the many methods that reuse the nonmonotone spectral framework: inexact SPG, augmented Lagrangian inner solvers, and projected BB methods for machine learning.

Status: the theorem is proved in the literature. This paper's proof reads "See [7]", a pointer to Birgin, Martínez and Raydan (2003). No Lean formalization of this theorem, of the nonmonotone Armijo analysis, or of the projected-gradient stationarity lemma is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

The obvious argument for monotone descent methods is to show that $f(x_k)$ decreases, so that the total decrease is finite and the per-iteration decrease $\gamma\lambda_k|\langle d_k,g(x_k)\rangle|$ tends to zero. Here $f(x_k)$ need not decrease. Only the reference value $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum along the whole sequence does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$. A second difficulty is that the accepted step lengths $\lambda_k$ may tend to zero along the subsequence, while $f$ is $C^1$ only on a neighbourhood of $\Omega$ and no Lipschitz constant for $g$ is available, so no uniform sufficient-decrease estimate holds. The spectral steps $\alpha_k$ vary within $[\alpha_{\min},\alpha_{\max}]$, so the directions $d_k$ are not a fixed function of $x_k$.

Formalization scope

• Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. $f$ is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and $g$ is Mathlib's gradient f. The algorithm evaluates $f$ and $g$ only at points of $\Omega$.
• Iteration and trials. Iterations are indexed from $0$. The backtracking choice (2) is universally quantified: a run carries, at each iteration, a finite trial list $\lambda^{(0)}=1$, $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$, in which test (3) fails at every trial but the last and holds at the last.
• Step size. $\alpha_{k+1}$ is given by Step 3 exactly.
• Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
• Excluded simplifications. A run predicate that accepts any positive step, or lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$, is not SPG2. Nor is a goal stating $g_t(\bar x)=0$ instead of the variational inequality, or one that adds convexity of $f$, a Lipschitz gradient or a bounded level set.
• Non-vacuity. The hypotheses of the goal are satisfiable: for $f(x)=\|x\|^2$, $\Omega=\mathbb R^n$, $M=1$, $\alpha_{\min}=1/8$, $\alpha_{\max}=1/4$, $\gamma=1/2$ and $v\ne0$, the iterates $x_k=2^{-k}v$ with $\alpha_k=1/4$ form an infinite run with accumulation point $0$.
• Infrastructure. A complete development needs the variational characterization of the projection (Mathlib has it for the iInf form: norm_eq_iInf_iff_real_inner_le_zero), continuity properties of the projection, a mean-value estimate for $C^1$ functions on segments in $\Omega$, and the nonmonotone reference-value bookkeeping. The projection lemmas and the nonmonotone bookkeeping are reusable beyond this mission, in particular for the companion mission on SPG1, and contributions of them as separate lemmas are welcome.

Selected references

• E. G. Birgin, J. M. Martínez, M. Raydan, Nonmonotone spectral projected gradient methods on convex sets, SIAM J. Optim. 10(4) (2000) 1196–1211; authors' updated version, July 2004. https://doi.org/10.1137/S1052623497330963, https://www.ime.unicamp.br/~martinez/bmr.pdf
• E. G. Birgin, J. M. Martínez, M. Raydan, Inexact spectral projected gradient methods on convex sets, IMA J. Numer. Anal. 23 (2003) 539–559. https://doi.org/10.1093/imanum/23.4.539
• J. Barzilai, J. M. Borwein, Two-point step size gradient methods, IMA J. Numer. Anal. 8 (1988) 141–148. https://doi.org/10.1093/imanum/8.1.141
• L. Grippo, F. Lampariello, S. Lucidi, A nonmonotone line search technique for Newton's method, SIAM J. Numer. Anal. 23 (1986) 707–716. https://doi.org/10.1137/0723046
• M. Raydan, The Barzilai and Borwein gradient method for the large scale unconstrained minimization problem, SIAM J. Optim. 7 (1997) 26–33. https://doi.org/10.1137/S1052623494266365
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Trans. Automat. Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$, a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$-self-concordant ($\kappa\ge0$) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

$$\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},$$

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$-th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$. Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

$$\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},$$

and its logarithmic barrier (35) is

$$\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y$$

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$, with $h_1$ along $s$ and $h_2$ along $y$, and $h\in\mathbb R^3$ for $\varphi_B$.

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$,

$$|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}$$

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$-self-concordant on $F_f$.

Milestones (the displayed steps of the proof)

1. Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$.
2. The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$.
3. Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$:

$$\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.$$

4. Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$, then $\varphi_B$ is $(1+\beta/3)$-self-concordant on $F_f$.

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$. A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$.

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$, which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$, together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$. The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$, fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$. A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$. Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$, but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

• "$f:\mathbb R^+\to\mathbb R$" is read as $f$ convex on the open half-line $(0,\infty)$; the Burg case $f=-\log$ is undefined at $0$, and $f$ is only evaluated at $s/y$ with $s,y>0$.
• $f$ is assumed $C^3$ on $(0,\infty)$. The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$.
• The printed third-differential display ends in $s^3h_x^3/y^5$; the correct term is $s^3h_2^3/y^5$, and the Lean statement uses it. The milestone text keeps the printed version.
• Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$", which is false for $\beta<0$: with $f\equiv0$, (36) holds for every $\beta$ and $\beta=-3$ would give a $0$-self-concordant $-\ln z-\ln s-\ln y$. The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$, the domain is exactly $F_f$ (not a subset such as $\emptyset$), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$.

Selected references

• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
• D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
• Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791