Convex Optimization

Motivation

For a convex function on $\mathbb R^n$, a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice $\mathbb Z^n$ can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.

Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of $\mathbb Z^n$-valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the $3^n - 1$ neighbors obtained by independently nudging each coordinate by $-1$, $0$, or $+1$ (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.

Setting

Let $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ be a function with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f = \{x \in \mathbb Z^n : f(x) \ne +\infty\}$. The convex closure of $f$ is

$$\bar f(x) = \sup_{p \in \mathbb R^n,\, \alpha \in \mathbb R} \{\langle p,x\rangle + \alpha : \langle p,y\rangle + \alpha \le f(y)\ \forall y \in \mathbb Z^n\} \qquad (x \in \mathbb R^n),$$

the pointwise supremum of every affine function minorizing $f$ on all of $\mathbb Z^n$. If $\bar f$ agrees with $f$ on integer points, $f$ is convex extensible. The integral neighborhood of $x \in \mathbb R^n$ is

$$N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil,\ 1 \le i \le n\},$$

and the local convex extension $\tilde f$ relaxes $\bar f$'s definition by requiring the affine minorant condition only on $N(x)$ rather than on all of $\mathbb Z^n$. Always $\tilde f \ge \bar f$ pointwise, and the two agree on $\mathbb Z^n$. A function $f$ is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ — equivalently, if $\tilde f$ is a convex function on all of $\mathbb R^n$ (it is automatically convex on every unit cube $[z, z+1]^n$ with $z \in \mathbb Z^n$, but need not be convex globally without this extra condition).

A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S$ equals the set of integer points in its own real convex hull, and $\arg\min f[-p]$ denotes the minimizer set, over $\mathbb Z^n$, of the linearly perturbed function $f[-p](x) = f(x) - \langle p,x\rangle$.

Formalization targets

Goal: Theorem 3.21 (local optimality characterizes global optimality)

For integrally convex $f$ and $x \in \operatorname{dom}_{\mathbb Z} f$:

$$f(x) \le f(y)\ (\forall y \in \mathbb Z^n) \iff f(x) \le f(x + \chi_Y - \chi_Z)\ (\forall\, Y, Z \subseteq \{1,\dots,n\}),$$

where $\chi_Y \in \{0,1\}^n$ is the indicator vector of $Y$. The right-hand side is a check over at most $3^n - 1$ points (each coordinate independently unchanged, incremented, or decremented), regardless of how large $\operatorname{dom}_{\mathbb Z} f$ is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single $(Y,Z)$ or letting the right-hand side range over all of $\mathbb Z^n$ would trivialize or falsify the equivalence.

Milestones: Propositions 3.18 and 3.19

Proposition 3.18: $f$ convex extensible $\implies$ $\arg\min f[-p]$ hole free for every $p$ (and conversely, when $\operatorname{dom}_{\mathbb Z} f$ is bounded). Proposition 3.19: $f$ is integrally convex if and only if every restriction $f_{[a,b]}$ to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of $f$ one at a time.

Significance

The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension $n$, not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M$^\natural$-convex, L-convex, and L$^\natural$-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.

Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on $\mathbb R^n$, and an LP-duality-based alternate formula for $\tilde f$) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.

Difficulty

The natural first attempt is to try to prove the "$\Leftarrow$" direction of Theorem 3.21 by a direct induction on the $\ell^1$-distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces $x$ to be a local minimizer of the local convex extension $\tilde f$ restricted to the unit ball around $x$, then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on $\mathbb R^n$) to conclude $x$ globally minimizes $\bar f$, and finally uses integral convexity ($\tilde f = \bar f$) to transfer this back to $f$ on $\mathbb Z^n$. The identification of $f$'s local behavior with $\tilde f$'s convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.

Formalization scope

The ground set is $\mathbb Z^n$, represented as Fin n → ℤ; $f$'s codomain is WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$), while the convex closure $\bar f$ and local convex extension $\tilde f$ take values in EReal (exactly $\mathbb R \cup \{\pm\infty\}$, a complete lattice, so their defining suprema are total functions with no side conditions). A trivializing formalization of the goal would quantify the right-hand side over a single fixed $(Y,Z)$ pair, or over all of $\mathbb Z^n$ instead of the sign-pattern neighbors; both are excluded by keeping $Y, Z$ universally quantified Finset (Fin n) ranging over the full $3^n$ sign-pattern space (minus the trivial case, which the equivalence still holds through vacuously).

Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary convex-function local-to-global optimality, LP duality): these are broadly available in Mathlib's convex-analysis library in some form, but none of them is imported here, since none appears in the statement of any item this mission drafts — they belong to a proof this pass does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex functions and will need the same convex-closure/local-extension vocabulary.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Favati, F. Tardella, "Convexity in nonlinear integer programming," Ricerca Operativa, 53, 1990, pp. 3–44.

