Convex Optimization

Motivation

Training a statistical model by empirical risk minimization means minimizing an average of $N$ losses over a parameter vector $w\in\mathbb R^n$, where both $N$ and $n$ can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.

Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every $L$ steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the $O(1/k)$ expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).

Setting

Let $f_1,\dots,f_N:\mathbb R^n\to\mathbb R$ be twice continuously differentiable losses and

$$F(w)=\frac1N\sum_{i=1}^N f_i(w).$$

For a sample $\mathcal S\subseteq\{1,\dots,N\}$ of size $b$, the minibatch gradient is $\nabla F_{\mathcal S}(w)=\frac1b\sum_{i\in\mathcal S}\nabla f_i(w)$. For a sample $\mathcal S_H$ of size $b_H$, the subsampled Hessian is $\nabla^2F_{\mathcal S_H}(w)=\frac1{b_H}\sum_{i\in\mathcal S_H}\nabla^2 f_i(w)$.

Assumption 1 requires constants $0<\lambda,\Lambda$ with $\lambda I\prec\nabla^2F_{\mathcal S_H}(w)\prec\Lambda I$ for every $w$ and every Hessian sample. It also requires a bound $\gamma^2$ on the second moment of the stochastic gradient. $w^*$ denotes the minimizer of $F$.

Algorithm 2 turns correction pairs $(s_j,y_j)$ into a matrix $H_t$. With $\tilde m=\min\{t,M\}$, it starts from $\frac{s_t^Ty_t}{y_t^Ty_t}I$ and applies the BFGS update

$$H\leftarrow(I-\rho_js_jy_j^T)H(I-\rho_jy_js_j^T)+\rho_js_js_j^T,\qquad\rho_j=\frac1{y_j^Ts_j},$$

for $j=t-\tilde m+1,\dots,t$.

Algorithm 1 (SQN) runs for $k=1,2,\dots$. It draws a gradient sample $\mathcal S_k$ and steps

$$w^{k+1}=w^k-\alpha^kH\nabla F_{\mathcal S_k}(w^k),$$

where $H=I$ for $k\le2L$ and $H=H_t$, $t=\lfloor(k-1)/L\rfloor-1$, afterwards. Every $L$ iterations it forms the block average $\bar w_t$ of the last $L$ iterates and a new pair

$$s_t=\bar w_t-\bar w_{t-1},\qquad y_t=\nabla^2F_{\mathcal S_{H,t}}(\bar w_t)\,s_t .$$

Samples are drawn independently and uniformly among the subsets of their size. The step length is $\alpha^k=\beta/k$.

Formalization targets

Goal: Corollary 3.3, with a corrected constant

There are $0<\mu_1\le\mu_2$, depending only on the problem data, such that every matrix Algorithm 1 applies satisfies $\mu_1I\prec H\prec\mu_2I$. Moreover, for every $\beta>1/(2\mu_1\lambda)$,

$$E[F(w^k)-F(w^*)]\le\frac{Q_c(\beta)}k\qquad(k\ge1),$$ $$Q_c(\beta)=\max\Big\{\frac{\Lambda\mu_2^2\beta^2\gamma^2}{2(2\mu_1\lambda\beta-1)},\ \Lambda\mu_2^2\beta^2\gamma^2,\ F(w^1)-F(w^*)\Big\}.$$

The constants $\mu_1,\mu_2$ are not fixed numerically. The goal asserts a rate of order $1/k$ with an explicit constant in terms of them.

Milestones

• (3.8)–(3.10): the curvature bounds $\lambda\|s\|^2\le y^Ts\le\Lambda\|s\|^2$ and $\lambda\le\|y\|^2/y^Ts\le\Lambda$ for Hessian-product pairs.
• (3.11) and (3.12): the trace bound and Powell's determinant formula for the direct L-BFGS matrices.
• Lemma 3.1: $\mu_1I\prec H_t\prec\mu_2I$ uniformly along every run.
• (3.18): expected descent for the general Newton-like iteration $w^{k+1}=w^k-\alpha^kH_k\nabla f(w^k,\xi^k)$.
• (3.19): $2\lambda[F(w)-F(w^*)]\le\|\nabla F(w)\|^2$.
• (3.22): the recursion $\phi_{k+1}\le(1-2\alpha^k\mu_1\lambda)\phi_k+\frac\Lambda2(\alpha^k\mu_2)^2\gamma^2$.
• Theorem 3.2: the $Q_c(\beta)/k$ rate for the Newton-like iteration.

