Optimization

Motivation

Quadratic programming, the minimisation of a quadratic function subject to linear inequality constraints, is a basic subproblem of nonlinear optimisation (sequential quadratic programming, trust-region methods) and a model in its own right in portfolio selection, least-squares estimation and control. The classical solution methods are active-set methods: they keep a set of constraints treated as equalities, minimise over the resulting affine set, and then decide which constraint to drop or add (Gill, Murray and Wright, Practical Optimization, 1981; Fletcher, Practical Methods of Optimization, Vol. 2, 1981). Their finite-termination proofs need either a nondegeneracy assumption (linearly independent active constraints) or an anti-cycling rule, because under degeneracy the choice of the constraint to drop, made from Lagrange multiplier estimates, can cycle.

Calamai and Moré (Mathematical Programming 39, 1987) showed that the gradient projection method can take over the step that leaves a working set. Their Algorithm 6.1 alternates two kinds of step: an arbitrary non-increasing step that adds constraints to the working set until the equality-constrained subproblem is solved, and a single projected-gradient step once it is solved. Theorem 6.2 states that this algorithm terminates at a stationary point for every quadratic that is bounded below on the feasible polyhedron, with no nondegeneracy assumption and no anti-cycling rule. The same paper's Sections 2–4 (the subject of the first two missions of this series) supply the properties of the gradient projection step that the argument uses.

Timeline of the ingredients:

• 1964, 1966: Goldstein and Levitin–Polyak introduce the gradient projection method $x_{k+1} = P(x_k - \alpha_k\nabla f(x_k))$ for convex constraint sets.
• 1976: Bertsekas proves finite identification of the active constraints for bound constraints and the Armijo rule.
• 1981: Dunn uses the descent inequalities (2.4)–(2.5) in the analysis of the method.
• 1987: Calamai and Moré generalise the step rule to (2.1)–(2.2), prove convergence of projected gradients, identification of active constraints for general polyhedra, and finite termination of Algorithm 6.1.

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb{R}^n$ with a general inner product). The feasible set is a polyhedron

$$\Omega = \{x \in E : \langle c_j, x\rangle \ge \delta_j,\ j = 1, \dots, m\},$$

with active set $A(x) = \{j : \langle c_j, x\rangle = \delta_j\}$. The objective is a quadratic function $f(x) = \tfrac12\langle x, Qx\rangle + \langle b, x\rangle + c_0$ with $Q$ self-adjoint but not necessarily positive semidefinite, so $f$ may be nonconvex. Its gradient $\nabla f$ is taken with respect to the inner product of $E$.

The projection into $\Omega$ is $P(x) = \operatorname{argmin}\{\|z - x\| : z \in \Omega\}$, and a point $x^* \in \Omega$ is stationary if $\langle\nabla f(x^*), x - x^*\rangle \ge 0$ for every $x \in \Omega$.

A gradient projection step from $x_k$ is $x_{k+1} = P(x_k - \alpha_k\nabla f(x_k))$ with $\alpha_k > 0$ satisfying the sufficient decrease condition (2.1) with a constant $\mu_1 \in (0,1)$, the condition (2.2) that $\alpha_k \ge \gamma_1$ or $\alpha_k \ge \gamma_2\bar\alpha_k > 0$ for some $\bar\alpha_k$ at which the decrease test (2.3) with constant $\mu_2 \in (0,1)$ fails, and the upper bound $\alpha_k \le \gamma_3$ (3.2).

A working set is a set $W \subseteq \{1, \dots, m\}$; problem (6.2) is $\min\{f(y) : \langle c_j, y\rangle = \delta_j,\ j \in W\}$, over an affine set that ignores the inequality constraints outside $W$.

Algorithm 6.1 produces iterates $x_k \in \Omega$ and working sets $W_k \subseteq A(x_k)$ from $x_0 \in \Omega$:

• (a) if $x_k$ is a global minimiser of (6.2) for $W_k$, then $x_{k+1}$ is a gradient projection step from $x_k$;
• (b) otherwise $x_{k+1} \in \Omega$, $f(x_{k+1}) \le f(x_k)$, $W_k \subseteq W_{k+1}$, and if $W_{k+1} = W_k$ then $x_{k+1}$ is a global minimiser of (6.2).

Formalization targets

Goal: Theorem 6.2

For every quadratic $f$ bounded below on $\Omega$, all constants $\gamma_1, \gamma_2 > 0$, $\mu_1, \mu_2 \in (0,1)$, $\gamma_3 \in \mathbb{R}$, and every run $(x_k, W_k, \alpha_k)_{k\ge0}$ of Algorithm 6.1,

$$\exists\, l \ge 0 :\quad \langle \nabla f(x_l), x - x_l\rangle \ge 0 \quad \text{for all } x \in \Omega.$$

The theorem makes no assumption on the boundedness of the iterates and none on the linear independence of the constraints.

Milestones

• Lemma 2.1(a): for nonempty closed convex $\Omega$, $z \in \Omega$ and any $x$, $\langle P(x) - x, z - P(x)\rangle \ge 0$.
• Eq. (2.5): for $x_k \in \Omega$, $\alpha_k > 0$ and $x_{k+1} = P(x_k - \alpha_k\nabla f(x_k))$,

$$\langle\nabla f(x_k), x_k - x_{k+1}\rangle \ge \frac{\|x_{k+1} - x_k\|^2}{\alpha_k}.$$

