Optimization

Motivation

Training a model in machine learning means minimizing an expected loss over a data distribution, using a finite sample from it. Two families of methods dominate. Stochastic gradient methods step along the gradient of the loss at one data point: each step is cheap, but the noise forces small steps and many sequential iterations. Batch methods average the gradient over a large set of points: each step is accurate and parallelizes well, but costs a pass over the data. Bottou and Bousquet (The tradeoffs of large scale learning, NIPS 2007) compared the two by the total work needed to reach accuracy $\epsilon$ and concluded that stochastic gradient descent is preferable in large-scale learning.

Byrd, Chin, Nocedal and Wu (Sample size selection in optimization methods for machine learning, Math. Program. 2012) analyse a third option: a dynamic batch method, which takes gradient steps on mini-batches whose size grows over the run. A small batch makes early progress cheap; a large batch later makes the steps accurate. Their Theorem 4.2 shows that when the batch size grows geometrically, steepest descent with a fixed step converges linearly in expectation, and their Corollary 4.3 derives from it a total work bound of the same order as stochastic gradient descent. The analysis underlies a line of work on adaptive sampling and variance-controlled batch methods (for example Friedlander and Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 2012; Bottou, Curtis and Nocedal, Optimization methods for large-scale machine learning, SIAM Review 2018, §5.2).

Setting

Let $(Z,P)$ be a probability space of data points $z$; in the paper $z=(x,y)$ is an input–output pair with distribution $P(x,y)$. The parameter is $w\in\mathbb R^m$ ($m$ is the number of variables). A per-sample loss $\ell(w;z)$ is given with gradient $\nabla\ell(w;z)$ in $w$, and the objective is the expected loss (2.1)

$$J(w)=\int\ell(w;z)\,dP(z).$$

The gradient of the objective is the expected per-sample gradient, $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$.

Uniform convexity (4.2): $J$ is twice continuously differentiable and there are constants $0<\lambda<L$ with

$$\lambda\|d\|_2^2\le d^T\nabla^2J(w)\,d\le L\|d\|_2^2\qquad\text{for all } w,d .$$

Then $J$ has a unique minimizer $w^*$.

For a random vector $X\in\mathbb R^m$, $\|\mathrm{Var}(X)\|_1=\mathbb E\|X-\mathbb EX\|_2^2$ is the sum of its componentwise variances. The variance bound (4.22) asks for a constant $\omega$ with

$$\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1\le\omega\qquad\text{for all } w .$$

The algorithm. Fix sample sizes $n_k\ge1$ and a starting point $w_0$. At iteration $k$ draw a batch $S_k$ of $n_k$ points, independently with law $P$ and independently of earlier batches, form the batch gradient (4.19)

$$g_k=\frac1{n_k}\sum_{i\in S_k}\nabla\ell(w_k;i),$$

and take the dynamic batch steepest descent step (4.24)

$$w_{k+1}=w_k-\frac1L\,g_k .$$

The iterates $w_k$ are random, and expectations below are over all batches.

Formalization targets

Goal: Theorem 4.2

If $n_k\ge a^k$ for all $k$, for some $a>1$, and (4.22) holds, then

$$\mathbb E[J(w_k)-J(w^*)]\le C\rho^k\quad\text{for all }k,\qquad \rho=\max\{1-\lambda/(4L),\,1/a\}<1,\quad C=\max\{J(w_0)-J(w^*),\,2\omega/\lambda\}.$$

The constants are the paper's. The goal also asserts that $J(w_k)$ is integrable for every $k$.

Milestones, in the order the proof uses them

1. (4.5), p. 8: $\nabla J(w)^T\nabla J(w)\ge\lambda[J(w)-J(w^*)]$ for every $w$.
2. Taylor bound, p. 11: $J(w-\frac1Lg)\le J(w)-\frac1L\nabla J(w)^Tg+\frac1{2L}\|g\|^2$ for every $w$ and $g$.
3. (4.25), p. 11: at a fixed point $w$, with $g$ the batch gradient of $n$ i.i.d. draws,

$$\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1L\|\nabla J(w)\|^2+\tfrac1{2L}\mathbb E\|g\|^2,\qquad \mathbb E\|g\|^2=\|\nabla J(w)\|^2+\|\mathrm{Var}(g)\|_1 .$$

4. Variance of the batch gradient, p. 12: $\|\mathrm{Var}(g)\|_1\le\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1/n$.
5. (4.26), p. 12: $\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1{2L}\|\nabla J(w)\|^2+\tfrac1{2Ln}\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1$.
6. (4.27), p. 12: $\mathbb E[J(w-\tfrac1Lg)-J(w^*)]\le(1-\tfrac{\lambda}{2L})(J(w)-J(w^*))+\tfrac{\omega}{2Ln}$.

Milestones 3–6 are the paper's conditional expectations given $w_k$, stated at a fixed point $w$ with the batch drawn afresh.

Significance

Theorem 4.2 is the convergence guarantee of the dynamic sampling strategy: it says that the noise of a mini-batch gradient does not destroy the linear rate of steepest descent, provided the batch grows geometrically. The rate $\rho$ makes the trade-off explicit: the optimization contracts by $1-\lambda/(4L)$ per step, the noise by $1/a$, and the slower of the two governs. From it the paper's Corollary 4.3 bounds the total number of sample-gradient evaluations to reach $\mathbb E[J(w_k)-J(w^*)]\le\epsilon$ by $O(L/(\lambda\epsilon))$, which places dynamic batch methods on the same footing as stochastic gradient descent in the Bottou–Bousquet comparison, while keeping the parallelism of batch methods.

The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization produces a reusable account of the one-iteration analysis of a mini-batch gradient step (descent lemma, variance of an i.i.d. sample mean of random vectors, conditional expectation over a fresh batch), and of the passage from a conditional one-step recursion to an unconditional bound over a run driven by an infinite i.i.d. array. Corollary 4.3 is not part of this mission: it involves $O(\cdot)$ bounds, a cost model for gradient evaluations and an iteration count treated as a real number.

Difficulty

The arithmetic of the induction on p. 12 is short. The difficulty is in making the probability rigorous. The iterate $w_k$ is random, and the paper's one-step bound (4.27) is a conditional expectation given $w_k$, with $J(w_k)$ on the right-hand side. Turning it into an unconditional recursion requires that the batch of iteration $k$ be independent of $w_k$, that $w_k$ be a measurable function of the earlier batches, and that $J(w_k)$ and $\|g_k\|^2$ be integrable at every step, none of which is automatic for a run driven by an infinite array of draws. A naive formalization that treats $w_k$ as a fixed point, or $g_k$ as an abstract random vector with a postulated variance bound, skips exactly this content.

The variance identity for a sample mean of random vectors in $\mathbb R^m$ and the bound $\|\nabla J(w)\|\le L\|w-w^*\|$ from (4.2) are standard but not packaged in this form in Mathlib.

Formalization scope