Significance

The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the $\beta/k$ schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.

The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner $H_t$ depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which $H_t$ is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.

On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of $H_t$ that is uniform over all runs and all $t$. The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and $A\prec B$ is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices $k,t$ start at $1$ as in the paper. In the corollary, $E$ is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. $H_k$ and $w^k$ are $\mathcal F_k$-measurable, the sample $\xi^k$ is $\mathcal F_{k+1}$-measurable, and unbiasedness is a conditional expectation. Integrability of $F(w^k)$ is part of each conclusion, so a junk-zero integral cannot satisfy it.

Two corrections to the paper, each labelled in the item titles and notes:

• Iterate-wise $\gamma$. Assumption 1(3) says $E_\xi\|\nabla f(w,\xi)\|^2\le\gamma^2$ for all $w$. Together with unbiasedness and $\lambda$-strong convexity on $\mathbb R^n$, this forces $\lambda\|w-w^*\|\le\|\nabla F(w)\|\le\gamma$ for every $w$, which is impossible. The mission imposes the bound at the iterates, conditionally on the past, which is how the proof uses it.
• Constant $Q_c(\beta)$. The induction after (3.22) multiplies by $1-2\beta\mu_1\lambda/k$, which is negative for $k<2\beta\mu_1\lambda$. Counterexample: $n=1$, $f_{1,2}(w)=(w\mp1)^2/2$, $H_k=I$, $w^1=0$, $\beta=2$, $\gamma^2=5$. Then $F(w^2)-F(w^*)=2>Q(2)/2=5/3$, and the example survives perturbing the constants so that every strict inequality holds. The middle entry of $Q_c$ repairs it, and $Q_c=Q$ whenever $2\mu_1\lambda\beta\le3/2$.

Smaller conventions:

• The pairs must satisfy $s_t\neq0$, since Algorithm 2 is undefined otherwise.
• Hessian samples have size $b_H\ge1$; the empty sample makes (2.3) a $0/0$.
• The corollary's undefined $\mu_2$ is Lemma 3.1's constant, enlarged together with $\mu_1$ to cover the initial $H=I$ steps.
• The block average of Algorithm 1 is used, not Eq. (2.1).

Trivializing encodings are ruled out: $H_t$ is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all $w$.

Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of $C^2$ functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.

Selected references

• R. H. Byrd, S. L. Hansen, J. Nocedal, Y. Singer, A Stochastic Quasi-Newton Method for Large-Scale Optimization, SIAM J. Optim. 26(2):1008–1031, 2016. https://doi.org/10.1137/140954362
• A. Mokhtari, A. Ribeiro, Global Convergence of Online Limited Memory BFGS, J. Mach. Learn. Res. 16:3151–3181, 2015. https://jmlr.org/papers/v16/mokhtari15a.html
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2):223–311, 2018. https://doi.org/10.1137/16M1080173
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277
• M. J. D. Powell, Some global convergence properties of a variable metric algorithm for minimization without exact line searches, in Nonlinear Programming, SIAM-AMS Proc. IX, 1976, pp. 53–72.

Motivation

A competitive equilibrium is a list of production plans, consumption plans and prices at which every firm maximizes profit, every consumer maximizes utility within the budget, and no market has excess demand. Whether such prices exist at all is the consistency question behind general equilibrium theory, the welfare theorems, and applied equilibrium models used in policy analysis. Arrow and Debreu gave the first proof of existence for a model with production, private ownership and general convex preferences (Econometrica 22, 1954), using Debreu's existence theorem for abstract economies (PNAS 38, 1952).

Their Theorem I assumes that every consumer initially holds a positive amount of every commodity (Assumption IV.a). The authors call this "clearly unrealistic" (p. 280): a household does not hold every good, and most households own little beyond their labor. Theorem II, the subject of this mission, removes that assumption. It only asks that every consumer be able to supply some type of labor that is always productive of a commodity everyone desires. This is the version of the existence theorem that allows a wage-earner economy.

Timeline. Wald (1935–36) proved existence for special production models. Nash (1950) proved existence of equilibrium points for finite games, and Debreu (1952) extended it to abstract economies, in which each player's feasible set depends on the others' choices. Arrow and Debreu (1954) proved Theorems I and II. McKenzie's independent existence proof was published the same year (Econometrica 22, 1954).