Significance

Theorem 6.2 separates the two roles an active-set method plays: solving equality-constrained subproblems, for which any method that does not increase $f$ may be used, and choosing the next working set, which the gradient projection step does. The consequence is a finitely terminating quadratic programming algorithm for nonconvex quadratics that needs neither nondegeneracy nor an anti-cycling rule, and a template for large-scale bound-constrained and linearly constrained solvers that combine projection steps with subspace minimisation.

The result is proved in the paper and is classical; no machine-checked version is known. A formalization produces a checked finite-termination theorem for an active-set method on degenerate problems, together with reusable pieces: the projection onto a polyhedron as a total function with its variational inequality, the descent estimate of a projected step, and a predicate describing active-set runs with working sets, which other active-set algorithms can reuse.

Difficulty

The obvious argument — each step decreases $f$ and there are finitely many working sets — fails on two counts. First, step (b) only guarantees $f(x_{k+1}) \le f(x_k)$, so $f$ values alone do not rule out infinitely many iterations; the nesting of working sets and the final clause of step (b) are what bound consecutive (b)-steps. Second, a gradient projection step taken at a solution of (6.2) can in principle leave $f$ unchanged, and nothing in the algorithm's rules says directly that it makes progress; that it does so at every non-stationary iterate is a property of the projection and of the step conditions (2.1)–(2.2), not of the algorithm. A further point is that the minimum of (6.2) is taken over an affine set, not over $\Omega$, and the link between the value at a step-(a) iterate and later iterates runs through the requirement $W_k \subseteq A(x_k)$.

Formalization scope

The space is a finite-dimensional real inner product space E; $\nabla f$ is Mathlib's gradient. Constraints are indexed by Fin m, working and active sets are Finset (Fin m), and a run is a predicate IsAlgorithm61Run on three sequences $x : \mathbb{N} \to E$, $W$, $\alpha$ indexed from $0$. The run does not stop by itself; "the algorithm terminates at a stationary iterate" is rendered as the existence of an index $l$ with $x_l$ stationary. The projection is argmin made total by a junk value $0$ that is unreachable when $\Omega$ is nonempty, closed and convex. The paper's "$\subset$" between working sets is inclusion. A quadratic function is $\tfrac12\langle x, Qx\rangle + \langle b, x\rangle + c_0$ with $Q$ symmetric and no definiteness assumption.

A trivializing formalization — a run predicate that forces $x_0$ to be stationary, or that no sequence satisfies — would make the goal empty; the step rules here are the paper's verbatim, and a run on $\Omega = [0,\infty) \subset \mathbb{R}$ with $f(x) = x$ starting at the non-stationary point $x_0 = 1$ satisfies the predicate. Replacing step (a) by "any step that strictly decreases $f$" would assume the central fact and is not acceptable.

A complete development needs: the variational inequality of the projection (Lemma 2.1(a)), the descent estimate (2.5), the characterisation of stationary points as fixed points of the projected step, and a finiteness argument over the finitely many subsets of Fin m. Proofs of the milestones, of these auxiliary facts, and of the goal are all welcome.

Selected references

• P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Mathematical Programming 39 (1987) 93–116. https://doi.org/10.1007/BF02592073
• A. A. Goldstein, Convex programming in Hilbert space, Bulletin of the AMS 70 (1964) 709–710. https://doi.org/10.1090/S0002-9904-1964-11178-2
• E. S. Levitin and B. T. Polyak, Constrained minimization methods, USSR Computational Mathematics and Mathematical Physics 6 (1966) 1–50. https://doi.org/10.1016/0041-5553(66)90114-5
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Transactions on Automatic Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
• J. C. Dunn, Global and asymptotic convergence rate estimates for a class of projected gradient processes, SIAM Journal on Control and Optimization 19 (1981) 368–400. https://doi.org/10.1137/0319022
• P. E. Gill, W. Murray and M. H. Wright, Practical Optimization, Academic Press, 1981. https://doi.org/10.1137/1.9781611975604

Motivation

Minimizing a smooth function subject to linear inequality constraints is the core subproblem of much of nonlinear optimization: bound-constrained problems, quadratic programs, and the subproblems of sequential quadratic programming and augmented Lagrangian methods all have this form. Methods for these problems are usually built from two parts, one that decides which constraints hold with equality at the solution and one that solves the resulting equality-constrained problem quickly. The first part only pays off if the decision stabilizes after finitely many iterations; otherwise the fast local method never gets to run.

Calamai and Moré (Math. Programming 39, 1987) proved that this stabilization is a property of the limit point, not of the algorithm. Any feasible sequence that converges and whose projected gradients tend to zero identifies the active constraints of a nondegenerate limit in finitely many steps. This is the result that later active-set and gradient-projection methods for bound-constrained and linearly constrained problems invoke to justify switching to a fast local phase.

Timeline.

• 1976: Bertsekas proves finite identification of the active set for the gradient projection method with an Armijo step on bound constraints, at a local minimizer satisfying strict complementarity and second-order sufficiency.
• 1984: Gafni and Bertsekas (SIAM J. Control Optim. 22) prove a similar result for two-metric projection methods, under an assumption that excludes the choice of the gradient as search direction.
• 1987: Calamai and Moré remove the second-order condition, allow a general polyhedral feasible set and a general inner product, and make the result independent of the method generating the sequence (Theorem 4.1); they extend it to binding sets defined by multiplier estimates (Theorem 4.2).

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb{R}^n$ with a general inner product) and let $f : E \to \mathbb{R}$ be continuously differentiable on the feasible set, with gradient $\nabla f$ taken with respect to the inner product of $E$.