• The space is EuclideanSpace ℝ (Fin m). The paper's $\lambda$ is written lam (λ is a Lean keyword). (4.2) is ContDiff ℝ 2 J, 0 < lam < L, and the two-sided bound on fderiv ℝ (fderiv ℝ J) w d d.
• $J$ is defined as the Bochner integral $\int\ell(w;z)\,dP(z)$ for a general per-sample loss $\ell$; the paper's linear predictor $f(w;x)=w^Tx$ and convex loss $l$ are not used by the theorem and are not assumed. The model assumes: $\ell(w;\cdot)$ integrable; $\nabla\ell(w;z)$ the gradient of $\ell(\cdot;z)$ at $w$; $(w,z)\mapsto\nabla\ell(w;z)$ jointly measurable; $\nabla\ell(w;\cdot)$ square-integrable; and $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$ (differentiation under the integral, which the paper uses without proof).
• Sampling with replacement. The paper's (3.5) is sampling without replacement from $N$ points; it takes $N\to\infty$ on p. 5, which "also corresponds to the case of sampling with replacement". The formalization draws every point i.i.d. from $P$: draw $i$ of iteration $k$ is $\xi_{k,i}$ and the law of the whole array is Measure.infinitePi over $\mathbb N\times\mathbb N$. The finite-population factor $(N-n_k)/(N-1)$ is not modelled.
• $w^*$ is a given minimizer of $J$; $n_k$ are natural numbers with $a^k\le n_k$ (real powers of a real $a>1$); $\omega$ is a real number.
• The goal asserts integrability of $J(w_k)$ together with the bound, so the inequality cannot be met by the Bochner integral's value $0$ on a non-integrable function. The batch gradient is the mean over $n_k$ draws at the current iterate, and $w_k$ is the random run: a goal with an abstract random $g_k$ satisfying a postulated variance bound, or with $w_k$ a deterministic sequence, would not be this theorem.
• Welcome contributions: the variance of an i.i.d. mean of $\mathbb R^m$-valued random vectors; the descent lemma and gradient-dominance inequality from Hessian bounds; measurability and independence lemmas for processes driven by Measure.infinitePi. All three are reusable beyond this mission.

Selected references

• R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012) 127–155. https://doi.org/10.1007/s10107-012-0572-5
• L. Bottou, O. Bousquet, The tradeoffs of large scale learning, NIPS 2007. https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning
• M. P. Friedlander, M. Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 34 (2012) A1380–A1405. https://doi.org/10.1137/110830629
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization methods for large-scale machine learning, SIAM Review 60 (2018) 223–311. https://doi.org/10.1137/16M1080173

Motivation

Training a machine-learning model usually means minimizing an expected or empirical loss $J(w)$ over parameters $w \in \mathbb{R}^m$. Exact gradients of such objectives are expensive, because each one requires a pass over the whole data set; practical methods replace $\nabla J(w_k)$ by a cheaper approximation $g_k$, for instance a gradient computed on a subsample. This raises a basic question for the analysis of optimization algorithms: how accurate must the approximate gradient be for steepest descent to keep its linear rate of convergence?

Byrd, Chin, Nocedal and Wu (Math. Program. 2012) answer this question with a relative-error condition, and use the answer to motivate a rule that increases the sample size during the run. Their §4.1 treats the deterministic case: the approximations $g_k$ are arbitrary vectors, and only a geometric condition linking $g_k$ to $\nabla J(w_k)$ is assumed. That deterministic result, Theorem 4.1, is the goal of this mission. The stochastic counterpart (Theorem 4.2, dynamic batch sizes) is a separate mission of the same series.

Relative-error conditions of this kind ("the error is a fixed fraction of the step") appear throughout the literature on inexact gradient and inexact Newton methods (e.g. Bertsekas and Tsitsiklis 2000 on gradient methods with errors), and the condition (4.8) below is the deterministic template for the adaptive sampling tests later developed for stochastic optimization.

Setting

Let $J : \mathbb{R}^m \to \mathbb{R}$ be twice continuously differentiable and uniformly convex: there are constants $0 < \lambda < L$ such that

$$\lambda\|d\|_2^2 \;\le\; d^T \nabla^2 J(w)\, d \;\le\; L\|d\|_2^2 \qquad\text{for all } w, d \in \mathbb{R}^m. \tag{4.2}$$

Such a $J$ has a unique minimizer $w_*$; following the paper, it is normalized so that $J(w_*) = 0$.

Fix $\theta \in (0,1)$. Given a sequence of vectors $g_0, g_1, \ldots$ (the approximate gradients), the fixed-steplength steepest descent iteration is

$$w_{k+1} = w_k - \alpha g_k, \qquad \alpha = \frac{1-\theta}{L}. \tag{4.1, 4.7}$$

The approximate gradient at iteration $k$ satisfies the relative-error condition if

$$\|g_k - \nabla J(w_k)\| \;\le\; \theta\, \|g_k\|. \tag{4.8}$$

Write

$$\beta = \frac{(1-\theta)^2}{2(1+\theta)^2}. \tag{4.9}$$

Formalization targets

Goal: Theorem 4.1 (p. 8)

1. If (4.8) holds at iteration $k$, then

$$J(w_{k+1}) \le \Bigl(1 - \frac{\beta\lambda}{L}\Bigr) J(w_k). \tag{4.9}$$

2. If (4.8) holds at every iteration, then $w_k \to w_*$ (4.10); every $k > \frac{L}{\beta\lambda}[\log(1/\epsilon) + \log J(w_0)]$ satisfies $J(w_k) < J(w_*) + \epsilon$ (4.11); and

$$\|g_k\|^2 \le \frac{1}{(1-\theta)^2}\,\frac{2L^2J(w_0)}{\lambda}\Bigl(1-\frac{\beta\lambda}{L}\Bigr)^k. \tag{4.12}$$

The constants are those of the paper and are kept explicit.

Milestones

In the order the paper's proof uses them:

• (4.5) $\nabla J(w)^T\nabla J(w) \ge \lambda[J(w) - J(w_*)]$ and (4.6) $J(w) - J(w_*) \ge \frac{\lambda}{2L^2}\|\nabla J(w)\|_2^2$, consequences of (4.2) alone (p. 8);
• (4.13) $(1-\theta)\|g_k\| \le \|\nabla J(w_k)\| \le (1+\theta)\|g_k\|$ and (4.14) $\nabla J(w_k)^Tg_k \ge (1-\theta)\|g_k\|^2$ under (4.8) (p. 9);
• (4.16) the one-step decrease $J(w_{k+1}) \le J(w_k) - \frac{\beta}{L}\|\nabla J(w_k)\|^2$ under (4.8) at $k$ (p. 9);
• (4.17) $J(w_k) \le (1 - \beta\lambda/L)^k J(w_0)$ under (4.8) at every earlier iteration (p. 9).

Significance

Theorem 4.1 says that the linear convergence of steepest descent on a uniformly convex function survives arbitrary gradient errors, provided each error is at most a fixed fraction $\theta$ of the approximate gradient's own norm. The price is explicit: the per-step contraction factor is $1 - \beta(\theta)\lambda/L$ instead of a factor of the form $1 - c\lambda/L$ with an absolute constant $c$, and the iteration bound (4.11) grows like $L/(\beta\lambda)$ times a logarithm. Because (4.8) is relative rather than absolute, no a priori bound on the error is needed, and the error may be large far from the solution. In the paper this is the motivation for requiring the sample variance of a subsampled gradient to be small relative to $\|g_k\|^2$, which leads to the dynamic sample-size rule analysed in §4.2.

The result is proved in the paper (pp. 9–10). No machine-checked proof of it, or of any relative-error inexact gradient method with explicit constants, has been published. A formal proof provides a checked reference statement for inexact first-order methods with the paper's constants, and the milestones (4.5), (4.6), (4.13), (4.14) are reusable facts about strongly convex smooth functions and about relative-error gradient approximations.

Difficulty