Setting

There are $l$ commodities, $n$ producers and $m$ consumers; vectors live in $\mathbb R^l$ and $x\leqq y$ is componentwise. Producer $j$ has a production set $Y_j$. Consumer $i$ has a consumption set $X_i$, a utility $u_i$ on $X_i$, an endowment $\zeta_i$ and profit shares $\alpha_{ij}$. Write $Y=\sum_jY_j$, $X=\sum_iX_i$, $\zeta=\sum_i\zeta_i$, and let $P=\{p\geqq0,\ \sum_hp_h=1\}$ be the price simplex. A competitive equilibrium $(x_1^*,\dots,x_m^*,y_1^*,\dots,y_n^*,p^*)$ satisfies four conditions. Each $y_j^*$ maximizes $p^*\cdot y_j$ on $Y_j$. Each $x_i^*$ maximizes $u_i$ on $\{x_i\in X_i: p^*\cdot x_i\le p^*\cdot\zeta_i+\sum_j\alpha_{ij}p^*\cdot y_j^*\}$. The price vector satisfies $p^*\in P$. Finally $z^*=\sum x_i^*-\sum y_j^*-\zeta\leqq0$ and $p^*\cdot z^*=0$.

The assumptions of Theorem II are as follows. I: production sets are closed, convex and contain $0$; $Y\cap\Omega=\{0\}$ (no output without input); $Y\cap(-Y)=\{0\}$ (no reversible production). II: each $X_i$ is closed, convex and bounded below. III: $u_i$ is continuous, has no satiation point, and satisfies $u_i(tx+(1-t)x')>u_i(x')$ whenever $u_i(x)>u_i(x')$ and $0<t<1$. IV.b: shares are nonnegative and sum to one for each firm. Two sets of commodities are defined from the data. The set $\mathcal D$ contains the commodities always desired by every consumer: from any $x_i\in X_i$, adding some positive amount of the commodity stays in $X_i$ and raises $u_i$. The set $\mathcal P$ contains the types of productive labor: for every $y\in Y$, (a) $y_h\le0$, and (b) some $y'\in Y$ satisfies $y'_{h'}\ge y_{h'}$ for all $h'\ne h$ and $y'_{h''}>y_{h''}$ for some $h''\in\mathcal D$. The remaining assumptions are:

• IV′.a: each consumer has some $x_i\in X_i$ with $x_i\leqq\zeta_i$ and $x_{hi}<\zeta_{hi}$ for some $h\in\mathcal P$;
• V: some $x\in X$ and $y\in Y$ satisfy $x_h<y_h+\zeta_h$ for every $h$;
• VI: $\mathcal D\ne\emptyset$;
• VII: $\mathcal P\ne\emptyset$.

Formalization targets

Goal: Theorem II (§4.5, p. 281)

$$\text{Assumptions I–III, IV}',\ \text{V–VII}\ \Longrightarrow\ \exists\,(x^*,y^*,p^*)\ \text{satisfying Conditions 1–4.}$$

Milestones (§5, pp. 282–287)

They follow the paper's proof. Let $\pi=|\mathcal P|$ and $P^\varepsilon=\{p\in P: p_h\ge\varepsilon\ \forall h\in\mathcal P\}$ for $0<\varepsilon\le1/(2\pi)$. Let $E^\varepsilon$ be the abstract economy in which consumers maximize utility under budget constraints, producers maximize profit, and a market participant chooses $p\in P^\varepsilon$ to maximize $p\cdot z$. The milestones are:

1. §5.0 (1). On $P^\varepsilon$ every consumer can spend strictly less than $p\cdot\zeta_i$.
2. §5.1.1 (5). Equilibrium points of $E^\varepsilon$ satisfy $x^*-y^*\leqq\zeta'$ for a vector $\zeta'$ independent of $\varepsilon$.
3. §5.2.0. The attainable sets relative to $\zeta'$ are bounded.
4. §5.2.1. The truncated economy $\tilde E^\varepsilon$ has an equilibrium point.
5. §5.2.2 (3)–(5). An equilibrium point of $\tilde E^\varepsilon$ is one of $E^\varepsilon$.
6. §5.3.0 (2). If $p^*_h>\varepsilon$ for all $h\in\mathcal P$, the point is a competitive equilibrium.
7. §5.3.2 (1). Limits of equilibrium points as $\varepsilon\to0$ are quasi-equilibria for consumers.
8. §5.3.4 (3). If the floors bind, some desired commodity has limit price $0$.
9. §5.3.4 (6). If the floors bind, limit consumption minimizes expenditure over $X_i$.
10. §5.3.5. For some $\varepsilon$ the floor does not bind.

Significance

Theorem II is the existence theorem for a competitive economy in which consumers may own nothing but their labor. It shows that the survival assumption IV.a can be traded for conditions on labor, desirability and the possibility of an overall excess supply. Section 5.3.3 of the paper also isolates the quasi-equilibrium, in which utility maximization under the budget is replaced by cost minimization at a given utility level. That notion is used in later existence and welfare arguments.

The theorem has been proved since 1954; this mission does not reopen it. The work here is the machine-checked proof. The companion mission on Theorem I formalizes the shared model and Debreu's lemma. As of September 2026 neither theorem has a Lean formalization on the platform, and Mathlib contains no general equilibrium theory.

Difficulty

The obvious approach reuses the proof of Theorem I: build the abstract economy of consumers, producers and a price-choosing participant, and apply Debreu's lemma. That fails at the boundary of the price simplex. Without IV.a, a consumer's cheapest point in $X_i$ can cost as much as the endowment at some prices, so the budget correspondence is not continuous there and the lemma does not apply. The paper therefore keeps prices of productive labor at least $\varepsilon$ and must then show that the floor does not bind for some $\varepsilon$. That is a limit argument as $\varepsilon\to0$ which uses Assumptions V, VI and VII together, and each of the milestones 7–9 is a step of it. Debreu's lemma itself needs a Kakutani-type fixed point theorem for correspondences, which Mathlib does not provide.

Formalization scope

Commodity vectors are Fin l → ℝ. Consumers are indexed by Fin m and producers by Fin n. The inner product is ⬝ᵥ. The paper's $x<y$ is strict in every component and is written componentwise, never as Lean's < on functions. $\mathcal D$ and $\mathcal P$ are computed from the economy, not supplied as parameters. Utilities are total functions, but every assumption on $u_i$ quantifies over $X_i$ only. "Maximizes" is membership plus an inequality against every feasible alternative; no supremum is used. $E$, $E^\varepsilon$ and $\tilde E^\varepsilon$ are built by one constructor over the players Fin m ⊕ Fin n ⊕ Unit. The vector $\zeta'$ takes the lower bounds $\xi_i$ of Assumption II as an explicit argument. The milestones of §5.3 are stated for the limit of a sequence of equilibrium points, which is how the paper constructs them. Assumption V is dropped from every milestone except §5.3.5 and the goal. With V, the case assumption of §5.3.1 is contradictory and those milestones would hold vacuously.

A trivializing formalization is ruled out as follows. The assumptions are satisfiable with IV.a failing: a sorry-free check covers two goods, one consumer who owns nothing and can only supply labor, and one firm turning labor into the desired good. The goal therefore does not hold vacuously.

Needed infrastructure includes a Kakutani fixed point theorem or Debreu's lemma, compactness of truncated action sets, and sequential compactness arguments in $\mathbb R^l$. AGT.brouwer_fixed_point is on the platform and can serve as a starting point. The lemma is reusable well beyond this mission. Contributions to any milestone, to the lemma, or to the boundedness results shared with Theorem I are welcome.

Selected references

• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 265–290, 1954. https://doi.org/10.2307/1907353
• G. Debreu, A Social Equilibrium Existence Theorem, Proceedings of the National Academy of Sciences 38(10), 886–893, 1952. https://doi.org/10.1073/pnas.38.10.886
• L. W. McKenzie, On Equilibrium in Graham's Model of World Trade and Other Competitive Systems, Econometrica 22(2), 147–161, 1954. https://doi.org/10.2307/1907352
• J. F. Nash, Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1), 48–49, 1950. https://doi.org/10.1073/pnas.36.1.48