The feasible set is a polyhedral set

$$\Omega = \{x \in E : \langle c_j, x\rangle \ge \delta_j,\ j = 1, \dots, m\}$$

for constraint normals $c_j \in E$ and scalars $\delta_j$. The active set at $x$ is $A(x) = \{j : \langle c_j, x\rangle = \delta_j\}$.

A direction $v$ is feasible at $x \in \Omega$ if $x + \tau v \in \Omega$ for all sufficiently small $\tau > 0$. The tangent cone $T(x)$ is the closure of the set of feasible directions. The projected gradient is the point of $T(x)$ closest to $-\nabla f(x)$:

$$\nabla_\Omega f(x) = \operatorname{argmin}\{\|v + \nabla f(x)\| : v \in T(x)\}.$$

A point $x^* \in \Omega$ is stationary if $\langle \nabla f(x^*), x - x^*\rangle \ge 0$ for all $x \in \Omega$. It is a Kuhn–Tucker point if $\nabla f(x^*) = \sum_{j \in A(x^*)} \lambda^*_j c_j$ with $\lambda^*_j \ge 0$. It is nondegenerate if the active normals $\{c_j : j \in A(x^*)\}$ are linearly independent and the multipliers satisfy $\lambda^*_j > 0$ for every $j \in A(x^*)$.

A Lagrange multiplier estimate is a map $x \mapsto \lambda(x) \in \mathbb{R}^m$. It defines the binding set $B(x) = \{j \in A(x) : \lambda_j(x) \ge 0\}$. The estimate is consistent if $\lambda_j(x_k) \to \lambda_j(x^*)$ whenever $x_k \to x^*$, the point $x^*$ is a nondegenerate Kuhn–Tucker point, and $A(x_k) = A(x^*)$ for every $k$.

Formalization targets

Goal: Theorem 4.1 (finite identification of the active set)

Let $\{x_k\}$ be an arbitrary sequence in $\Omega$ converging to $x^*$. If $\|\nabla_\Omega f(x_k)\| \to 0$ and $x^*$ is nondegenerate, then

$$A(x_k) = A(x^*) \quad \text{for all sufficiently large } k.$$

The sequence need not come from any particular algorithm. The goal asserts eventual equality of the index sets, not inclusion.

Milestones

• Lemma 3.1. At $x \in \Omega$: $-\langle\nabla f(x), \nabla_\Omega f(x)\rangle = \|\nabla_\Omega f(x)\|^2$; $\min\{\langle \nabla f(x), v\rangle : v \in T(x), \|v\| \le 1\} = -\|\nabla_\Omega f(x)\|$; and $x$ is stationary if and only if $\nabla_\Omega f(x) = 0$.
• Lemma 3.3. The map $x \mapsto \|\nabla_\Omega f(x)\|$ is lower semicontinuous on $\Omega$.
• Tangent cone of a polyhedron (p. 105). For $x \in \Omega$, $T(x) = \{v : \langle c_j, v\rangle \ge 0,\ j \in A(x)\}$.
• Eq. (4.3). For polyhedral $\Omega$, a point $x^* \in \Omega$ is stationary if and only if it is a Kuhn–Tucker point.
• Theorem 4.2. Assume the binding sets come from a consistent estimate whose value at $x^*$ is the Kuhn–Tucker multiplier vector, and assume the hypotheses of Theorem 4.1. Then $B(x_k) = B(x^*)$ for all sufficiently large $k$.

Significance

The result. Theorem 4.1 separates identification from convergence. Any method that keeps its iterates feasible and drives the projected gradient to zero inherits finite identification, whatever its step-size rule or search direction. After identification the constrained problem is locally an unconstrained problem on the affine subspace $\{x : \langle c_j, x\rangle = \delta_j,\ j \in A(x^*)\}$, so Newton-type or conjugate-gradient methods can take over. Theorem 4.2 carries the same conclusion to methods that drop constraints according to the signs of multiplier estimates. The companion missions of this series use the result: the gradient projection method drives the projected gradients to zero (mission I), and a gradient projection algorithm for quadratic programs terminates finitely (mission III).

Formalizing it. The theorems are proved in the paper. No machine-checked version of the projected gradient, of tangent cones of polyhedra with their active-set description, or of finite active-set identification is known to exist. Formalization adds a reusable account of tangent cones and polar cones of polyhedral sets and of the equivalence between stationarity and the Kuhn–Tucker conditions for linear constraints, together with a method-independent identification theorem stated at the level of generality of the paper.

Difficulty

Two different limits are involved. Convergence $x_k \to x^*$ is enough to show that no inactive constraint of $x^*$ is active at $x_k$ for large $k$. The hard direction is the converse: a constraint active at $x^*$ might be inactive at infinitely many $x_k$, approached from the interior. Convergence of the points alone cannot rule this out. The projected gradient is also not continuous, because the tangent cone changes when a new constraint becomes active. So the hypothesis $\|\nabla_\Omega f(x_k)\| \to 0$ cannot be passed to the limit naively. Both nondegeneracy conditions matter: without linear independence, or with a zero multiplier, the statement fails.