Motivation

Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.

Setting

Let $V$ be a finite ground set (identified with $\{1,\dots,n\}$ in the book) and let $L = (\ell_{ij})_{i,j\in V}$ be a symmetric real matrix. $L$ has off-diagonal nonpositivity if $\ell_{ij}\le 0$ for all $i\ne j$, and diagonal dominance if $\sum_{j} \ell_{ij}\ge 0$ for every row $i$. The associated quadratic form is $g(p) = \tfrac12 p^\top L p$ for $p \in \mathbb R^V$. For $p,q\in\mathbb R^V$ write $p\vee q$, $p\wedge q$ for the componentwise maximum and minimum. A function $g:\mathbb R^V\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$ for all $p,q$, and has translation submodularity if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf 1)\vee q)+g(p\wedge(q+\alpha\mathbf 1))$ holds for every $\alpha \ge 0$, where $\mathbf 1$ is the all-ones vector (ordinary submodularity is the case $\alpha=0$).

On the conjugate side, for $x\in\mathbb R^V$ write $\operatorname{supp}^+(x)=\{i : x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$, and let $\chi_i$ denote the $i$-th unit vector ($\chi_0$ denotes the zero vector). A function $f:\mathbb R^V\to\mathbb R$ has the exchange property if for all $x,y\in\mathbb R^V$ and $i\in\operatorname{supp}^+(x-y)$ there exist $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ such that $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for every $\alpha\in[0,\alpha_0]$. The Legendre-Fenchel conjugate of $f$ is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$; two functions $g,f$ are conjugate to each other when $g=f^\bullet$ and $f=g^\bullet$. For positive-definite symmetric $M,L$, the quadratic forms $f(x)=\tfrac12x^\top Mx$ and $g(p)=\tfrac12p^\top Lp$ are conjugate to each other exactly when $M$ and $L$ are matrix inverses of one another.

Formalization targets

Goal (Theorem 2.11). For conjugate strictly convex quadratic forms $g$ and $f$ as above,

$$g \text{ has translation submodularity} \iff f \text{ has the exchange property.}$$

This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.

Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of $g$); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of $g$); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric $M$, among membership in the matrix class $\mathcal L^{-1}$, two sign-consistency inequalities on the columns of $M$ together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class $\mathcal L^{-1}$ is closed under taking principal submatrices).

Significance

The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.

Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.

Difficulty

The naive approach to Theorem 2.11 tries to derive the exchange property for $f$ directly from the defining supremum in the conjugate relation $f = g^\bullet$, differentiating under the sup; this fails because the exchange property compares $f$ along a specific combinatorial direction $\chi_i - \chi_j$ tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair $(i,j)$ without already knowing the sign pattern of $M = L^{-1}$. The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on $M$ itself (conditions (b)/(c)) via the identity $f'(x;d) = x^\top Md$, and closes the loop back to membership in $\mathcal L^{-1}$ using the Farkas lemma applied to the linear system $ML = I$ — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.

Formalization scope

Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V]) rather than a fixed Fin n, matching this project's convention elsewhere and letting Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be finite in general even though it is finite here. Every min(0, \dots)-based condition in Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop machinery — a faithful, checked-equivalent simplification, not a narrowing (see MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs instantiation anywhere in this mission. The formalization does not trivialize: the goal's exchange property is stated for the specific combinatorial direction $\chi_i - \chi_j$ with $i\in \operatorname{supp}^+(x-y)$, $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ — not an arbitrary direction, which would reduce the exchange property to a restatement of ordinary convexity and discard the entire combinatorial content the mission is about.

Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib); everything else (submodularity, translation submodularity, the exchange axioms, the sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13) as lemmas; contributions completing any of the seven milestones independently, or supplying the Schur-complement induction behind Proposition 2.4, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994.
• M. Fukushima, Y. Oshima, M. Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994.
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27.

Motivation