Motivation

Many first-order methods in optimization are fixed-point iterations $x^{k+1}=f(x^k)$ of a nonexpansive map $f:\mathbb R^n\to\mathbb R^n$: proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration $x^{k+1}=(1-\alpha)x^k+\alpha f(x^k)$ converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.

Timeline (as recounted in the paper's related-work section):

• 1965. Anderson introduces the method for nonlinear integral equations (J. ACM 12).
• 1978. Gay and Schnabel prove local Q-superlinear convergence of a full-memory AA-I-type method (Broyden with projected updates), assuming $f$ continuously differentiable near the solution.
• 2009. Fang and Saad connect AA with multisecant Broyden methods and distinguish the two types (Numer. Linear Algebra Appl. 16).
• 2011. Walker and Ni show the essential equivalence of full-memory AA with GMRES for affine $f$ (SIAM J. Numer. Anal. 49); Rohwedder and Schneider prove local Q-linear convergence of limited-memory AA-II for differentiable $f$.
• 2015. Toth and Kelley give local linear convergence of AA-II for contractive $f$ (SIAM J. Numer. Anal. 53).
• 2020. Zhang, O'Donoghue and Boyd introduce a stabilized AA-I method (Powell-type regularization, restart checking, safeguarding) and prove global convergence for every nonexpansive map with a fixed point, without differentiability (SIAM J. Optim. 30(4), 3170–3197; longer version arXiv:1808.03971).

Setting

Let $f:\mathbb R^n\to\mathbb R^n$ satisfy $\|f(x)-f(y)\|_2\le\|x-y\|_2$ for all $x,y$ (the Euclidean norm), and assume the solution set $X=\{x^\star\mid x^\star=f(x^\star)\}$ is nonempty. The residual is $g(x)=x-f(x)$, $g_k=g(x^k)$, and the averaged operator is $f_\alpha(x)=(1-\alpha)x+\alpha f(x)$.

Powell's weight. For $\bar\theta\in(0,1)$, $\phi_{\bar\theta}(\eta)=1$ if $|\eta|\ge\bar\theta$ and $\phi_{\bar\theta}(\eta)=(1-\operatorname{sign}(\eta)\bar\theta)/(1-\eta)$ otherwise, with $\operatorname{sign}(0)=1$.

Window matrices. For vectors $s_0,\dots,s_{m_k-1}$ and $y_0,\dots,y_{m_k-1}$, let $\hat s_i$ be their unnormalized Gram–Schmidt orthogonalization (3.2), $B^0=I$, and

$$B^{i+1}=B^i+\frac{(\tilde y_i-B^is_i)\hat s_i^T}{\hat s_i^Ts_i},\qquad \tilde y_i=\theta^iy_i+(1-\theta^i)B^is_i,\qquad \theta^i=\phi_{\bar\theta}\Bigl(\frac{\hat s_i^T(B^i)^{-1}y_i}{\|\hat s_i\|_2^2}\Bigr).$$

The matrix norm $\|\cdot\|_2$ is the induced $\ell_2$ operator norm.

Algorithm 3.1 (AA-I-S-m). With parameters $\bar\theta,\tau,\alpha\in(0,1)$, $D,\epsilon>0$ and max-memory $m\ge1$: start from $H_0=I$, $m_0=0$, $n_{AA}=0$, $\bar U=\|g_0\|_2$ and $x^1=\tilde x^1=f_\alpha(x^0)$. At iteration $k\ge1$, set $s_{k-1}=\tilde x^k-x^{k-1}$ and $y_{k-1}=g(\tilde x^k)-g(x^{k-1})$, orthogonalize $s_{k-1}$ against the current window, and restart the window (memory back to $1$, $H_{k-1}$ replaced by $I$) if the memory would exceed $m$ or $\|\hat s_{k-1}\|_2<\tau\|s_{k-1}\|_2$. Then apply one Powell-regularized rank-one update to obtain $H_k$ and the trial point $\tilde x^{k+1}=x^k-H_kg_k$. The trial point is accepted if $\|g_k\|_2\le D\bar U(n_{AA}+1)^{-(1+\epsilon)}$ (and $n_{AA}$ increases); otherwise $x^{k+1}=f_\alpha(x^k)$.

Formalization targets

Goal: Theorem 4.1

$$\text{for every run of Algorithm 3.1:}\qquad \lim_{k\to\infty}x^k=x^\star\quad\text{for some } x^\star=f(x^\star).$$

The only hypotheses are nonexpansiveness of $f$, $X\ne\emptyset$ and the parameter ranges. The limit is not specified: it depends on $x^0$ and the parameters.

Milestones

1. Lemma 3.2. Well-defined updates give $|\det B^{m_k}|\ge\bar\theta^{m_k}>0$.
2. Lemma 3.3. If $\|y_i\|_2\le2\|s_i\|_2$, $\|\hat s_i\|_2\ge\tau\|s_i\|_2$ and $m_k\le m$, then $\|B^{m_k}\|_2\le3((1+\bar\theta+\tau)/\tau)^m-2$.
3. Corollary 3.4. $\|H_k\|_2\le(3((1+\bar\theta+\tau)/\tau)^m-2)^{n-1}/\bar\theta^m$ (3.8).
4. Corollary 3.5. Along the algorithm, unless a solution is hit, (3.8) holds and $\mathrm{cond}(H_k)\le(3((1+\bar\theta+\tau)/\tau)^m-2)^n/\bar\theta^m$.
5. Eq. (4.3). $\|x^k-y\|_2\le\|x^0-y\|_2+CD\bar U\sum_{i\ge0}(i+1)^{-(1+\epsilon)}$ for every $y\in X$.
6. Eq. (4.6). $\lim_k\|g_k\|_2=0$.
7. Eq. (4.7). $\|x^{k+1}-y\|_2^2\le\|x^k-y\|_2^2+\epsilon_k$ with $\epsilon_k\ge0$ summable.
8. §4.1, Step 2. $\|x^k-y\|_2$ converges for every $y\in X$.

Significance

The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.

The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).