Formalization scope

The space is a real inner product space E with [FiniteDimensional ℝ E], and $\nabla f$ is Mathlib's gradient. "Continuously differentiable on $\Omega$" means DifferentiableAt ℝ f x for every $x \in \Omega$ together with ContinuousOn (gradient f) Ω. The constraints are indexed by Fin m. $\Omega$ is polyhedron c δ, and $A(x)$ is activeSet c δ x : Finset (Fin m).

The tangent cone is defined as the closure of the feasible directions, not by the polyhedral formula, which is a milestone. The projected gradient is the nearest point of $T(x)$ to $-\nabla f(x)$, chosen by a choice function that returns $0$ only when no nearest point exists. That never happens at a point of a polyhedral set.

Nondegeneracy is bundled as IsNondegenerate c δ f x*: $x^* \in \Omega$, the family $(c_j)_{j \in A(x^*)}$ is linearly independent, and positive multipliers represent $\nabla f(x^*)$. "For all sufficiently large $k$" is ∀ᶠ k in Filter.atTop.

In Theorem 4.2 the paper leaves one condition implicit: the estimate at $x^*$ must be the Kuhn–Tucker multiplier vector, $\nabla f(x^*) = \sum_{j \in A(x^*)} \lambda_j(x^*) c_j$. Without it the statement is false, so it is an explicit hypothesis. Consistency is required only along feasible sequences and only in the coordinates $j \in A(x^*)$.

A formalization that assumes $A(x_k) \subseteq A(x^*)$, assumes the active sets are eventually constant, weakens nondegeneracy to nonnegative multipliers, or concludes only inclusion is not the paper's theorem and does not satisfy this mission.

Needed infrastructure: tangent cones of convex sets, the Moreau decomposition into a closed convex cone and its polar, Farkas' lemma in a general inner product space, and orthogonal projections onto subspaces spanned by linearly independent vectors. The polyhedral tangent-cone and Kuhn–Tucker results are reusable beyond this mission. Proofs of any milestone are welcome, as are auxiliary lemmas on polyhedral cones.

Selected references

• P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Mathematical Programming 39 (1987) 93–116. https://doi.org/10.1007/BF02592073
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Transactions on Automatic Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
• E. M. Gafni and D. P. Bertsekas, Two-metric projection methods for constrained optimization, SIAM Journal on Control and Optimization 22 (1984) 936–964. https://doi.org/10.1137/0322061
• E. H. Zarantonello, Projections on convex sets in Hilbert space and spectral theory, in: Contributions to Nonlinear Functional Analysis, Academic Press, 1971, 237–424.

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 gradient projection method of Goldstein and of Levitin and Polyak needs only gradients and projections, but with constant or monotone Armijo step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients. The first is the projection. The second is 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. The third is 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 paper defines two variants. This mission concerns SPG1, which backtracks along the projection arc $\lambda\mapsto P(x_k-\lambda g(x_k))$, as in Bertsekas's analysis of the Armijo rule for gradient projection. The companion mission concerns SPG2, which backtracks along a fixed feasible direction.

Timeline:

• 1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
• 1976: Bertsekas analyses the Armijo rule along the projection arc (IEEE TAC).
• 1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
• 1988: Barzilai and Borwein propose the two-point step size. Raydan (1997) 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 analysis that the proof of Theorem 2.2 adapts, 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$ and $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 SPG1 (Algorithm 2.1) starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$. At iteration $k=0,1,\dots$ it does the following.

1. Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$, stop: $x_k$ is stationary.
2. Backtracking along the projection arc. Set $\lambda=\alpha_k$. While the trial point $x_+=P(x_k-\lambda g(x_k))$ fails

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

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

The first trial of each backtracking is the spectral step $\alpha_k$, not $1$. The sufficient-decrease term in (1) is $\gamma\langle x_+-x_k,g(x_k)\rangle=\gamma\langle g(x_k),g_\lambda(x_k)\rangle$, with no factor $\lambda$.

In Lean these objects are written as follows:

• 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 (1) is nonmonotoneRef f x M k;
• test (1) is SPG1Test;
• an infinite run is IsSPG1Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.2, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG1 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 it 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$ if and only if $\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.$$