Each step is classical, but the proof combines second-order information with metric estimates. The descent estimate (4.15) needs a second-order Taylor bound from the upper Hessian bound in (4.2), which in Lean means passing from a bound on the second Fréchet derivative to a quadratic upper bound on $J$ along a segment. The inequalities (4.5) and (4.6) relate the gradient norm to the optimality gap through the lower and upper Hessian bounds and the minimizer, and must be derived without an explicit averaged Hessian unless one is built. The convergence $w_k \to w_*$ in (4.10) requires turning convergence of the function values into convergence of the iterates, which again uses uniform convexity. Finally, (4.11) is a logarithmic iteration count whose boundary cases ($J(w_0) = 0$, $\epsilon \ge J(w_0)$) must be handled. A naive reading of the iteration with exact gradients does not apply: the step is $(1-\theta)/L$, not $1/L$, and the direction $-g_k$ is only known to be a descent direction through (4.14).

Formalization scope

The space is EuclideanSpace ℝ (Fin m). Assumption (4.2) is a definition HessianBounds J lam L (with lam for $\lambda$, a Lean keyword): ContDiff ℝ 2 J, 0 < lam < L, and both bounds on the quadratic form fderiv ℝ (fderiv ℝ J) w d d. The gradient is Mathlib's gradient J. The minimizer is a point wstar with J wstar ≤ J w for all w, and J wstar = 0 is a hypothesis of the goal and of (4.17), exactly as in the paper; (4.5) and (4.6) are stated with $J(w_*)$ and without it. The constant $\beta$ is a definition beta θ; it is never a free variable. The approximate gradients $g_k$ are an arbitrary sequence and nothing is random. The iterates are any sequence with w (k+1) = w k - ((1 - θ) / L) • g k for all k.

The one-step claim (4.9) assumes (4.8) only at the index $k$; (4.10)–(4.12) assume it at every index. (4.11) is stated in the form the proof derives in (4.18): every $k$ strictly beyond the bound has $J(w_k) < \epsilon$. The logarithm is natural; when $J(w_0) = 0$ Lean's convention $\log 0 = 0$ applies, which is harmless because every iterate is then optimal. No positivity hypothesis on $J(w_0)$ is added.

A trivializing formalization is excluded: the step size is fixed by the paper, $\beta$ and the Hessian bounds are pinned, and the hypotheses are satisfiable, e.g. by $J(w) = \tfrac{c}{2}\|w\|^2$ with $\lambda < c < L$, $w_* = 0$ and $g_k = \nabla J(w_k)$.

A complete development needs: a second-order Taylor (or mean-value) bound from a Hessian bound, the strong-convexity inequalities (4.5)–(4.6), and elementary real-analysis facts about geometric sequences and logarithms. The milestones (4.5), (4.6), (4.13) and (4.14) are independent of the iteration and reusable. Proofs of any milestone, and alternative proofs with sharper constants stated as separate theorems, are welcome.

Selected references

• R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012), 127–155. https://doi.org/10.1007/s10107-012-0572-5
• D. P. Bertsekas, J. N. Tsitsiklis, Gradient convergence in gradient methods with errors, SIAM Journal on Optimization 10 (2000), 627–642. https://doi.org/10.1137/S1052623497331063
• L. Bottou, O. Bousquet, The tradeoffs of large scale learning, Advances in Neural Information Processing Systems 20 (2008). https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning

Motivation

Nonlinear semidefinite programming asks to minimize a smooth function subject to smooth equality constraints and a constraint that a smooth matrix-valued function be positive semidefinite. It covers robust control design, structural optimization, and nonconvex matrix problems such as low-rank approximation and nearest-correlation-matrix problems. Algorithms for it (sequential quadratic programming, augmented Lagrangian and semismooth Newton methods) converge fast locally only when the Karush–Kuhn–Tucker (KKT) point they approach is stable under perturbation, and the question is which checkable conditions guarantee that stability.

For classical nonlinear programming the answer has been known since the 1980s: at a local minimizer, Robinson's strong second order sufficient condition together with linear independence of the active gradients is equivalent to strong regularity of the KKT point (Robinson 1980; Jongen et al. 1987; Kojima 1980). D. Sun extended this equivalence to nonlinear semidefinite programs, where the constraint cone is not polyhedral and second-order analysis carries an extra curvature term.

Timeline.

• 1980: S. M. Robinson introduces strong regularity of generalized equations and shows that for nonlinear programs the strong second order sufficient condition plus linear independence of active gradients implies it (Math. Oper. Res. 5).
• 1997–2000: Shapiro, and Bonnans and Shapiro, develop second-order optimality conditions for cone-constrained problems, with the "sigma term" built from second order tangent sets and C²-cone reducibility (Bonnans–Shapiro 2000).
• 2002: Sun and Sun prove that the projector onto the positive semidefinite cone is strongly semismooth and compute its directional derivative.
• 2005–2006: D. Sun proves the equivalence theorem formalized here (preprint of May 15, 2005; journal version Math. Oper. Res. 31(4), 761–776).

Setting

$X$ is a finite-dimensional real inner-product space, $\Re^m$ is Euclidean space, and $\mathcal S^p$ is the space of real symmetric $p\times p$ matrices with the Frobenius inner product $\langle A,B\rangle=\mathrm{Tr}(A^TB)$. $\mathcal S^p_+$ is the cone of positive semidefinite matrices. The problem is

$$\text{(NLSDP)}\qquad \min f(x)\quad\text{s.t.}\quad h(x)=0,\ \ g(x)\in\mathcal S^p_+,$$

with $f:X\to\Re$, $h:X\to\Re^m$, $g:X\to\mathcal S^p$ twice continuously differentiable. Write $G=(h,g)$ and $K=\{0\}\times\mathcal S^p_+$. The Lagrangian is $L(x,\zeta,\Gamma)=f(x)+\langle\zeta,h(x)\rangle+\langle\Gamma,g(x)\rangle$, and the multiplier set $\mathcal M(x)$ consists of the $(\zeta,\Gamma)$ with $J_xL(x,\zeta,\Gamma)=0$, $h(x)=0$ and $\Gamma$ in the normal cone $N_{\mathcal S^p_+}(g(x))$ (so $\Gamma\preceq0$ and $\langle\Gamma,g(x)\rangle=0$). A triple $(\bar x,\bar\zeta,\bar\Gamma)$ with $(\bar\zeta,\bar\Gamma)\in\mathcal M(\bar x)$ is a KKT point.

For a closed set $D$, $T_D(y)=\{d:\exists t_k\downarrow0,\ \mathrm{dist}(y+t_kd,D)=o(t_k)\}$ is the tangent cone and $\mathrm{lin}(T)$ its lineality space. Robinson's constraint qualification at $\bar x$ is $J_xG(\bar x)X+T_K(G(\bar x))=\Re^m\times\mathcal S^p$; constraint nondegeneracy replaces $T_K$ by $\mathrm{lin}(T_K)$. The critical cone is $C(\bar x)=\{d:J_xG(\bar x)d\in T_K(G(\bar x)),\ J_xf(\bar x)d\le0\}$.

For $B\in\mathcal S^p$ with Moore–Penrose pseudo-inverse $B^\dagger$, set $\Upsilon_B(\Gamma,A)=2\langle\Gamma,AB^\dagger A\rangle$. Let $\Pi_{\mathcal S^p_+}$ be the metric projector, $A=g(\bar x)+\Gamma$, and $C(A;\mathcal S^p_+)=T_{\mathcal S^p_+}(A_+)\cap(A_+-A)^\perp$ with $A_+=\Pi_{\mathcal S^p_+}(A)$. Then $\mathrm{app}(\zeta,\Gamma)=\{d:J_xh(\bar x)d=0,\ J_xg(\bar x)d\in\mathrm{aff}\,C(A;\mathcal S^p_+)\}$ and $\widehat C(\bar x)=\bigcap_{(\zeta,\Gamma)\in\mathcal M(\bar x)}\mathrm{app}(\zeta,\Gamma)$. The strong second order sufficient condition (SSOSC) at $\bar x$ is