Difficulty

The accelerated step $\tilde x^{k+1}=x^k-H_kg_k$ need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding $\|H_kg_k\|_2$, requires a bound on $\|H_k\|_2$ that holds uniformly along the run; without the Powell regularization $B_k$ can be singular, and without the restart rule $\|B_k\|_2$ can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; $u\hat s^T$ is rankOne ℝ u ŝ; $\det$ is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by $f$, the parameters and $x^0$, and a sorry-free check that runs exist (for $f=\mathrm{id}$) was built locally. The reset of $H_{k-1}$ in line 8 is local to its iteration. $\mathrm{sign}(0)=1$ is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.

Line 9. The paper prints $\tilde y_{k-1}=\theta_{k-1}y_{k-1}-(1-\theta_{k-1})g_{k-1}$, derived from (3.3) through $B_{k-1}s_{k-1}=-g_{k-1}$, which fails when the window starts afresh ($m_k=1$). The mission uses (3.3) there: $\tilde y_{k-1}=\theta_{k-1}y_{k-1}+(1-\theta_{k-1})s_{k-1}$ when $m_k=1$, and the printed formula when $m_k\ge2$.

Milestones of §4.1 and Corollary 3.5 carry the hypothesis $f(x^k)\ne x^k$ for all $k$, as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on $\|H_k\|_2$, contractivity of $f$, or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.

Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality $\|f_\alpha(x)-y\|_2^2\le\|x-y\|_2^2-\alpha(1-\alpha)\|g(x)\|_2^2$, quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's $H_k^{-1}$) and of the convergence steps are all welcome.