• Lemma 2.2 (i). For $x\in\Omega$ and $z\in\mathbb R^n$, the map $s\mapsto\|P(x+sz)-x\|/s$ is nonincreasing on $s>0$.
• Lemma 2.2 (ii). For every $x\in\Omega$ there is $s_x>0$ such that $f(P(x-tg(x)))-f(x)\le\gamma\langle g(x),g_t(x)\rangle$ for all $t\in[0,s_x]$.
• Theorem 2.2, first clause (SPG1 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence starting at $\alpha\in[\alpha_{\min},\alpha_{\max}]$ reaches a trial point satisfying (1). The statement is for an arbitrary reference value $R\ge f(x)$, which covers the maximum in (1).

Significance

Theorem 2.2 is the global convergence guarantee for SPG1. It holds without monotone decrease of $f$ and with no restriction on the spectral step beyond the safeguards. Lemma 2.2 carries Bertsekas's curvilinear Armijo analysis, stated for monotone gradient projection, over to the nonmonotone spectral setting. The projection-arc search is the natural one when $\Omega$ is a box or a polyhedron: there the arc is piecewise linear and each trial point is feasible by construction.

Status: the theorem is proved in the literature. This paper's proof reads "Use Lemma 2.2 with the proof technique of [7]", and Lemma 2.2 is quoted from Bertsekas's Nonlinear Programming (Lemma 2.3.1 and Theorem 2.3.3 (a)). No Lean formalization of this theorem, of the Armijo analysis along the projection arc, or of the monotonicity of $\|P(x+sz)-x\|/s$ is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

For monotone descent methods, the usual argument shows that $f(x_k)$ decreases, so the total decrease is finite and the per-iteration decrease tends to zero. That argument fails here, because $f(x_k)$ need not decrease. Only the window maximum $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$.

Along the projection arc there is a second obstacle. The decrease predicted by (1) is $\gamma\langle g(x_k),g_{\lambda_k}(x_k)\rangle$, and $g_\lambda(x_k)$ depends nonlinearly on $\lambda$: for $\lambda<\alpha_k$ the trial point is not a rescaling of the first one. So small accepted steps do not translate into small multiples of a fixed direction, as they do for SPG2. The step lengths $\lambda_k$ may also tend to zero, $f$ is $C^1$ only on a neighbourhood of $\Omega$, and no Lipschitz constant for $g$ is available.

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. Every trial point is a projection, so 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. At each iteration, a run carries a finite trial list with $\lambda^{(0)}=\alpha_k$ and $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$; test (1) 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.

• Lemma 2.2 (i). The paper names the domain $[0,\infty)$ but defines $h$ only for $s>0$, so the milestone is stated on $(0,\infty)$.

• Excluded simplifications. None of the following is SPG1:

  • a run predicate that accepts any positive step;
  • a run predicate that starts backtracking at $1$;
  • a run predicate that uses SPG2's test $\gamma\lambda\langle d_k,g(x_k)\rangle$;
  • a run predicate that lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$.

  Nor is a goal that states $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. Take $f(x)=\|x\|^2$, $\Omega=\mathbb R^n$, $M=1$, $\alpha_{\min}=1/8$, $\alpha_{\max}=1/4$, $\gamma=1/2$, $\sigma_1=1/10$, $\sigma_2=9/10$ and $v\ne0$. Then 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 in the iInf form, norm_eq_iInf_iff_real_inner_le_zero) and the nonexpansiveness of the projection;
  • a first-order expansion of a $C^1$ function along curves in $\Omega$;
  • the bookkeeping of the nonmonotone reference value.

  The projection lemmas, including Lemma 2.2 (i), are reusable for any gradient projection method and are welcome as separate contributions.

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
• D. P. Bertsekas, Nonlinear Programming, Athena Scientific, 1995, Section 2.3.
• 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
• 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

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

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

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

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

Milestones, in attack order

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

The k-median problem asks to open $k$ facilities among a set of candidate sites so that the total distance from clients to their nearest open facility is as small as possible. It is a basic model of facility location and of clustering, and it is NP-hard, so the question studied in approximation algorithms is how close a polynomial-time method can get to the optimum.

Local search is the method most used in practice: start from any $k$ facilities and repeatedly replace a few of them by others whenever this lowers the cost. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first analysis of a local search for k-median with a bounded performance guarantee using only $k$ medians. For single swaps they proved a locality gap of $5$ (Theorem 3.2, the subject of the first mission of this series); allowing up to $p$ facilities to be exchanged at once improves the gap to $3 + 2/p$, which the paper notes improves on the $4$-approximation of Charikar and Guha. That $p$-swap bound is the result this mission formalizes.

Timeline (as recounted in §1 of the paper):

• Shmoys, Tardos and Aardal, and Charikar, Guha, Tardos and Shmoys: LP rounding gives a $6\tfrac23$-approximation for k-median.
• Jain and Vazirani: primal–dual schema and Lagrangian relaxation give a $6$-approximation; Charikar and Guha improve it to $4$.
• Korupolu, Plaxton and Rajaraman: local search with add, delete and swap moves gives a solution with $k(1+\epsilon)$ facilities and service cost at most $3 + 5/\epsilon$ times the optimum.
• Arya et al.: locality gap $5$ for single swaps and $3 + 2/p$ for $p$-swaps with exactly $k$ facilities, with a tight example.
• Later work (Li and Svensson, 2013/2016) goes below $3$ with methods other than local search.

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji} = d(j,i)$ is the cost of serving client $j$ by facility $i$.

For a nonempty set $S \subseteq F$ of open facilities, each client is served by its nearest open facility, and

$$\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.$$

Fix an integer $p \ge 1$. A $p$-swap $\langle A, B\rangle$ deletes a set $A \subseteq S$ of at most $p$ facilities and adds a set $B \subseteq F$ of the same size. The $p$-swap neighbourhood of $S$ is

$$\mathcal B(S) = \{(S \setminus A) \cup B \mid A \subseteq S,\ B \subseteq F,\ |A| = |B| \le p\},$$

and $S$ is locally optimum when $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over instances, of the ratio between the cost of a locally optimum solution and the cost of a global optimum.

In Lean the instance is MetricInstance Cl Fa with the distance on Cl ⊕ Fa, the cost is kmCost I S hS (defined only for nonempty S), and local optimality is IsPSwapLocalOpt I p S hS, all in the namespace LocalSearchFL.MultiSwap.

Formalization targets

Goal: locality gap at most $3 + 2/p$