$$\sup_{(\zeta,\Gamma)\in\mathcal M(\bar x)}\Big\{\langle d,J^2_{xx}L(\bar x,\zeta,\Gamma)d\rangle-\Upsilon_{g(\bar x)}\big(\Gamma,J_xg(\bar x)d\big)\Big\}>0\qquad\forall d\in\widehat C(\bar x)\setminus\{0\}.$$

The KKT map is $F(x,\zeta,\Gamma)=\big(\nabla_xL(x,\zeta,\Gamma),\,-h(x),\,-g(x)+\Pi_{\mathcal S^p_+}(g(x)+\Gamma)\big)$ on $Z=X\times\Re^m\times\mathcal S^p$; its zeros are the KKT points. The KKT system is also the generalized equation $0\in\varphi(z)+N_D(z)$ with $\varphi=(\nabla_xL,-h,-g)$ and $D=X\times\Re^m\times\mathcal S^p_-$. A solution $\bar z$ is strongly regular if, for all small $\delta$, the linearized equation $\delta\in\varphi(\bar z)+J\varphi(\bar z)(z-\bar z)+N_D(z)$ has a unique solution near $\bar z$ that depends Lipschitz-continuously on $\delta$. Clarke's generalized Jacobian $\partial F$ is the convex hull of the B-subdifferential $\partial_BF$, the set of limits of Jacobians at nearby differentiability points. $\Phi(\delta)=F'(\bar z;\delta)$ is the directional derivative. The uniform second order growth condition and strong stability quantify over all $C^2$-smooth parameterizations $(f(x,u),G(x,u))$ of the problem.

Formalization targets

Goal: Theorem 21

At a local minimizer $\bar x$ satisfying Robinson's CQ, with $(\bar\zeta,\bar\Gamma)\in\mathcal M(\bar x)$, the following are equivalent:

$$\begin{aligned} &\text{(a) SSOSC at }\bar x\text{ and constraint nondegeneracy;}\quad \text{(b) every }V\in\partial F(\bar x,\bar\zeta,\bar\Gamma)\text{ is nonsingular;}\\ &\text{(c) }(\bar x,\bar\zeta,\bar\Gamma)\text{ is strongly regular;}\quad \text{(d) uniform second order growth and nondegeneracy;}\\ &\text{(e) strong stability and nondegeneracy;}\quad \text{(f) }F\text{ is a locally Lipschitz homeomorphism near }(\bar x,\bar\zeta,\bar\Gamma);\\ &\text{(h) }\Phi\text{ is a globally Lipschitz homeomorphism;}\quad \text{(j) every }V\in\partial\Phi(0)\text{ is nonsingular.} \end{aligned}$$

Milestones

The matrix analysis of $\Pi_{\mathcal S^p_+}$: Lemma 1 (a B-subdifferential chain rule), Lemma 2, Propositions 3 and 4 (the block structure of $\partial_B\Pi_{\mathcal S^p_+}$ and $\partial\Pi_{\mathcal S^p_+}$), and Proposition 7 (the inequality $\langle\Delta B,\Delta\Gamma\rangle\ge-\Upsilon_B(\Gamma,\Delta B)$). Second-order theory: Proposition 8 (the strict CQ gives a unique multiplier and $\mathrm{aff}\,C(\bar x)=\mathrm{app}$), Theorem 10 (the classical second-order conditions with the sigma term) and Lemma 11 ($\Upsilon$ equals the sigma term on $C(\bar x)$). The equivalences: Remark 15 (strong regularity iff a natural map is a Lipschitz homeomorphism), Proposition 16 ((a) ⇒ (b) ⇒ (c) at any KKT point), Lemma 18 (uniform growth ⇒ SSOSC) and Lemma 20 ($\partial_B\Phi(0)=\partial_BF(\bar z)$).

Significance

The theorem identifies the SSOSC, a condition that can be checked from the problem data, with the stability notions that local algorithms need. Strong regularity is the hypothesis under which Newton-type methods for the KKT system converge locally and solutions vary Lipschitz-continuously with the data. Nonsingularity of $\partial F$ gives quadratic convergence of semismooth Newton methods. Uniform growth and strong stability are what sensitivity analysis uses. Without the theorem, each of these properties has to be verified separately for semidefinite programs. The theorem also shows that the classical nonlinear programming equivalence survives on a non-polyhedral cone if the curvature term $\Upsilon$ is added.

The result is proved in the literature but has no machine-checked proof. Formalizing it requires the B-subdifferential and Clarke Jacobian of the PSD projector, second order tangent sets of $\mathcal S^p_+$, and the Robinson–Kummer characterization of strong regularity. None of these exists in Mathlib. Items (g) and (i), which use the topological degree, are not formalized.

Difficulty

The obvious route is to copy the nonlinear programming proof: write strong regularity as nonsingularity of a reduced Jacobian on the active constraints. This fails because $\mathcal S^p_+$ is not polyhedral. The KKT map is only semismooth, and its generalized Jacobian at a non-strictly complementary point is a whole family of operators, parametrized by $\partial\Pi_{\mathcal S^{|\beta|}_+}(0)$. Nonsingularity has to be shown for every member of that family. The curvature of the cone appears only through $\Upsilon$, which links the second-order condition to the Jacobian family. The converse directions combine several external theorems (Bonnans–Shapiro's stability theory, Clarke's inverse function theorem, Kummer's characterization), each needing nonsmooth infrastructure.

Formalization scope

All objects are defined in SunNLSDP.Equiv.Setting. $\mathcal S^p$ is the subspace of symmetric vectors in EuclideanSpace ℝ (n × n) for a finite index type n, so its inner product is exactly the Frobenius product. $Y$ and $Z$ are WithLp 2 products, carrying the sum of the inner products. $B^\dagger$ is computed by the continuous functional calculus. The metric projector returns its argument when no minimiser exists; it is applied only to nonempty closed convex sets. Clarke's Jacobian, $\partial_B$, the one-sided directional derivative, the normal cone and the lineality space are the published definitions NonsmoothNewton.Shared.clarkeJac, NonsmoothNewton.Local.dirDeriv and RobinsonSR.Reduction.Setting.

Conventions committed to:

• The brace systems (41), (42), (49) are read as one coupled system: every $(a,B)$ equals $(J_xh(\bar x)d,\,J_xg(\bar x)d+T)$ for a single $d$. Read as two independent equations they would be strictly weaker.
• "$\sup>0$" is stated as "some multiplier gives a positive value". The non-strict supremum of Theorem 10 (44) and the support function are taken in the extended reals.
• Local optimality is local minimality of $f$ on the feasible set together with feasibility of $\bar x$.
• "Nonsingular" means bijective.
• Parameter spaces in Definitions 17 and 19 range over Banach spaces in the universe of $X$.
• Lemma 2 and Remark 15 add nonemptiness of $D$.

Items (g) and (i) of Theorem 21 are omitted, because Brouwer degree is unavailable; no surrogate for the index is substituted. A formalization that reads the CQs or nondegeneracy as two decoupled equations, or states SSOSC only on $C(\bar x)$ instead of $\widehat C(\bar x)$, proves a different theorem and is ruled out.

Reusable infrastructure: the PSD projector and its generalized Jacobians, second order tangent sets, the Moore–Penrose pseudo-inverse of symmetric matrices, and the characterization of strong regularity by Lipschitz homeomorphisms. Proofs of individual milestones are welcome, as are lemmas on $\Pi_{\mathcal S^p_+}$ and on strong regularity of generalized equations.

Selected references

• D. Sun, The strong second order sufficient condition and constraint nondegeneracy in nonlinear semidefinite programming and their implications, preprint dated May 15, 2005; Mathematics of Operations Research 31(4), 761–776, 2006. https://doi.org/10.1287/moor.1060.0195
• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• J. F. Bonnans and A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• D. Sun and J. Sun, Semismooth matrix-valued functions, Mathematics of Operations Research 27(1), 150–169, 2002. https://doi.org/10.1287/moor.27.1.150.342
• B. Kummer, Lipschitzian inverse functions, directional derivatives, and applications in C^{1,1} optimization, Journal of Optimization Theory and Applications 70, 559–580, 1991. https://doi.org/10.1007/BF00941302

Motivation

Augmented Lagrangian methods are among the standard ways to solve smooth nonlinear programs. They replace a constrained problem by a sequence of subproblems in which some constraints are moved into the objective through a penalty term and multiplier estimates. The method of Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18(4), 2007) is the theory behind the ALGENCAN solver. It moves only the "upper-level" constraints into the objective, keeps arbitrary "lower-level" constraints in the subproblems, and requires the subproblems to be solved only approximately.