Monotone variational inequalities cover convex minimisation, convex–concave saddle-point problems, Nash equilibria of monotone games and complementarity problems, and they are the standard model for these in optimization and operations research. First-order methods for them (extragradient, forward–backward–forward, reflected and projected gradient methods) need a stepsize below $1/L$, where $L$ is a global Lipschitz constant of the operator. That constant is often unknown, too pessimistic, or nonexistent: in composite minimisation with a locally smooth term, or in saddle-point problems with bilinear-plus-nonlinear couplings, the operator is only locally Lipschitz. The usual remedy is a linesearch, which costs extra operator or prox evaluations per iteration and complicates the complexity accounting.

Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities (preprint 2018, Optimization Online 6598; published in Mathematical Programming, 2020, doi:10.1007/s10107-019-01416-w) proposes the Explicit Golden Ratio Algorithm (EGRAAL): its stepsizes are computed in closed form from the last two iterates, it uses one evaluation of $F$ and one proximal step per iteration, and it needs neither a Lipschitz constant nor a linesearch. This mission formalizes its main convergence theorem, Theorem 2 of the preprint.

Setting

Let $\mathcal E$ be a finite-dimensional real inner product space with norm $\|\cdot\|=\sqrt{\langle\cdot,\cdot\rangle}$. Let $g:\mathcal E\to(-\infty,+\infty]$ with domain $\operatorname{dom} g=\{x: g(x)<+\infty\}$, and $F:\operatorname{dom} g\to\mathcal E$. The variational inequality (1) asks for

$$z^*\in\mathcal E\quad\text{with}\quad \langle F(z^*),z-z^*\rangle+g(z)-g(z^*)\ge0\quad\forall z\in\mathcal E. \tag{1}$$

Its solution set is $S$. The standing assumptions are: (C1) $S\ne\emptyset$; (C2) $g$ is proper, convex and lower semicontinuous; (C3) $F$ is monotone on $\operatorname{dom} g$, $\langle F(u)-F(v),u-v\rangle\ge0$ for $u,v\in\operatorname{dom}g$.

The proximal operator is $\operatorname{prox}_g(w)=\operatorname{argmin}_x\{g(x)+\tfrac12\|x-w\|^2\}$. Write $\varphi=\frac{\sqrt5+1}{2}$ for the golden ratio. Algorithm 1 (EGRAAL) takes $z^0,z^1\in\mathcal E$, $\lambda_0>0$, a parameter $\phi\in(1,\varphi]$ and a cap $\bar\lambda>0$, sets $\bar z^0=z^1$, $\theta_0=1$, $\rho=\frac1\phi+\frac1{\phi^2}$, and for $k\ge1$ computes

$$\lambda_k=\min\Big\{\rho\lambda_{k-1},\ \frac{\phi\theta_{k-1}}{4\lambda_{k-1}}\frac{\|z^k-z^{k-1}\|^2}{\|F(z^k)-F(z^{k-1})\|^2},\ \bar\lambda\Big\},\qquad \bar z^k=\frac{(\phi-1)z^k+\bar z^{k-1}}{\phi},$$ $$z^{k+1}=\operatorname{prox}_{\lambda_k g}\big(\bar z^k-\lambda_kF(z^k)\big),\qquad \theta_k=\frac{\lambda_k}{\lambda_{k-1}}\phi,$$

with the convention $0/0=+\infty$ in the middle term. The paper uses the bifunction $\Psi(u,v)=\langle F(u),v-u\rangle+g(v)-g(u)$.

Formalization targets

Goal: Theorem 2

If $F$ is locally Lipschitz continuous and (C1)–(C3) hold, then for every run of Algorithm 1 there is $z^*\in S$ with

$$z^k\to z^*\qquad\text{and}\qquad \bar z^k\to z^*.$$

Nothing is fixed beyond the paper's parameter ranges: $\phi\in(1,\varphi]$, $\bar\lambda>0$, $\lambda_0>0$ and the starting points are arbitrary. The two sequences share one limit.

Milestones

1. Eq. (4), the prox-inequality: $\bar x=\operatorname{prox}_g w\iff\langle\bar x-w,x-\bar x\rangle\ge g(\bar x)-g(x)$ for all $x$.
2. Eq. (18), the estimates the step rule gives: $\lambda_k\le\rho\lambda_{k-1}$, $\theta_k\le1+\frac1\phi$, and $\lambda_k^2\|F(z^k)-F(z^{k-1})\|^2\le\frac{\theta_k\theta_{k-1}}4\|z^k-z^{k-1}\|^2$.
3. Eq. (24), an identity that follows from the averaging step: $\|z^{k+1}-z\|^2=\frac\phi{\phi-1}\|\bar z^{k+1}-z\|^2-\frac1{\phi-1}\|\bar z^k-z\|^2+\frac1\phi\|z^{k+1}-\bar z^k\|^2$.
4. Eq. (27), the energy inequality, for $z\in\operatorname{dom}g$ and $k\ge2$.
5. Lemma 2: along bounded runs, $(\lambda_k)$ and $(\theta_k)$ are bounded and bounded away from $0$.
6. Lemma 1 (Bauschke–Combettes, Theorem 5.5): a Fejér monotone sequence whose cluster points lie in a nonempty set $C$ converges to a point of $C$.