Selected references

• J. Zhang, B. O'Donoghue, S. Boyd, Globally Convergent Type-I Anderson Acceleration for Nonsmooth Fixed-Point Iterations, SIAM J. Optim. 30(4), 3170–3197, 2020. https://doi.org/10.1137/18M1232772
• J. Zhang, B. O'Donoghue, S. Boyd, longer version, 2018. https://arxiv.org/abs/1808.03971
• D. M. Gay, R. B. Schnabel, Solving systems of nonlinear equations by Broyden's method with projected updates, in Nonlinear Programming 3, Academic Press, 245–281, 1978 (reference [20] of the paper). https://doi.org/10.1137/18M1232772
• D. G. Anderson, Iterative procedures for nonlinear integral equations, J. ACM 12(4), 547–560, 1965. https://doi.org/10.1145/321296.321305
• H. Fang, Y. Saad, Two classes of multisecant methods for nonlinear acceleration, Numer. Linear Algebra Appl. 16(3), 197–221, 2009. https://doi.org/10.1002/nla.617
• H. F. Walker, P. Ni, Anderson acceleration for fixed-point iterations, SIAM J. Numer. Anal. 49(4), 1715–1735, 2011. https://doi.org/10.1137/10078356X
• A. Toth, C. T. Kelley, Convergence analysis for Anderson acceleration, SIAM J. Numer. Anal. 53(2), 805–819, 2015. https://doi.org/10.1137/130919398
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7

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