A convergence theory for such a method has to say what the limit points of the iterates are. This mission is about the second half of that theory (Theorem 4.2): a limit point that is feasible is a KKT point of the original problem, provided it satisfies a weak constraint qualification, the constant positive linear dependence condition (CPLD) of Qi and Wei (SIAM J. Optim. 10(4), 2000). Earlier global convergence results for augmented Lagrangian methods, such as Conn, Gould and Toint's, assumed linear independence of the active gradients (LICQ) at all limit points. CPLD is implied by MFCQ and by LICQ, holds automatically for linear constraints, and is required only at feasible points.

Timeline of the relevant notions:

• 1967: Mangasarian and Fromovitz introduce MFCQ.
• 2000: Qi and Wei introduce CPLD for SQP methods.
• 2005: Andreani, Martínez and Schuverdt show that CPLD is a genuine constraint qualification.
• 2007: this paper proves Theorem 4.2 for augmented Lagrangian methods with general lower-level constraints.

Setting

The problem (2.1) is

$$\text{minimize } f(x)\quad\text{subject to}\quad h_1(x)=0,\ g_1(x)\le 0,\ h_2(x)=0,\ g_2(x)\le 0,$$

with $f:\mathbb R^n\to\mathbb R$ and constraint maps $h_1,g_1,h_2,g_2$ into $\mathbb R^{m_1},\mathbb R^{p_1},\mathbb R^{m_2},\mathbb R^{p_2}$, all continuously differentiable. $\Omega_1=\{h_1=0,\ g_1\le 0\}$ and $\Omega_2=\{h_2=0,\ g_2\le 0\}$.

The augmented Lagrangian with respect to $\Omega_1$ (2.2) is

$$L(x,\lambda,\mu,\rho)=f(x)+\frac{\rho}{2}\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}{\rho}\Big)^2+\frac{\rho}{2}\sum_{i=1}^{p_1}\Big(\Big[[g_1(x)]_i+\frac{\mu_i}{\rho}\Big]_+\Big)^2 .$$

Algorithm 3.1 works in outer iterations $k=1,2,\dots$ with a penalty parameter $\rho_k$ and safeguarded multipliers $\bar\lambda_k$, $\bar\mu_k$ that stay in fixed boxes. At iteration $k$ it finds $x_k$ and lower-level multipliers $v_k$, $u_k\ge 0$ that satisfy the KKT conditions of "minimize $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ on $\Omega_2$" up to a tolerance $\varepsilon_k\to 0$. It then computes the first-order estimates $\lambda_{k+1}=\bar\lambda_k+\rho_k h_1(x_k)$ and $\mu_{k+1}=\max\{0,\bar\mu_k+\rho_k g_1(x_k)\}$. Finally it increases $\rho_k$ by a factor $\gamma>1$ unless a feasibility-complementarity measure has decreased by the factor $\tau<1$.

A point $x$ satisfies CPLD if, whenever some gradients of constraints active at $x$ have a nontrivial vanishing linear combination with nonnegative coefficients on the inequalities, those gradients remain linearly dependent at every point of a neighbourhood of $x$.

Formalization targets

Goal: Theorem 4.2

If $x_*\in\Omega_1\cap\Omega_2$ is a limit point of $\{x_k\}$ and satisfies CPLD with respect to all constraints of (2.1), then $x_*$ is a KKT point of (2.1). If moreover $x_*$ satisfies MFCQ and $\{x_k\}_{k\in K}\to x_*$, then

$$\{\|\lambda_{k+1}\|,\ \|\mu_{k+1}\|,\ \|v_k\|,\ \|u_k\|\}_{k\in K}\ \text{is bounded.}\tag{4.8}$$

Milestones

1. (4.9). At every outer iteration, the gradient of the Lagrangian of (2.1) at $x_k$ with multipliers $(\lambda_{k+1},\mu_{k+1},v_k,u_k)$ has norm at most $\varepsilon_k$.
2. (4.10). Along a subsequence converging to $x_*$, the multipliers of inequality constraints that are inactive at $x_*$ eventually vanish.
3. (4.11)–(4.15). For a general $C^1$ program: if $y_k\to x_*$, $x_*$ is feasible and satisfies CPLD, and the residuals $\nabla F(y_k)+\sum a_{k,i}\nabla H_i(y_k)+\sum b_{k,j}\nabla G_j(y_k)$ tend to zero with $b_k\ge 0$ supported on the constraints active at $x_*$, then $x_*$ is a KKT point.
4. (4.8) under MFCQ. In the same setting with MFCQ instead of CPLD, the coefficients $a_k$, $b_k$ are bounded.

Significance

The theorem says that the algorithm has the right limit points: a feasible limit point is stationary under a constraint qualification weaker than MFCQ and LICQ, with no assumption on the penalty parameters. Milestone 3 is a result of independent interest: an "approximate KKT" sequence converges to a KKT point under CPLD. This sequential argument was later developed into the theory of approximate KKT conditions (Andreani, Haeser & Martínez 2011), and it applies to any algorithm that produces approximate KKT points, not only to this one. Milestone 4 gives the classical fact that MFCQ bounds the multipliers of such sequences.

All results are proved in the paper. As far as is known, none has a machine-checked proof. Neither CPLD nor the augmented Lagrangian method of this paper is formalized in Mathlib or on the platform. The companion missions of this series formalize Theorem 4.1 (feasibility of limit points) and Theorem 5.4 (boundedness of the penalty parameters).

Difficulty

The obvious argument divides the approximate KKT relation by the size of the multipliers, passes to the limit and obtains a contradiction with the constraint qualification. Under CPLD this argument fails, because CPLD does not bound the multipliers: they may diverge along the sequence even though the limit is a KKT point, and the limit of the normalized relation need not contradict anything at $x_*$ itself. CPLD speaks about linear dependence on a whole neighbourhood of $x_*$, while the relation holds only at the iterates, so the information has to be transferred from $x_*$ to nearby points. A pointwise version of CPLD (dependence at $x_*$ only) is plain positive linear dependence, and with it the statement is false.