Significance

The result. Theorem 2 shows that a monotone variational inequality with a locally Lipschitz operator can be solved by a method whose stepsizes adapt to the local curvature of $F$ at no extra cost: one $F$ evaluation and one prox step per iteration, and no global constant and no backtracking. Because $F$ is only ever evaluated at the prox outputs $z^k\in\operatorname{dom}g$, the method also applies when $F$ is undefined or badly behaved outside the feasible set, where reflected-gradient methods can fail. The same analysis gives an ergodic $O(1/k)$ rate and, under an error bound, an $R$-linear rate (§2.2 of the preprint; not part of this mission). The paper also derives fixed-point algorithms for demi-contractive operators from it.

Formalizing it. The theorem has a published proof; to our knowledge no machine-checked version exists, and Mathlib has no proximal operator, no theory of monotone variational inequalities and no Fejér-monotonicity lemma. This mission produces a formal convergence proof for an adaptive first-order method with a nonsmooth convex term, together with reusable pieces: the prox-inequality for extended-real-valued convex functions, a finite-dimensional Fejér convergence lemma, and a formal model of an adaptive-step algorithm with the $0/0=+\infty$ rule.

Difficulty

The usual convergence argument for projected or extragradient methods bounds the cross term $\langle F(z^k)-F(z^{k-1}),z^k-z^{k+1}\rangle$ using a global Lipschitz constant and a fixed stepsize. Here neither exists. The stepsize at iteration $k$ depends on the iterates, and the energy that decreases changes from step to step, since it involves $\theta_{k-1}$. Local Lipschitz continuity gives a usable constant only once the iterates are known to be bounded, and boundedness has to come from the energy inequality. Stepsizes that tend to $0$ would also break the argument (Lemma 2 excludes this for bounded runs). The last step, identifying cluster points as solutions, needs lower semicontinuity of $g$ and a limit in the prox-inequality along a subsequence with convergent stepsizes.

Formalization scope

$\mathcal E$ is a real InnerProductSpace with FiniteDimensional ℝ E. $g$ is a map E → EReal; (C2) is a structure: $g$ never takes the value $\bot$, is finite somewhere, has a convex epigraph in $E\times\mathbb R$, and is LowerSemicontinuous on $E$. $F$ is a total map E → E, and every hypothesis on it (monotonicity, Lipschitz bounds) is restricted to $\operatorname{dom}g$. The variational inequality is stored as $g(z^*)\le\langle F(z^*),z-z^*\rangle+g(z)$, with $z^*\in\operatorname{dom}g$, which avoids extended-real subtraction. $\operatorname{prox}_{\lambda g}$ is an argmin predicate, so it never produces a junk value. The algorithm is a predicate on the four sequences, written for index $k+1$. The rule $0/0=+\infty$ is a case split: if $F(z^k)=F(z^{k-1})$ the step is $\min\{\rho\lambda_{k-1},\bar\lambda\}$. No condition such as $F(z^1)\ne F(z^0)$ or $\lambda_0\le\bar\lambda$ is imposed.

"Locally Lipschitz" is formalized as Lipschitz on every bounded subset of $\operatorname{dom}g$. This is the property the proof of Lemma 2 uses. It agrees with local Lipschitz continuity when $\operatorname{dom}g$ is closed (for example $g=\delta_C$ for a closed convex $C$, or $g$ finite everywhere) and is stronger otherwise. Eq. (27) is stated for $z\in\operatorname{dom}g$, where $F(z)$ and $\Psi(z,z^k)$ are defined. Lemma 1 carries the hypothesis $C\ne\emptyset$ of its cited source, without which it is false.

The statements are not vacuous: $g\equiv0$, $F\equiv0$ satisfy (C1)–(C3) and the Lipschitz hypothesis, and admit a run of Algorithm 1 with $\lambda_k=\min\{\rho\lambda_{k-1},\bar\lambda\}$. A proof of Theorem 2 must hold for every run with the paper's parameters, not only for such degenerate data.

Contributions welcome: the prox-inequality and the existence of the prox for proper convex lsc $g$ (both reusable beyond this mission), the Fejér lemma, the algebraic estimates (18) and (24), and the energy inequality (27). Once these are in place, Lemma 2 and the cluster-point argument complete Theorem 2.

Selected references

• Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint, Optimization Online 6598, 2018. https://optimization-online.org/wp-content/uploads/2018/05/6598.pdf ; published in Mathematical Programming 184 (2020), 383–410. https://doi.org/10.1007/s10107-019-01416-w
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (Theorem 5.5). https://doi.org/10.1007/978-1-4419-9467-7
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976), 747–756.
• Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM Journal on Optimization 25 (2015), 502–520. https://doi.org/10.1137/14097238X

Motivation

Newton's method converges quadratically near a non-degenerate minimizer, but classical theory says little about its behaviour far from one: the pure Newton step can move uphill, diverge, or be undefined when the Hessian is singular. For decades the global analysis of Newton-type methods consisted of convergence statements without rates. Nesterov and Polyak (Math. Program. 108, 2006) replaced the quadratic model of Newton's method by a cubic-regularized model and proved, for the first time, global worst-case complexity bounds for a second-order method on several problem classes, including classes of non-convex functions.

This mission covers one of these results: on star-convex functions, the method reduces the optimality gap at the rate $O(1/k^2)$ (Theorem 4 of the paper). Star-convexity is a weakening of convexity that only asks for convexity along segments towards the global minimizers. It includes non-convex functions such as $f(x)=|x|(1-e^{-|x|})$ on $\mathbb R$, and, as the paper notes, it arises in sum-of-squares problems such as $f(x,y)=x^2y^2+x^2+y^2$.

Timeline.

• 1981: Griewank studies Newton's method modified by bounding cubic terms (Cambridge DAMTP technical report NA/12), without complexity bounds.
• 2006: Nesterov and Polyak introduce method (3.3) and prove global rates: $O(k^{-2/3})$ for a second-order stationarity measure on general functions with Lipschitz Hessian, $O(1/k^2)$ on star-convex functions, and linear-then-superlinear rates on gradient-dominated functions.
• 2008: Nesterov accelerates the method on convex functions to $O(1/k^3)$ (Math. Program. 112).
• 2011: Cartis, Gould and Toint develop adaptive cubic regularization (ARC), with inexact subproblem solves and adaptive regularization parameters (Math. Program. 127).
• 2020: Hinder, Sidford and Sohoni give near-optimal first-order methods for star-convex and quasar-convex functions (arXiv:1906.11985).

Setting

Let $F\subseteq\mathbb R^n$ be a closed convex set with nonempty interior, and let $f:\mathbb R^n\to\mathbb R$ be twice differentiable on $F$, with gradient $f'(x)$ and Hessian $f''(x)$. A starting point $x_0\in\operatorname{int}F$ is fixed, and $F$ is assumed large enough to contain the level set $\{x: f(x)\le f(x_0)\}$ in its interior. Assumption 1 is that the Hessian is Lipschitz continuous on $F$ with constant $L>0$:

$$\|f''(x)-f''(y)\|\le L\|x-y\|\qquad\text{for all }x,y\in F,$$

where the matrix norm is the spectral norm.

For a parameter $M>0$ and a point $x$, the cubic model is

$$m_{M,x}(y)=\langle f'(x),y-x\rangle+\tfrac12\langle f''(x)(y-x),y-x\rangle+\tfrac M6\|y-x\|^3 .$$

The cubic step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb R^n$ (Eq. (2.4)), and $\bar f_M(x)=f(x)+\min_y m_{M,x}(y)$ is the model value.

Method (3.3) takes parameters $0<L_0\le L$. At iteration $k\ge0$ it finds $M_k\in[L_0,2L]$ such that $f(T_{M_k}(x_k))\le\bar f_{M_k}(x_k)$, and sets $x_{k+1}=T_{M_k}(x_k)$. The choice $M_k\equiv L$ always passes the test.

A function $f$ is star-convex (Definition 1) if its set $X^*$ of global minimizers is nonempty and, for every $x^*\in X^*$, every $x\in F$ and every $\alpha\in[0,1]$,

$$f(\alpha x^*+(1-\alpha)x)\le\alpha f(x^*)+(1-\alpha)f(x).$$

Write $f^*=f(x^*)$ for the optimal value, and $D=\operatorname{diam}F$ when $F$ is bounded.

Formalization targets

Goal: Theorem 4, item 2, inequality (4.2)

Assume $f$ is star-convex, $F$ is bounded with $\operatorname{diam}F=D$, and $f(x_0)-f^*\le\tfrac32LD^3$. Then every run of method (3.3) satisfies

$$f(x_k)-f(x^*)\le\frac{3LD^3}{2\left(1+\tfrac13k\right)^2},\qquad k\ge0 .$$

The constants are those printed on p. 189. The bound depends on the problem only through $L$ and $D$; the lower parameter $L_0$ and the choice of $M_k$ within $[L_0,2L]$ are free.

Milestones