For every metric instance, every integer $p \ge 1$, every $k \ge 1$, every locally optimum $S$ with $|S| = k$, and every nonempty $O \subseteq F$ with $|O| \le k$,

$$\mathrm{cost}(S) \le \left(3 + \frac{2}{p}\right)\mathrm{cost}(O).$$

This is the bound concluded at the end of §3.4 (p. 553, announced p. 551). The comparison solution $O$ is arbitrary, not only an optimum, which is the strongest form printed.

Milestones

1. §3.4, p. 551: for sets $X, Y \subseteq S$, disjoint sets have disjoint captures, and $X \subseteq Y$ implies $\mathrm{capture}(X) \subseteq \mathrm{capture}(Y)$, where $\mathrm{capture}(A) = \{o \in O \mid |N_S(A) \cap N_O(o)| > |N_O(o)|/2\}$.
2. Claim 3.1, p. 552: when $|S| = |O|$, there are partitions $A_1,\dots,A_r$ of $S$ and $B_1,\dots,B_r$ of $O$ with $|A_i| = |B_i|$, $B_i = \mathrm{capture}(A_i)$ and exactly one bad facility in $A_i$ for $i < r$, and only good facilities in $A_r$.
3. §3.4, pp. 552–553: a family of swaps of size at most $p$ with positive weights, such that each $o \in O$ is swapped in with total weight exactly $1$, each $s \in S$ is swapped out with total weight at most $(p+1)/p$, and $\mathrm{capture}(A) \subseteq B$ for every swap $\langle A, B\rangle$.
4. Property 3.2, p. 553: a bijection $\pi$ of $N_O(o)$ with $\pi(P) \cap P = \emptyset$ for every class $P$ of a partition of $N_O(o)$ with $|P| \le \tfrac12|N_O(o)|$.

Significance

The bound shows that the simplest optimization heuristic, stopped at any local optimum, is within a constant factor of optimal for metric k-median, and that the factor tends to $3$ as the neighbourhood grows; the paper's tight example (§3.5, given for $p = 2$ and stated to generalize to every $p$) shows that the analysis cannot be improved for this neighbourhood. Combined with the standard $\varepsilon$-improvement rule (p. 548), it yields a polynomial-time $(3 + 2/p + \varepsilon)$-approximation. The analysis template (charging each client's reassignment through a bijection of $N_O(o)$, and averaging the local-optimality inequalities of carefully chosen swaps) was reused for facility location, capacitated variants and k-means.

The result has been proved since 2001. What this mission adds is a machine-checked proof: no formalization of the k-median problem or of any locality-gap bound is known to exist in Mathlib or on this platform. The combinatorial milestones (capture, the partition of Claim 3.1, the weighted swaps, the bijection of Property 3.2) are independent of the metric and are reusable in any local-search analysis of clustering objectives.

Difficulty

For single swaps each facility of $O$ is paired with one facility of $S$ and a direct counting argument suffices. With $p$-swaps, a facility of $S$ may capture several facilities of $O$ at once, and a group of facilities of $S$ may jointly capture a facility of $O$ that none of them captures alone. Pairing facilities one by one then fails: the clients of a captured facility cannot be reassigned cheaply unless the capturing set is swapped out together with everything it captures. Swapping whole groups is only allowed when a group has at most $p$ members; larger groups must be split into single swaps, and the weights must be chosen so that every facility of $O$ is counted exactly once while no facility of $S$ is counted more than $(p+1)/p$ times. Getting the constant $3 + 2/p$ (rather than a weaker one) depends on this exact accounting.

Formalization scope

• Clients and facilities are types Cl, Fa with Fintype and DecidableEq; solutions are Finset Fa. The distance is real-valued on Cl ⊕ Fa; d x x = 0 is not assumed (the paper neither states nor uses it).
• The cost is the nearest-facility cost of a nonempty set; the empty set has no cost, so no junk value enters. The bound is stated multiplied out, kmCost I S hS ≤ (3 + 2 / (p : ℝ)) * kmCost I O hO, with the constant computed in $\mathbb R$.
• $|S| = k$ is required; $O$ ranges over all nonempty sets with $|O| \le k$. §3.3 introduces multiswaps with $p > 1$; the statement takes $p \ge 1$, where $p = 1$ is Theorem 3.2 (bound $5$).
• Local optimality is over the whole neighbourhood (3), including sets $B$ that meet $S$, not only over the swaps used in the analysis. Restricting it to those swaps would state a theorem with a stronger hypothesis.
• The milestones state Claim 3.1, the swap construction and Property 3.2 in existence form; the procedure of Figure 8 is not formalized. Capture, good and bad are computed against the original $S$ and $O$. The client assignments in the milestones are arbitrary functions; nearest-facility assignments are a special case. Milestone 3 also records that the deleted sets of two swaps are equal or disjoint, which is immediate from the construction and is what makes Property 3.2 applicable.
• The per-swap reassignment inequality is not a milestone: the paper describes it only as "similar to the one presented for the single-swap heuristic" and prints no inequality.
• Out of scope: the tight example (§3.5), the polynomial-time wrapper, and arbitrary client demands.