A second difficulty is complementarity (milestone 2). The safeguarded multipliers $\bar\mu_k$ do not vanish on inactive constraints. Whether $\mu_{k+1}$ does depends on whether the penalty parameters are bounded, which needs the update rule of Step 4.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\nabla$ is Mathlib's gradient. The problem is a structure of component functions indexed by Fin m. The standing assumption "continuous first derivatives on a sufficiently large and open domain" is read as ContDiff ℝ 1 on all of $\mathbb R^n$.

A run of Algorithm 3.1 is a predicate on sequences (IsRun), not a computed object:

• $x_0$ is the initial point and the outer iterations are $k\ge 1$;
• every outer iteration succeeds, which is the paper's standing assumption of §4;
• the three tolerances $\varepsilon_{k,1},\varepsilon_{k,2},\varepsilon_{k,3}$ of Step 2 are separate, as on the page;
• $\nabla L$ is the true gradient of the defined function (2.2);
• (3.1) uses the Euclidean norm, and (3.4) and Step 4 use the sup norm. The paper's norm is arbitrary, and only $\varepsilon_k\to 0$ enters.

KKT, CPLD and MFCQ are defined once for an abstract program with finite index types. The constraints of (2.1) enter as the families $h_1\oplus h_2$ and $g_1\oplus g_2$:

• the KKT definition includes feasibility, nonnegative inequality multipliers and complementarity;
• CPLD quantifies over subsets of equality indices and of active inequality indices, and requires linear dependence on a neighbourhood;
• gradient families are indexed by sum types, so repeated gradients count as dependent.

"Limit point" is MapClusterPt. (4.8) is required for every strictly increasing reindexing converging to $x_*$, and it bounds the unsafeguarded estimates $\lambda_{k+1}$, $\mu_{k+1}$; the safeguarded ones are bounded by construction and would make (4.8) trivial.

Trivializing formalizations are ruled out:

• a run is satisfiable (a sorry-free sanity check exhibits one, with a feasible CPLD limit point);
• KKT fails for a nonzero linear objective, so it is not automatic;
• the gradient is never applied to a function that is not differentiable under the hypotheses;
• gradient families are never collapsed into sets;
• the tolerances of Step 2 are not merged into $\varepsilon_k$.

Contributions welcome: proofs of the four milestones and of the goal, and in particular a reusable conic Carathéodory lemma and a library-level "approximate KKT + CPLD ⇒ KKT" theorem (milestone 3), which is useful well beyond this paper.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4):1286–1309, 2007. https://doi.org/10.1137/060654797 (HAL preprint hal-01295437v1 used here: https://hal.science/hal-01295437)
• L. Qi, Z. Wei, On the constant positive linear dependence condition and its application to SQP methods, SIAM J. Optim. 10(4):963–981, 2000. https://doi.org/10.1137/S1052623497326629
• R. Andreani, J. M. Martínez, M. L. Schuverdt, On the relation between constant positive linear dependence condition and quasinormality constraint qualification, J. Optim. Theory Appl. 125(2):473–485, 2005. https://doi.org/10.1007/s10957-004-1861-9
• O. L. Mangasarian, S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, J. Math. Anal. Appl. 17:37–47, 1967. https://doi.org/10.1016/0022-247X(67)90163-1
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60(5):627–641, 2011. https://doi.org/10.1080/02331930903578700
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999 (Carathéodory's theorem for cones, p. 689).

Why the penalty parameter matters

Augmented Lagrangian methods solve a constrained problem by minimizing a sequence of penalized subproblems while updating estimates of the Lagrange multipliers. Each subproblem carries a penalty parameter $\rho_k$. When $\rho_k$ grows without bound the subproblems become ill-conditioned and hard to solve, and the method behaves like a plain external penalty method. Avoiding that growth is one of the main reasons for using multiplier updates at all, so conditions under which $\rho_k$ stays bounded matter both in theory and in practice (Bertsekas 1982; Conn, Gould, Toint 1991).

Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); HAL hal-01295437) propose an augmented Lagrangian method, Algorithm 3.1, in which only some of the constraints are penalized. Their §5 shows that, under classical local hypotheses at the limit point and a subproblem tolerance tied to the current infeasibility, the penalty parameters remain bounded. This mission formalizes that result for equality-constrained problems (Theorem 5.4), together with the general case (Theorem 5.5) as a companion statement.

Setting

Let $f:\mathbb R^n\to\mathbb R$, $h_1:\mathbb R^n\to\mathbb R^{m_1}$, $g_1:\mathbb R^n\to\mathbb R^{p_1}$, $h_2:\mathbb R^n\to\mathbb R^{m_2}$, $g_2:\mathbb R^n\to\mathbb R^{p_2}$ be continuously differentiable. Problem (2.1) is

$$\text{Minimize } f(x)\ \text{ subject to } h_1(x)=0,\ g_1(x)\le0,\ h_2(x)=0,\ g_2(x)\le0 .$$

The upper-level constraints $h_1,g_1$ are penalized by the PHR augmented Lagrangian

$$L(x,\lambda,\mu,\rho)=f(x)+\frac\rho2\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}\rho\Big)^2+\frac\rho2\sum_{i=1}^{p_1}\Big([g_1(x)]_i+\frac{\mu_i}\rho\Big)_+^2,$$

while the lower-level constraints $h_2,g_2$ stay in the subproblems.

Algorithm 3.1 fixes $\tau\in[0,1)$, $\gamma>1$, $\rho_1>0$, a box $[\bar\lambda_{\min},\bar\lambda_{\max}]$, a bound $\bar\mu_{\max}\ge0$ and tolerances $\varepsilon_k\to0$. At outer iteration $k\ge1$ it finds $x_k$ and lower-level multipliers $v_k,u_k$ such that $x_k$ is an $\varepsilon_k$-approximate KKT point of minimizing $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ over the lower-level set, in the sense of (3.1)–(3.4). It then forms the first-order multiplier estimates

$$\lambda_{k+1}=\bar\lambda_k+\rho_k h_1(x_k),\qquad \mu_{k+1}=\max\{0,\bar\mu_k+\rho_k g_1(x_k)\},$$

and safeguarded estimates $\bar\lambda_{k+1},\bar\mu_{k+1}$, which in §5 are the projections of $\lambda_{k+1},\mu_{k+1}$ on their boxes. Finally it updates the penalty parameter: with $[\sigma_k]_i=\max\{[g_1(x_k)]_i,-[\bar\mu_k]_i/\rho_k\}$,

$$\rho_{k+1}=\begin{cases}\rho_k & \text{if } \max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}\le\tau\max\{\|h_1(x_{k-1})\|_\infty,\|\sigma_{k-1}\|_\infty\},\\ \gamma\rho_k & \text{otherwise.}\end{cases}$$

In §5.1 there are no inequality constraints ($p_1=p_2=0$): problem (5.1), with Lagrangian $L_0(x,\lambda,v)=f(x)+\langle h_1(x),\lambda\rangle+\langle h_2(x),v\rangle$. Assumptions 1–6 at the limit $x_*$ of $\{x_k\}$ are: convergence, feasibility, linear independence of all constraint gradients, $C^2$ near $x_*$, the second-order sufficient condition with multipliers $\lambda_*,v_*$, and $\lambda_*$ in the interior of the safeguard box.

Formalization targets

Goal: Theorem 5.4

Under Assumptions 1–6, $\tau>0$, and $\varepsilon_k\le\eta_k\|h_1(x_k)\|_\infty$ for a sequence $\eta_k\to0$,