1. Lemma 1, (2.3): the cubic Taylor bound $|f(y)-f(x)-\langle f'(x),y-x\rangle-\tfrac12\langle f''(x)(y-x),y-x\rangle|\le\tfrac L6\|y-x\|^3$ for $x,y\in F$.
2. Lemma 4, (2.10): $\bar f_M(x)\le\min_{y\in F}\big[f(y)+\tfrac{L+M}{6}\|y-x\|^3\big]$ for $x\in F$.
3. Monotonicity of (3.3) (Section 3, p. 184): $f(x_{k+1})\le f(x_k)$.
4. Theorem 4, item 1: if $f(x_0)-f^*\ge\tfrac32LD^3$, then $f(x_1)-f^*\le\tfrac12LD^3$.

Significance

The result. Theorem 4 gives a global function-value rate for a second-order method on a class that contains non-convex functions, with no assumption on the Hessian at the minimizer. The method needs no knowledge of the class: the same iteration (3.3) that yields second-order stationarity rates on general functions yields $O(1/k^2)$ on star-convex ones. This adaptivity is the paper's main message for Section 4. The analysis also serves as the template for Theorems 5, 8 and 9 of the paper (star-convex with a non-degenerate minimum, and the convex case).

Formalizing it. The theorem has been proved in the paper, and to our knowledge it has not been machine-checked. A complete formalization produces:

• a reusable Lean statement of the cubic-regularized Newton step and of method (3.3);
• the Taylor estimates under a Lipschitz Hessian in $\mathbb R^n$;
• a verified $O(1/k^2)$ recursion argument.

These are the pieces needed for the paper's other rates and for later variants (accelerated and adaptive cubic regularization).

Difficulty

The argument has three parts, and each needs some care.

The first is the Taylor bound (2.3) on a convex set $F$, under a Hessian that is Lipschitz only on $F$. The Hessian is given as the derivative of a gradient map, not as a smooth function on all of $\mathbb R^n$.

The second is keeping the iterates inside $F$. Lemma 4 and the diameter bound $\|x^*-x_k\|\le D$ apply only to points of $F$. So the iterates must be shown to stay in the level set, and the points $\alpha x^*+(1-\alpha)x_k$ used in the estimate must also lie in $F$.

The third is the passage from the one-step inequality to the explicit constant in (4.2). The one-step inequality is a minimum over $\alpha\in[0,1]$ of a cubic in $\alpha$. It has two regimes (the unconstrained minimizer $\alpha_k$ lies inside $[0,1]$ or beyond it), and the recursion for $\alpha_k$ must be carried through without losing the constant $3LD^3/2$ or the factor $\tfrac13$. A generic "sublinear recursion" lemma gives the rate only up to a constant, which is not the printed theorem.

Formalization scope

• Space and derivatives. The space is EuclideanSpace ℝ (Fin n) with $n$ arbitrary. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every $x\in F$. These are two-sided derivatives, also at boundary points of $F$; the iterates lie in $\operatorname{int}F$. The Hessian norm is the operator norm.
• The cubic step. $T_M(x)$ is any global minimizer of the cubic model (IsCubicStep). Every statement about it holds for every such minimizer.
• The model value. $\bar f_M(x)$ is written as $f(x)+m_{M,x}(T)$ at the chosen minimizer $T$.
• The run. A run of (3.3) is the predicate IsCubicNewtonRun, with a 0-based index.
• Star-convexity. IsStarConvexFn quantifies $x$ over $F$, as in display (4.1). It requires $X^*\neq\emptyset$ and the inequality for every global minimizer.
• The diameter. $D$ is Metric.diam F, with Bornology.IsBounded F as a hypothesis. It is the diameter of $F$ itself, not of the level set.
• The optimal value. $f^*$ is $f(x^*)$ for a global minimizer $x^*$, not an arbitrary lower bound.

Ruling out trivial formalizations. Without the boundedness hypothesis, Metric.diam F is $0$, and the goal would assert $f(x_k)=f^*$ outright. The formalization keeps boundedness, the nonemptiness of $X^*$ and the global-minimizer reading of $T_M(x)$, so that the hypotheses describe the paper's class and not a degenerate one. The hypotheses are satisfiable: for example, $f(y)=\tfrac12\|y\|^2$ on $\mathbb R^1$ with $F$ the closed unit ball, $x_0=0$ and $M_k\equiv L=1$.