Needed infrastructure: finite sums over clients, Finset.inf', permutations (Equiv.Perm), and a weighted double-counting argument over the swaps. Proofs of the combinatorial milestones and alternative routes to the goal are welcome.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. Charikar, S. Guha, É. Tardos, D. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
• K. Jain, V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
• M. Korupolu, C. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• S. Li, O. Svensson, Approximating k-Median via Pseudo-Approximation, SIAM J. Comput. 45(2):530–547, 2016. https://doi.org/10.1137/130938645

Motivation

Line searches are the step-size rules inside most methods for smooth unconstrained minimization $\min_{x \in \mathbb{R}^n} f(x)$: steepest descent, conjugate gradient, quasi-Newton and limited-memory methods all choose a direction $d_k$ and then a step $\alpha_k$ along it. Classical Armijo and Wolfe rules are monotone: they require $f(x_{k+1}) < f(x_k)$. Grippo, Lampariello and Lucidi (SIAM J. Numer. Anal., 1986) observed that insisting on monotone decrease can slow a method down, and proposed comparing $f(x_{k+1})$ with the maximum of the last $M$ function values instead. That max-based rule discards good function values and depends strongly on $M$, and Dai showed that R-linearly convergent iterates can violate it for every fixed memory $M$.

Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum by a weighted average of all previous function values. Their averaged nonmonotone line search is used in practical codes, for example with L-BFGS and in later nonmonotone spectral and conjugate-gradient methods. This mission formalizes the paper's first main result: global convergence to stationary points for nonconvex $f$.

Setting

Let $f : \mathbb{R}^n \to \mathbb{R}$ be continuously differentiable, with gradient $g_k = \nabla f(x_k)$ at the $k$-th iterate. The Nonmonotone Line Search Algorithm (NLSA) has parameters

$$0 \le \eta_{\min} \le \eta_{\max} \le 1, \qquad 0 < \delta < \sigma < 1 < \rho, \qquad \mu > 0.$$

It maintains weights $Q_k$ and reference values $C_k$:

$$Q_0 = 1,\ C_0 = f(x_0), \qquad Q_{k+1} = \eta_k Q_k + 1, \qquad C_{k+1} = \frac{\eta_k Q_k C_k + f(x_{k+1})}{Q_{k+1}}, \qquad (1.6)$$

with $\eta_k \in [\eta_{\min}, \eta_{\max}]$ chosen at each step. The iterates are $x_{k+1} = x_k + \alpha_k d_k$, where the step $\alpha_k > 0$ satisfies one of two rules, fixed for the whole run:

• the nonmonotone Wolfe conditions

$$f(x_k + \alpha_k d_k) \le C_k + \delta \alpha_k g_k^{\mathsf T} d_k \quad (1.4), \qquad \nabla f(x_k + \alpha_k d_k) d_k \ge \sigma g_k^{\mathsf T} d_k \quad (1.5);$$

• the nonmonotone Armijo conditions: $\alpha_k = \bar\alpha_k \rho^{h_k}$, where $\bar\alpha_k > 0$ is a trial step and $h_k$ is the largest integer such that (1.4) holds and $\alpha_k \le \mu$.

The choice $\eta_k = 0$ gives $C_k = f(x_k)$, the monotone line search; $\eta_k = 1$ gives $C_k = A_k = \frac{1}{k+1}\sum_{i \le k} f(x_i)$.

The direction assumption asks for constants $c_1, c_2 > 0$ with $g_k^{\mathsf T} d_k \le -c_1\|g_k\|^2$ (2.4) and $\|d_k\| \le c_2\|g_k\|$ (2.5) for all sufficiently large $k$. The level set is $\mathcal L = \{x : f(x) \le f(x_0)\}$, and $\bar{\mathcal L}$ is the set of points whose distance to $\mathcal L$ is at most $\mu d_{\max}$, where $d_{\max} = \sup_k \|d_k\|$.

Formalization targets

Goal: Theorem 2.2

Suppose $f$ is bounded from below, $g_k^{\mathsf T} d_k \le 0$ for every $k$, the direction assumption holds, and $\nabla f$ is Lipschitz continuous on $\mathcal L$ (Wolfe rule) or on $\bar{\mathcal L}$ (Armijo rule). Then

$$\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0, \qquad (2.6)$$

and if $\eta_{\max} < 1$,

$$\lim_{k \to \infty} \nabla f(x_k) = 0, \qquad (2.7)$$

so every limit of a convergent subsequence of iterates is a stationary point. No convexity is assumed.

Milestones

• Lemma 1.1: $f_k \le C_k \le A_k$ along the run, and a Wolfe step and a largest Armijo exponent exist whenever $g_k^{\mathsf T} d_k < 0$ and $f$ is bounded below.
• Eq. (1.8): $Q_{j+1} = 1 + \sum_{i=0}^{j} \prod_{m=0}^{i} \eta_{j-m} \le j+2$.
• Lemma 2.1: the lower bounds (2.1) and (2.2) on accepted Wolfe and Armijo steps.
• Eqs. (2.8)–(2.9): $f_{k+1} \le C_k - \beta\|g_k\|^2$ with the explicit constant

$$\beta = \min\left\{\frac{\delta\mu c_1}{\rho}, \frac{2\delta(1-\delta)c_1^2}{L\rho c_2^2}, \frac{\delta(1-\sigma)c_1^2}{Lc_2^2}\right\}.$$