$$\sup_k\rho_k<\infty .$$

Milestones, in attack order

1. Proposition 5.1: $\lambda_k\to\lambda_*$, $v_k\to v_*$, and $\bar\lambda_k=\lambda_k$ for $k$ large.
2. Lemma 5.2: there is $\bar\rho>0$ such that for all $\pi\in[0,1/\bar\rho]$

$$\begin{pmatrix}\nabla^2_{xx}L_0(x_*,\lambda_*,v_*)&\nabla h_1(x_*)&\nabla h_2(x_*)\\ \nabla h_1(x_*)^T&-\pi I&0\\ \nabla h_2(x_*)^T&0&0\end{pmatrix}\ \text{is nonsingular.}$$

3. Lemma 5.3: if $\rho_k\ge\bar\rho$ eventually, then for $k$ large

$$\|x_k-x_*\|,\ \|\lambda_{k+1}-\lambda_*\|\le M\max\Big\{\tfrac{\|\bar\lambda_k-\lambda_*\|_\infty}{\rho_k},\|\alpha_k\|,\|\beta_k\|\Big\},$$

with $\alpha_k=\nabla L(x_k,\bar\lambda_k,\rho_k)+\nabla h_2(x_k)v_k$ and $\beta_k=h_2(x_k)$. 4. (5.10): if $\rho_k\to\infty$, then $\|h_1(x_k)\|_\infty\le C\|\lambda_k-\lambda_*\|_\infty/\rho_k$ for $k$ large. 5. Contraction: if $\rho_k\to\infty$, then $\|h_1(x_k)\|_\infty\le (C/\rho_k)\|h_1(x_{k-1})\|_\infty$ for $k$ large.

Companion statements

Theorem 5.5, the general problem (2.1) under Assumptions 7–13 (LICQ, $C^2$, a second-order condition on the tangent subspace of all active constraints, multipliers inside the safeguard boxes, strict complementarity for the active upper-level inequalities), with $\varepsilon_k\le\eta_k\max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}$; and two steps of its proof, (5.13) and (5.14).

Significance

Theorem 5.4 tells a user of the method when it does not degenerate: if the safeguard box contains the true multipliers and the subproblems are solved to a precision proportional to the current infeasibility, then the penalty parameter is eventually constant. The Remark after Theorem 5.5 draws the practical conclusion that the box should be large enough to contain the true multipliers. The result underlies the analysis of the ALGENCAN solver built on Algorithm 3.1.

The results are proved on paper. To our knowledge none of them, nor the PHR augmented Lagrangian method itself, has a machine-checked formalization. A formal proof would also pin down two gaps in the printed statements, recorded under Formalization scope: the case $\tau=0$ and the early iterations in Lemma 5.3. The local analysis (a uniformly nonsingular KKT matrix and implicit-function error bounds for multiplier estimates) is reusable for other augmented Lagrangian and SQP methods.

Difficulty

Without the second-order structure there is no reason for $\rho_k$ to stay bounded: the update test compares consecutive infeasibilities, and nothing in the global theory forces them to decrease geometrically. The local argument has to show that $\|h_1(x_k)\|_\infty$ contracts by a factor of order $1/\rho_k$, which requires error bounds for both $x_k$ and $\lambda_{k+1}$ that hold uniformly as $1/\rho_k$ varies in an interval containing $0$. The uniformity in the perturbation parameter $\pi=1/\rho_k$, around the singular-looking limit $\pi=0$, is the central difficulty. Applying the implicit function theorem at each fixed $\rho$ does not give it.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Constraint maps are families of real functions indexed by Fin m, and problem (5.1) is (2.1) with $p_1=p_2=0$. The norm in (3.1), on $x$ and on $\alpha_k$ is Euclidean. Every $\|\cdot\|_\infty$, and the norms in (3.4), on $\lambda$ and on $\beta_k$, are the sup norm. The paper's norm is arbitrary and the constants absorb the change. A run of Algorithm 3.1 is a predicate on sequences: x 0 is $x_0$, the outer iterations are $k\ge1$, and the three tolerances of Step 2 are kept separate. The gradient in (3.1) is the true gradient of the defined augmented Lagrangian. "Continuous first derivatives" is $C^1$ on $\mathbb R^n$; "continuous second derivatives near $x_*$" is ContDiffAt ℝ 2. Hessians are derivatives of gradients. Every statement that uses a Hessian assumes $C^2$ at $x_*$, so it cannot be a junk value. Assumption 5 is pinned to Fletcher's equality-constrained second-order sufficient condition. Linear independence is that of a family indexed by a sum type, so equal gradients count as dependent.

Added hypotheses, each stated in the item's Formalization Note:

• $\tau>0$ in Theorems 5.4 and 5.5. With $\tau=0$ the theorem is false.
• Lemma 5.3 holds for $k\ge k_1$ instead of every $k$. It is false at early iterations.
• In Proposition 5.1, $\lambda_*,v_*$ are Lagrange multipliers at $x_*$.
• In Theorem 5.5, the multipliers are KKT multipliers of (2.1), and strict complementarity holds for the active lower-level inequalities. Without it the theorem fails when $\tau\gamma<1$.

Statements that would trivialize the goal are excluded. These include a run predicate that no sequence satisfies, merging the three tolerances into $\varepsilon_k$, collapsing gradient families into sets, a junk Hessian, and assuming $\rho_k\to\infty$ or $\rho_k\ge\bar\rho$ in the goal. The last two appear only as milestone hypotheses.

A complete development needs the PHR gradient formula, uniform invertibility of a continuous family of matrices on a compact interval, a quantitative inverse function estimate for $C^1$ maps, and the convergence of multiplier estimates under LICQ. Proofs of any milestone, and reusable lemmas for these pieces, are welcome.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4), 2007, 1286–1309. https://doi.org/10.1137/060654797 (HAL hal-01295437v1: https://hal.science/hal-01295437)
• R. Fletcher, Practical Methods of Optimization, 2nd ed., Wiley, 1987. https://doi.org/10.1002/9781118723203
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982. https://doi.org/10.1016/C2013-0-10366-2
• A. R. Conn, N. I. M. Gould, Ph. L. Toint, A globally convergent augmented Lagrangian algorithm for optimization with general constraints and simple bounds, SIAM J. Numer. Anal. 28(2), 1991, 545–572. https://doi.org/10.1137/0728030

Motivation

The proximal algorithm is the basic implicit scheme for minimizing a function $f$: from the current point $x^k$ it moves to a minimizer of $f$ plus a quadratic penalty on the distance travelled. For convex $f$ its convergence theory is classical (Martinet 1970, Rockafellar 1976). For nonconvex, nonsmooth $f$ the situation is different: descent and boundedness give only that limit points are critical, and the whole sequence may fail to converge even for smooth $f$ (Palis–de Melo; Absil, Mahony and Andrews, SIAM J. Optim. 2005).