Contributions are welcome at every level: proofs of the milestones, and general-purpose lemmas on Taylor bounds with a Lipschitz Hessian on convex sets. Those lemmas are reusable for missions I, III and IV of this series, which formalize the paper's other rates.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• Yu. Nesterov, Accelerating the cubic regularization of Newton's method on convex problems, Mathematical Programming Ser. B 112 (2008) 159–181. https://doi.org/10.1007/s10107-006-0089-x
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
• O. Hinder, A. Sidford and N. Sohoni, Near-optimal methods for minimizing star-convex functions and beyond, COLT 2020. https://arxiv.org/abs/1906.11985

Motivation

A variational inequality asks for a point $x$ of a set $K\subseteq\mathbb R^n$ at which a vector field $f$ points "into" $K$: $(x'-x)^T f(x)\ge 0$ for every $x'\in K$. It is the common form of the first-order optimality conditions of constrained optimization, of complementarity problems, and of equilibrium models in economics and traffic networks. In many of these models the feasible set itself depends on the decision: the admissible actions of one agent are restricted by the current state, as in the impulse-control problems of Bensoussan and Lions that motivated quasi-variational inequalities, where $K=K(x)$.

D. Chan and J. S. Pang, The generalized quasi-variational inequality problem (Math. Oper. Res. 7 (1982) 211–222), unify the quasi-variational inequality with the generalized (set-valued) variational inequality of Fang and Peterson (JOTA 1982). Their §§3–4 prove existence by fixed-point theorems for set-valued maps; §5 takes a different route and characterizes solutions as fixed points of a composite projection map. Theorem 5.3, the subject of this mission, gives conditions under which that map is a contraction, so that its fixed point exists, is unique, solves the problem, and is computed by plain fixed-point iteration from any starting point. It is the algorithmic result of the paper, and an early instance of the projection methods for strongly monotone quasi-variational inequalities studied since (e.g. Nesterov and Scrimali 2011).

Setting

Throughout, $\mathbb R^n$ carries the Euclidean inner product $x^T y$ and norm $\|x\|$.

Given point-to-set mappings $K$ and $f$ of $\mathbb R^n$ into itself, the generalized quasi-variational inequality problem $\mathrm{GQVI}(K,f)$ is to find vectors $x$ and $y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^T y\ge 0\quad\text{for all }x'\in K(x).$$

When $f$ is point-to-point, $f(x)$ is read as the singleton $\{f(x)\}$.

For a set $S$ and a point $z$, the projection $P_S(z)$ is the point of $S$ nearest to $z$, $P_S(z)=\operatorname{sol}\min_{x\in S}\|x-z\|$; it exists and is unique when $S$ is nonempty, closed and convex.

Theorem 5.3 concerns the special structure in which the feasible set moves by translation: fix a nonempty closed convex set $\tilde K$ and a point-to-point mapping $m$, and put

$$K(x)=m(x)+\tilde K=\{m(x)+k : k\in\tilde K\}.$$

For a step length $\lambda>0$ and a point-to-point $f$, the projection map is

$$F_\lambda(x)=P_{K(x)}\bigl(x-\lambda f(x)\bigr).$$

The mappings $m$ and $f$ are assumed Lipschitz continuous with constants $\alpha$, $\beta$ ($\|m(x)-m(y)\|\le\alpha\|x-y\|$, $\|f(x)-f(y)\|\le\beta\|x-y\|$) and strongly monotone with constants $\gamma$, $\delta$ ($(x-y)^T(m(x)-m(y))\ge\gamma\|x-y\|^2$, $(x-y)^T(f(x)-f(y))\ge\delta\|x-y\|^2$).

Formalization targets

Goal: Theorem 5.3 (p. 221)

For each $\lambda>0$ with

$$\lambda^2\beta^2+2\lambda(\alpha\beta-\delta)-2(\gamma-\alpha)<0,$$

the map $F_\lambda$ is a contraction (Lipschitz with a constant $c<1$ independent of the points), it has a fixed point $\tilde x_\lambda$, the point $\tilde x_\lambda$ solves $\mathrm{GQVI}(K,f)$, and the iterates $x^{k+1}=F_\lambda(x^k)$ converge to $\tilde x_\lambda$ from every initial vector $x^0\in\mathbb R^n$. All four conclusions are stated together.

Milestones

1. Projection onto a translate (§5, proof of Theorem 5.3, first display, p. 221): $P_{K(x)}(y)=m(x)+P_{\tilde K}(y-m(x))$ for all $x,y$.
2. Lipschitz estimate (§5, proof of Theorem 5.3, last display, p. 221): for every $\lambda>0$,

$$\|F_\lambda(y^1)-F_\lambda(y^2)\|\le\Bigl[\alpha+\bigl(\lambda^2\beta^2+2\lambda(\alpha\beta-\delta)+(1+\alpha^2-2\gamma)\bigr)^{1/2}\Bigr]\|y^1-y^2\|.$$

3. Theorem 5.1 (p. 220): if every $K(x)$ is closed and convex, $(x^*,y^*)$ solves $\mathrm{GQVI}(K,f)$ if and only if $x^*=P_{K(x^*)}(x^*-y^*)$ and $y^*\in f(x^*)$.

Significance

The result. Theorem 5.3 turns an existence question into a computation: under Lipschitz and strong monotonicity assumptions, a quasi-variational inequality with translated feasible sets has exactly one solution reachable by projection iterations, each of which is a projection on the fixed set $\tilde K$ (a convex quadratic program when $\tilde K$ is polyhedral). The step-size window it gives is explicit in $\alpha,\beta,\gamma,\delta$, so it certifies a convergent method before any iteration is run. The closing remark of the paper (p. 222) reads each step as solving the GQVI under a zero-th order approximation of $K$, the viewpoint behind later splitting methods.

Formalizing it. The result is proved in the paper; the proof is short, but its constants and the equivalence of the two contraction conditions are easy to get wrong. A machine-checked version fixes the exact hypotheses (no sign conditions on the constants, Euclidean geometry), and produces reusable pieces: the translation identity for projections, nonexpansiveness of the Euclidean projection on a closed convex set, and the projection characterization of quasi-variational inequalities (Theorem 5.1).

Difficulty

Banach's fixed-point theorem does the last step; the work is the estimate. The naive bound, projection nonexpansiveness applied directly to $F_\lambda$, fails because the sets $K(y^1)$ and $K(y^2)$ differ: two projections on different sets are not controlled by the distance of the projected points alone. The translation identity separates the moving part $m(y^1)-m(y^2)$ from a projection on the one set $\tilde K$, at the cost of the additive term $\alpha$ in the constant. The remaining square must be expanded with the inner-product cross terms bounded by the monotonicity constants in the right directions, including the cross term between $f$ and $m$. Finally, the condition "bracket $<1$" is equivalent to the stated $\lambda$-condition only when $\alpha<1$, which must be derived from the hypotheses rather than assumed.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n), with Mathlib's Euclidean norm and inner product; Fin n → ℝ (sup norm) would change every constant. No assumption $n\ge1$ is made; at $n=0$ all statements hold trivially.
• The constants $\alpha,\beta,\gamma,\delta$ are real numbers with no sign conditions, as in the paper; the Lipschitz and monotonicity hypotheses are the displayed inequalities for all $x,y$. For $n\ge1$ they force $\alpha,\beta\ge0$, $\gamma\le\alpha$, $\delta\le\beta$, and the $\lambda$-condition then forces $\alpha<1$ and $\delta>\alpha\beta$.
• $K(x)$ is the translate $\{m(x)+k : k\in\tilde K\}$ of a fixed set $\tilde K$, assumed nonempty, closed and convex. The projection is a nearest-point function proj that returns a junk value only when no nearest point exists; under the hypotheses of every statement using it, the nearest point exists and is unique, so proj is the paper's $P$. Theorem 5.1 is stated relationally (nearest-point predicate IsProj) to avoid junk values altogether.
• "Contraction" is Mathlib's ContractingWith c F with c : ℝ≥0: c < 1 and a Lipschitz bound with that single constant. A constant allowed to depend on the points, or a Lipschitz bound without c < 1, is not a contraction and would trivialize the goal; so would a projection whose junk value is reachable (e.g. with $\tilde K$ empty), which makes $F_\lambda$ unrelated to the paper's map. The fixed point must be linked to the GQVI and to the iteration from every starting point.
• The square root in the Lipschitz estimate is Real.sqrt; its radicand is nonnegative under the hypotheses when $n\ge1$.
• Useful infrastructure: Mathlib's ContractingWith.fixedPoint and ContractingWith.tendsto_iterate_fixedPoint (Banach), exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero (projection on convex sets), and the platform theorem VectorSpaceOpt.min_distance_convex_set. A general lemma that the Euclidean nearest-point map of a closed convex set is 1-Lipschitz is reusable well beyond this mission and is welcome as a separate contribution.

Selected references

• D. Chan and J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. C. Fang and E. L. Peterson, Generalized variational inequalities, Journal of Optimization Theory and Applications 38 (1982) 363–383. https://doi.org/10.1007/BF00935344
• Y. Nesterov and L. Scrimali, Solving strongly monotone variational and quasi-variational inequalities, Discrete and Continuous Dynamical Systems 31(4) (2011) 1383–1396. https://doi.org/10.3934/dcds.2011.31.1383

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