• Eq. (2.14): $\sum_k \|g_k\|^2 / Q_{k+1} < \infty$.
• Eq. (2.15): $Q_{k+1} \le 1/(1-\eta_{\max})$ when $\eta_{\max} < 1$.
• Corollary 2.3: the analogue of Theorem 2.2 when (2.5) is replaced by the growth condition $\|d_k\|^2 \le \tau_1 + \tau_2 k$ (2.16).

Significance

Theorem 2.2 is the convergence guarantee that makes the averaged reference value $C_k$ usable in practice: any direction method whose directions are uniformly gradient-related (for example L-BFGS with bounded Hessian approximations) inherits stationarity of its limit points when combined with this line search, for every choice of the weights $\eta_k$. The monotone Wolfe and Armijo results are the special case $\eta_k \equiv 0$. The same estimates, (2.8) and (2.15), are the input to the paper's second main result, R-linear convergence for strongly convex $f$ (Theorem 3.1, a separate mission in this series).

The result is proved in the paper. It has no machine-checked proof that this mission is aware of: the platform has monotone backtracking statements for convex problems, but no nonmonotone line search, no Wolfe conditions and no Zoutendijk-type global convergence theorem for nonconvex $f$. A complete development also provides reusable Lean statements of the Wolfe and Armijo conditions and of step-size lower bounds under local Lipschitz continuity of the gradient.

Difficulty

Each step is elementary, but the argument has several places where a naive formalization fails. The Lipschitz hypothesis is only local: on $\mathcal L$ for the Wolfe rule, on the $\mu d_{\max}$-neighbourhood $\bar{\mathcal L}$ for the Armijo rule. So the proof must first show that every iterate stays in $\mathcal L$ even though $f(x_k)$ is not monotone. This needs $f_k \le C_k$ and the monotonicity of $C_k$, and then that the Armijo rule's rejected trial point $x_k + \rho\alpha_k d_k$ lies in $\bar{\mathcal L}$. The Armijo lower bound uses the maximality of the integer exponent $h_k$ and a first-order Taylor bound along a segment. The passage from (2.14) to (2.6) and (2.7) uses the two growth bounds on $Q_{k+1}$. The first gives only $\liminf$, since $\sum \|g_k\|^2/(k+2) < \infty$ does not force $g_k \to 0$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) with the Euclidean norm, $f$ is ContDiff ℝ 1, and the paper's row vector $\nabla f(x)$ acting on $d$ is the inner product of Mathlib's gradient f x with $d$. $Q_k$, $C_k$ and $A_k$ are defined by recursion from the run. A run is an infinite sequence $(x_k, d_k, \alpha_k, \eta_k)$ satisfying the update, $\eta_k \in [\eta_{\min}, \eta_{\max}]$, and the chosen rule at every $k$. The stopping test is not modelled. The Armijo exponent ranges over $\mathbb{Z}$ (it may be negative since $\rho > 1$), and "largest" is IsGreatest. $d_{\max}$ and the distance to $\mathcal L$ are computed in $[0, \infty]$, so unbounded directions give $\bar{\mathcal L} = \mathbb{R}^n$.

The following repairs and readings of the printed statements are made:

1. Theorem 2.2 and Corollary 2.3 assume $\nabla f(x_k) d_k \le 0$ for every $k$. The printed theorem constrains $d_k$ only for large $k$, but its proof needs $f(x_{k+1}) \le C_k$ at every step, which is the hypothesis of Lemma 1.1. Without it an early ascent step could leave $\mathcal L$, where nothing is assumed. The direction assumption itself stays "for all sufficiently large $k$".
2. $\liminf_k \|\nabla f(x_k)\| = 0$ is stated as "for every $\varepsilon > 0$, $\|\nabla f(x_k)\| < \varepsilon$ for infinitely many $k$".
3. The final "Hence" sentence of Theorem 2.2 is stated under $\eta_{\max} < 1$, from which it is derived.
4. In Corollary 2.3, "positive constants $\tau_1, \tau_2$" is read as $\tau_1 > 0$, $\tau_2 \ge 0$, since the corollary itself treats $\tau_2 = 0$.
5. Lemma 2.1 is stated pointwise for one iteration. Its Armijo case makes explicit the fact $f(x_k) \le C_k$ that the paper's proof invokes.

The following formalizations would make the goal trivial or empty and are ruled out:

• a (2.6) written with Lean's real liminf, which is $0$ for a divergent sequence;
• a run class in which the step rule does not constrain $\alpha_k$ (Wolfe without (1.4), Armijo without maximality of $h_k$), or which no sequence satisfies. The constant run $f \equiv 0$, $d_k = 0$ satisfies both rules, so the class is nonempty;
• assuming $\nabla f$ globally Lipschitz or the directions bounded.

Welcome contributions: proofs of the milestones in the listed order, and general lemmas on Wolfe and Armijo steps under local gradient Lipschitz continuity, which are reusable for other line-search methods.

Selected references

• H. Zhang, W. W. Hager, A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization, SIAM J. Optim. 14(4):1043–1056, 2004. https://doi.org/10.1137/S1052623403428208
• L. Grippo, F. Lampariello, S. Lucidi, A Nonmonotone Line Search Technique for Newton's Method, SIAM J. Numer. Anal. 23(4):707–716, 1986. https://doi.org/10.1137/0723046
• Y.-H. Dai, On the Nonmonotone Line Search, J. Optim. Theory Appl. 112(2):315–330, 2002. https://doi.org/10.1023/A:1013653923062