Attouch and Bolte (Math. Program. 116, 2009, online 2007; author's version hal-00803898) showed that the Łojasiewicz inequality, which holds for real-analytic functions and for continuous subanalytic functions, restores convergence of the whole sequence for the nonsmooth proximal algorithm, together with explicit rates. The argument is Łojasiewicz's original gradient-flow idea transferred to a discrete, nonsmooth setting. It became the template for the later convergence analyses of proximal alternating minimization, forward–backward splitting and PALM under the Kurdyka–Łojasiewicz property, which are used throughout nonconvex optimization, signal processing and machine learning.

Timeline:

• 1963: Łojasiewicz proves his gradient inequality for real-analytic functions and deduces convergence of bounded gradient trajectories.
• 2005: Absil, Mahony and Andrews prove convergence of descent methods for analytic cost functions.
• 2007: Bolte, Daniilidis and Lewis extend the inequality to nonsmooth subanalytic functions with the limiting subdifferential (SIAM J. Optim. 17).
• 2007/2009: Attouch and Bolte prove the result of this mission for the proximal algorithm.

Setting

Points live in $\mathbb R^n$ with the Euclidean norm $|\cdot|$. Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ be proper (never $-\infty$, finite somewhere) and lower semicontinuous, with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$.

The limiting subdifferential $\partial f(x)$ is the set of limits $x^*$ of Fréchet subgradients $x_j^*\in\hat\partial f(x_j)$ along sequences $x_j\to x$ with $f(x_j)\to f(x)$. A point with $0\in\partial f(x)$ is critical, and the set of critical points is $\operatorname{crit} f$.

Fix $0<\lambda_-<\lambda_+<+\infty$ and step sizes $\lambda_k\in(\lambda_-,\lambda_+)$. From an arbitrary $x^0$ the proximal algorithm produces

$$x^{k+1}\in\operatorname{argmin}\Big\{f(u)+\frac{1}{2\lambda_k}|u-x^k|^2 : u\in\mathbb R^n\Big\}.\qquad(2)$$

Any minimizer may be selected. The standing hypotheses are

• (H1) $\inf_{\mathbb R^n} f>-\infty$;
• (H2) the restriction of $f$ to $\operatorname{dom} f$ is continuous;
• (H3) the Łojasiewicz property: for every critical point $\hat x$ there are $C,\varepsilon>0$ and $\theta\in[0,1)$ with

$$|f(x)-f(\hat x)|^\theta\le C|x^*|\qquad\forall x\in B(\hat x,\varepsilon),\ \forall x^*\in\partial f(x),\qquad(5)$$

with the convention $0^0=0$ (Remark 4). The number $\theta$ in (5) at a point is a Łojasiewicz exponent of that point.

$\omega(x^0)$ denotes the set of limit points of $(x^k)$.

Formalization targets

Goal: Theorem 4 (convergence)

Under (H1), (H2), (H3), if $(x^k)$ is bounded then

$$\sum_{k=0}^{\infty}|x^{k+1}-x^k|<+\infty\quad\text{and}\quad x^k\to x^\infty\in\operatorname{crit} f.$$

It fixes no constants and holds for every admissible step sequence and every selection in (2).

Milestones

• (3): $x^{k+1}=x^k-\lambda_k g^{k+1}$ with $g^{k+1}\in\partial f(x^{k+1})$.
• Proposition 2 (i)–(ii): $f(x^k)$ is nonincreasing and $\sum|x^{k+1}-x^k|^2<\infty$.
• Proposition 2 (iii): $\omega(x^0)\subset\operatorname{crit} f$ under (H2).
• Proposition 2 (iv): for bounded $(x^k)$, $\omega(x^0)$ is nonempty, compact and connected, and $d(x^k,\omega(x^0))\to0$.
• Lemma 3 (i): $f$ is constant on a connected set of critical points.
• Lemma 3 (ii): (5) holds with common constants on $\{x: d(x,K)\le\varepsilon\}$ for compact connected $K\subset\operatorname{crit} f$.
• (8) and (9), the one-step and summed length estimates of the proof.

Further statements

Theorem 5 (rates): with $\theta$ a Łojasiewicz exponent of $x^\infty$, $\theta=0$ gives finite termination, $\theta\in(0,\frac12]$ gives $|x^k-x^\infty|\le cQ^k$ with $Q\in[0,1)$, and $\theta\in(\frac12,1)$ gives $|x^k-x^\infty|\le c\,k^{-(1-\theta)/(2\theta-1)}$. Also: well-posedness of (2) under (H1), Proposition 2 (v), and Remark 2.

Significance

The theorem turns subsequential convergence into convergence of the whole sequence, with finite length, for a class that includes semi-algebraic, real-analytic and continuous subanalytic functions. Finite length is the property later used to analyse splitting and alternating schemes under the Kurdyka–Łojasiewicz property, and Theorem 5 is the first rate classification by the Łojasiewicz exponent for a nonsmooth algorithm.

The results are proved on paper. No machine-checked proof of Theorem 4 or Theorem 5 is known to exist. A formalization adds a checked convergence theorem for the nonsmooth proximal algorithm with extended-real-valued $f$, and a reusable set of descent, limit-set and uniformization lemmas that apply to other Łojasiewicz-type analyses.

Difficulty

Descent and $\sum|x^{k+1}-x^k|^2<\infty$ give only $|x^{k+1}-x^k|\to0$, which does not imply convergence: the iterates can circle a continuum of critical points with square-summable but non-summable steps, as in the counterexamples for smooth functions. The step that must be supplied is summability of $|x^{k+1}-x^k|$ itself. The local inequality (5) holds only near one critical point with its own constants, while the iterates approach a whole compact set $\omega(x^0)$, so the local constants first have to be made uniform near that set. The nonsmooth setting adds two difficulties: $f$ takes the value $+\infty$, and subgradients are limits of Fréchet subgradients, so their closure properties have to be established for this subdifferential.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $n=0$ is allowed. $f$ is EReal-valued and proper means never $\bot$ and somewhere not $\top$. Lower semicontinuity is Mathlib's LowerSemicontinuous. (H2) is ContinuousOn f {x | f x ≠ ⊤}. The limiting subdifferential and $\operatorname{crit} f$ are the published platform definitions NonconvexSplitting.Shared.LimitingSubdiff and NonsmoothLojasiewicz.Continuous.crit. Algorithm (2) is a predicate on a sequence (every step is some minimizer), not a proximal map. Limit points are cluster points of the sequence. The power in (5) is lojPow θ s = if s = 0 then 0 else s ^ θ, which implements $0^0=0$; real values of $f$ are used only where $f$ is finite.

Standing assumptions carried by the goal and Theorem 5: $f$ proper and lower semicontinuous, (H1), (H2), (H3), $0<\lambda_-<\lambda_+$ with $\lambda_k\in(\lambda_-,\lambda_+)$, a sequence complying with (2), and boundedness of its range. Milestones drop the assumptions their claims do not use. The milestones (8) and (9) also assume $x^{k+1}\ne x^k$ for all $k$ and use $\ell=\inf_k f(x^k)$. Both come from the proof's normalization. This reduction is not a hypothesis of Theorem 4: a goal that assumed it, mentioned the constants $\theta,M,N_0,r$, or assumed (8) would not be the paper's theorem.

The development needs the closure properties of the limiting subdifferential, the Fermat rule for proximal steps, and compactness and connectedness of limit sets of sequences with vanishing steps. These are reusable for every Łojasiewicz-type convergence proof. Proofs of individual milestones, of the rate lemmas in the proof of Theorem 5, and of the example $f(x)=|x|^2/2$ are welcome.

Selected references

• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116(1–2):5–16, 2009. https://doi.org/10.1007/s10107-007-0133-5 (author's version: https://hal.science/hal-00803898v1)
• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4):1205–1223, 2007. https://doi.org/10.1137/050644641
• P.-A. Absil, R. Mahony, B. Andrews, Convergence of the iterates of descent methods for analytic cost functions, SIAM J. Optim. 16(2):531–547, 2005. https://doi.org/10.1137/040605266
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, pp. 87–89.