Optimization

Motivation

Steepest descent is the oldest method for unconstrained minimization: to minimize a smooth function $f$, it moves from the current point $x_k$ along the negative gradient $-g_k = -\nabla f(x_k)$. It is the prototype of every first-order method, and its worst-case evaluation complexity — how many iterations it may need before the gradient norm drops below a tolerance $\epsilon$ — is the reference point against which faster methods are measured.

For a function that is bounded below and has a Lipschitz continuous gradient, steepest descent with a suitable step-length rule reaches $\|g_k\| \le \epsilon$ within $O(\epsilon^{-2})$ iterations (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Whether this bound is tight on nonconvex problems remained open until Cartis, Gould and Toint (preprint 15 October 2009; SIAM J. Optim. 20(6), 2010) built explicit one-dimensional examples showing that it is essentially sharp. The same paper shows that Newton's method can be as slow, and that the $O(\epsilon^{-3/2})$ bound of cubically regularized Newton methods is also tight; those results are the other missions of this series.

Timeline:

• 1983: Dennis and Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Theorem 6.3.3 — global convergence of steepest descent with a Goldstein–Armijo linesearch under twice continuous differentiability, boundedness below and a Lipschitz gradient.
• 2004: Nesterov's textbook states the $O(\epsilon^{-2})$ iteration bound for gradient methods on nonconvex functions with Lipschitz gradient.
• 2009/2010: Cartis, Gould and Toint construct, for every $\tau > 0$, examples on which steepest descent needs at least $\lfloor \epsilon^{-(2-\tau)} \rfloor$ iterations.

Setting

Let $f : \mathbb R \to \mathbb R$ be twice continuously differentiable, bounded below, with a derivative $f'$ that is bounded and Lipschitz continuous. The paper calls these standing assumptions AS.0. Write $g(x) = f'(x)$ for the gradient.

Steepest descent with step lengths $(\alpha_k)_{k\ge0}$ starts at $x_0 = 0$ and sets

$$x_{k+1} = x_k - \alpha_k\, g(x_k), \qquad k \ge 0.$$

The step lengths are only required to lie in a fixed interval (condition (2.6))

$$0 < \underline\alpha \le \alpha_k \le \overline\alpha < 2 .$$

Such step lengths can be produced by a Goldstein–Armijo linesearch, which accepts a step when the decrease $f(x_k) - f(x_{k+1})$ lies between $a\,\alpha_k|g_k|^2$ and $b\,\alpha_k|g_k|^2$ for fixed constants $0 < a < b < 1$.

Fix $\tau \in (0,1)$ and put $\eta = \eta(\tau) = \frac{1}{2-\tau} - \frac12 = \frac{\tau}{4-2\tau}$. The mission's definitions (namespace SlowConvergence.SteepestDescent) record the paper's prescribed data: iterates xk, steps sk, values fk, gradients $g_k = -(1/(k+1))^{\frac12+\eta}$ (gk), and the quintic pieces p with the quantities $\psi_k$, $\phi_k$, $\mu_k$ of (2.11)–(2.15).

Formalization targets

Goal: steepest descent can need $\lfloor \epsilon^{-(2-\tau)}\rfloor$ iterates

For every $\tau \in (0,1)$, every $0 < \underline\alpha \le \overline\alpha < 2$ and every step-length sequence with $\underline\alpha \le \alpha_k \le \overline\alpha$, there is $f$ satisfying AS.0 on all of $\mathbb R$ on which the steepest descent run from $x_0 = 0$ has

$$|f'(x_k)| = \Big(\frac{1}{k+1}\Big)^{\frac{1}{2-\tau}} \quad (k \ge 0), \qquad\text{hence}\qquad |f'(x_k)| \le \epsilon < 1 \;\Longrightarrow\; k+1 \ge \Big\lfloor \frac{1}{\epsilon^{2-\tau}} \Big\rfloor .$$

No constant (Lipschitz constant, gradient bound, lower bound) is fixed in the goal; only its existence is asserted.

Milestones

1. (2.10) and (2.3): $\eta > 0$ and $|g_k| = (1/(k+1))^{1/(2-\tau)}$.
2. The Goldstein–Armijo remark (p. 4): for $2(1-b) \le \alpha_k \le 2(1-a)$ the prescribed decrease satisfies both linesearch conditions.
3. (2.12)–(2.14): the quintic $p_k$ meets its six Hermite conditions on $[0,\mu_k]$.
4. (2.15): $0 < \psi_k < 1$.
5. (2.17): $|p_k''(t)| \le 1 + 150|\phi_k| \le 1 + 150\max[1,\overline\alpha]/\underline\alpha$ on $[0,\mu_k]$.
6. Lower bound (p. 5): $f_k - f_{k+1} \le \frac12 (1/(k+1))^{1+2\eta}$ and $f_k \ge 0$.

Significance

The result. Since $\tau > 0$ is arbitrary, the example shows that the $O(\epsilon^{-2})$ upper bound for steepest descent cannot be improved to $O(\epsilon^{-2+\tau})$ for any $\tau > 0$ under AS.0, even with a standard Goldstein–Armijo linesearch. It separates steepest descent from second-order methods with better worst-case bounds, and it is the template for the Newton and regularized-Newton examples of the same paper. A matching upper bound for gradient descent with step $1/L$ is formalized elsewhere on the platform (ShiOptRates.gd_exact_rate); together the two describe the complexity of the method up to the exponent $\tau$.

Formalizing it. The result is proved on paper; to our knowledge no machine-checked version exists. The mission adds a statement in which the method, the function class and the iteration count are fixed precisely. It also corrects three printed slips that a formal check exposes: the iteration count is off by one, the Goldstein–Armijo interval is printed reversed, and an intermediate step of (2.17) is false while its end bounds hold.

Difficulty

Matching prescribed values $f_k$ and gradients $g_k$ at the iterates is easy one point at a time. The difficulty is doing it with uniform control. The interval lengths $\mu_k$ shrink like $(k+1)^{-1/(2-\tau)}$, so a naive interpolant has second derivatives growing with $k$, and the gradient is then not globally Lipschitz. The prescribed values must also decrease at a rate whose sum stays finite, or the function is unbounded below. Both constraints pin the exponent: the construction works only because $\frac12 + \eta < 1$ makes the iterates escape to infinity while $1 + 2\eta > 1$ keeps $\sum_k (f_k - f_{k+1})$ finite. A further step remains: the paper's function lives on $[0,\infty)$ and must be extended to all of $\mathbb R$ without losing any property of AS.0.

Formalization scope

The problem is one-dimensional: f : ℝ → ℝ, the gradient is deriv f, and the second derivative is iteratedDeriv 2. AS.0 is ContDiff ℝ 2 f, BddBelow (Set.range f), a global bound on |deriv f|, and LipschitzWith L (deriv f). Every property holds on all of $\mathbb R$; the paper constructs $f$ on $[0,\infty)$ and says it extends smoothly to the negative reals, and that extension is part of the goal.

Conventions:

• $\tau \in (0,1)$: the construction needs it, and for $\epsilon < 1$ smaller $\tau$ gives larger counts, so the paper's "any $\tau > 0$" follows.
• The count is $k + 1 \ge \lfloor \epsilon^{-(2-\tau)} \rfloor$ (natural floor), the number of iterates $x_0, \dots, x_k$; the printed "iterations" count $k$ is off by one.
• Exponents are Real.rpow with base $1/(k+1) > 0$.
• The real zeta function is the series $\sum_{n\ge0} (1/(n+1))^t$, used only at $t = 1 + 2\eta > 1$.
• The step lengths are universally quantified before $f$, and the steepest-descent run is part of the conclusion, tied to $f$ by $x_{k+1} = x_k - \alpha_k f'(x_k)$. A goal asserting slow gradients along some sequence unrelated to $f$, or for one convenient step-length sequence only, would be trivial or weaker and is not the statement.

Infrastructure needed: quintic Hermite interpolation on intervals, gluing piecewise polynomials into a $C^2$ function on $[0,\infty)$ along an unbounded increasing knot sequence, a $C^2$ extension to the negative reals, and bounds for real $p$-series. The gluing lemma and the extension are reusable for the Newton and regularized-Newton missions of the series. Contributions of any milestone, of a construction of the glued function $f_1$ of (2.16), or of a direct proof of the goal are welcome.

Selected references

• C. Cartis, N. I. M. Gould, Ph. L. Toint, On the complexity of steepest descent, Newton's and regularized Newton's methods for nonconvex unconstrained optimization problems, SIAM J. Optim. 20(6), 2833–2852, 2010. https://doi.org/10.1137/090774100 (preprint 15 Oct 2009: https://people.maths.ox.ac.uk/cartis/papers/cgt36.pdf)
• J. E. Dennis, R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Prentice-Hall, 1983. https://doi.org/10.1137/1.9781611971200
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Quasi-Newton methods replace a costly exact Hessian with an operator updated from successive changes in position and gradient. A secant update must map the observed step $s$ to the observed gradient difference $y$. Many operators satisfy that one equation, so the choice of update needs another criterion. Gilbert and Lemaréchal's working paper studies variable-storage quasi-Newton algorithms and, in its Annex, characterizes familiar update formulas by how little they change the previous operator. The Annex treats real Hilbert spaces, rather than only matrices on Euclidean space, and allows the underlying scalar product and the weighting operator to vary. Its least-change characterization is the subject of this mission.

The source is the August 1988 IIASA Working Paper WP-88-121. A revised journal article appeared in 1989, but the theorem numbers and printed page references here belong to the working paper. The work is a formalization of a result proved in that paper; the mathematical question is not open.

Setting

Let $\mathcal H$ be a complete real inner-product space. A continuous linear operator $B$ is the current Hessian approximation. A step $s\in\mathcal H$ and a gradient difference $y\in\mathcal H$ determine the quasi-Newton equation $B_+s=y$ for the updated operator $B_+$. Write $B_+=B+P$, where $P$ is the perturbation. The source restricts $P$ to the Hilbert–Schmidt class $L_2(\mathcal H)$, so its size can be measured by an orthonormal basis $(e_i)_{i\in I}$:

$$\|P\|_{\mathrm{HS}}=\left(\sum_{i\in I}\|Pe_i\|^2\right)^{1/2}.$$

The index set $I$ need not be countable; membership in $L_2(\mathcal H)$ means the displayed family is summable. The value is independent of the chosen orthonormal basis. For $u,v\in\mathcal H$, the paper's bracket operator is $[u,v]d=\langle v,d\rangle u$. The order of its arguments matters.

The nonsymmetric feasible set is $\Pi=\{P\in L_2(\mathcal H):(B+P)s=y\}$. For a self-adjoint $B$, the symmetric problem uses $\Pi_S=\{P\in L_2(\mathcal H):P=P^*,\ (B+P)s=y\}$. A bijective continuous operator $R$ weights the symmetric objective $\|R^*PR\|_{\mathrm{HS}}$. The vector $c=R^{-*}R^{-1}s$ records how this weight changes the update. Both the feasible set and the weighted objective matter: taking a minimum over every bounded operator would change the problem.

Formalization targets

The goal is Proposition A.2 on printed p. 28 of the working paper. Suppose $B=B^*$, $R$ is bijective, and $s\ne0$. With $r=y-Bs$ and $c=R^{-*}R^{-1}s$, define

$$P_c=\frac{[r,c]+[c,r]}{\langle c,s\rangle} -\frac{\langle r,s\rangle}{\langle c,s\rangle^2}[c,c].$$

The target asserts that $P_c$ belongs to $\Pi_S$ and is the unique minimizer of $\|R^*PR\|_{\mathrm{HS}}$ over $P\in\Pi_S$. Its formula depends on $R$ only through $c$. No positivity condition on $B$ or on $\langle y,s\rangle$ is part of this result.

The milestones follow the source's supporting statements in order. They establish that the Hilbert–Schmidt sum is independent of the orthonormal basis and defines a norm on its domain; that the operator norm is bounded by this norm and the Hilbert–Schmidt class is stable under multiplication by bounded operators; the bracket identity $\|[u,v]\|_{\mathrm{HS}}=\|[u,v]\|_{\mathrm{op}}=\|u\|\|v\|$; the two bracket composition identities; Proposition A.1, the unique nonsymmetric least-change update for $\|R_1PR_2\|_{\mathrm{HS}}$; and its instance $R_2=I$, Broyden's update (A.5). The goal adds self-adjointness and a single two-sided weight.

The Annex then draws consequences of the goal, which are further milestones: the instance $R=I$ is the psb (Powell symmetric Broyden) update; Proposition A.3 states that for nonzero $y,s$ a self-adjoint positive operator ($\langle Bu,u\rangle>0$ for $u\ne0$) with $Bs=y$ exists if and only if $y=C^*Cs$ for a bijective $C$, if and only if $\langle y,s\rangle>0$; with $R=C^{-1}$ the weight becomes $c=y$ and (A.7) becomes the dfp (Davidon–Fletcher–Powell) update (A.8); and (A.9) is a product form of the dfp update from which its positivity follows when $B$ is self-adjoint positive and $\langle y,s\rangle>0$.

Significance

The theorem gives a precise optimization property to a rank-two symmetric secant formula. It identifies the operator selected by the weighted least-change criterion and guarantees there is no other feasible minimizer with the same value. Taking the weight to be the identity yields the psb update, and taking $R=C^{-1}$ with $C^*Cs=y$ yields the dfp update, so two of the classical symmetric secant formulas are least-change updates for different weights. Proposition A.1 similarly characterizes the rank-one update that becomes Broyden's formula when its right weight is the identity. These consequences explain why the familiar formulas arise from a common variational question, as the Annex states.

The paper supplies a mathematical proof. The remaining formalization work is to represent the Hilbert–Schmidt class, its norm and ideal property, the weighted objectives, and the exact minimization claims in Lean, then prove those claims. Mathlib supplies Hilbert spaces, Hilbert bases, bounded linear maps, adjoints, and the rank-one operator corresponding to the paper's bracket. The statements drafted for this mission compile, but they carry sorry and have no machine-checked proof from this mission yet. A completed development would leave reusable Hilbert–Schmidt and rank-one operator results beyond this quasi-Newton application.

Difficulty

The secant equation alone fixes an operator on only one vector. Even in two dimensions, a rank-one perturbation can satisfy that equation while failing to preserve self-adjointness. Requiring self-adjointness leaves many candidates, and minimizing the two-sided weighted Hilbert–Schmidt norm must distinguish exactly one of them. In infinite-dimensional spaces the norm also has a domain: some bounded operators have an infinite square sum. A formulation that silently assigns a finite default value to a nonsummable operator could turn the least-change claim into a different assertion. These are the mathematical and formal obstacles the milestone list exposes.

Formalization scope

Lean uses an arbitrary complete real inner-product space, with no finite-dimensional or separability assumption, and an arbitrary HilbertBasis index type. Each theorem takes a basis parameter; the basis-independence milestone states why this represents the paper's basis-free norm. The reusable definitions for the bracket and the Hilbert–Schmidt square sum are separate from the paper-specific feasible sets. bracket u v abbreviates Mathlib's rankOne ℝ u v, with $v$ paired with the input. A bijective bounded operator is represented by a continuous linear equivalence $R:\mathcal H\simeq\mathcal H$; the bounded inverse theorem makes this equivalent to the paper's bijective member of $L(\mathcal H)$. The definition of $c$ applies the adjoint of $R^{-1}$ to $R^{-1}s$.

Lean's real tsum has a default value when the family is not summable, so the Hilbert–Schmidt norm is used as a norm only for operators satisfying the explicit summability predicate. Both $\Pi$ and $\Pi_S$ include that predicate. The ideal-property milestone covers the weighted operators in the two objectives. The hypothesis $s\ne0$ is exactly the proposition's condition; it entails $\langle c,s\rangle=\|R^{-1}s\|^2>0$, so no extra nonzero-denominator hypothesis is imposed. The statement spells out “unique solution” as feasibility, minimality over every feasible perturbation, and equality of every feasible minimizer with $P_c$. The paper prints “problem (A.5)” in Proposition A.2, but (A.5) labels Broyden's displayed formula; its preceding paragraph defines the relevant symmetric minimization as (A.6). This mission formalizes (A.6).

In Proposition A.3 and (A.9), "positive" is the paper's strict notion $\langle Bu,u\rangle>0$ for $u\ne0$, not the non-strict positivity of Mathlib. The identity (A.9) is stated for self-adjoint $B$ and $\langle y,s\rangle\ne0$, the setting of the Annex's symmetric problem; the paper's sentence before the psb formula repeats the "(A.5)" misprint and is read as (A.6) in the same way.

The definition layer, basis independence, operator-ideal property, bracket results, both least-change propositions, and the Broyden, psb, dfp and positivity statements are welcome proof targets. The scaling results of §4.1 are outside this mission.

Selected references

• Jean Charles Gilbert and Claude Lemaréchal, Some numerical experiments with variable-storage quasi-Newton algorithms, IIASA Working Paper WP-88-121, August 1988, §2.1 and Annex, printed pp. 3 and 26–30. Working paper PDF.
• Jean Charles Gilbert and Claude Lemaréchal, Some numerical experiments with variable-storage quasi-Newton algorithms, Mathematical Programming 45 (1989), 407–435. DOI 10.1007/BF01589113. Cited for publication history; all statement indices above follow the working paper.

Motivation

Many objectives in statistics and machine learning are neither smooth nor convex, yet are well behaved in a weaker sense: robust phase retrieval, blind deconvolution, robust PCA and training with piecewise-linear losses all lead to weakly convex functions, functions that become convex after adding a fixed quadratic. For such functions the plain subgradient method $x_{k+1}=x_k-h\,f'(x_k)$ remains the method of choice, and the natural question is how fast it reaches approximate stationarity. Davis and Drusvyatskiy (SIAM J. Optim. 2019) gave the first such rate, measured by the gradient of the Moreau envelope, of order $\widetilde L^2\,4\kappa/\sqrt{N+1}$.

Das Gupta, Van Parys and Ryu (Math. Program. 204 (2024) 567–639) introduced BnB-PEP, a branch-and-bound method for solving nonconvex performance-estimation problems to global optimality, and used it to construct optimal and efficient first-order methods. Their one fully analytical result (§6.3) is a new potential-function analysis of the subgradient method on weakly convex functions with bounded subgradients. It produces an explicit stepsize and a rate that strictly improves on the Davis–Drusvyatskiy bound for all large enough $N$. The certificate was found numerically; the paper then gives a classical proof that can be checked by hand. This mission formalizes that result.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. A function $f:\mathbb R^d\to\mathbb R$ is $\rho$-weakly convex if $f+\frac{\rho}{2}\|\cdot\|^2$ is convex. For such $f$, a vector $g$ is a subgradient of $f$ at $x$, written $g\in\partial f(x)$, when

$$f(y)\ge f(x)+\langle g,y-x\rangle-\frac{\rho}{2}\|y-x\|^2\qquad\forall y\in\mathbb R^d .$$

The class $\mathcal W_{\rho,L}$ consists of the $\rho$-weakly convex $f$ whose subgradients all satisfy $\|g\|\le L$. Since $f\in\mathcal W_{\rho,L}$ exactly when $f/\rho\in\mathcal W_{1,L/\rho}$, the paper sets $\rho=1$ and writes $\widetilde L=L/\rho$; here the normalized bound is written $L$ (Lean: InWeakClass 1 L f, with subgradients IsWeakSubgrad 1 f x g).

For $\hat\rho>1$ the proximal point $\mathrm{prox}_{(1/\hat\rho)f}(x)$ is the unique minimizer of $y\mapsto f(y)+\frac{\hat\rho}{2}\|y-x\|^2$, and the Moreau envelope is the minimum value

$$f_{(1/\hat\rho)}(x)=\min_{y}\Big\{f(y)+\frac{\hat\rho}{2}\|y-x\|^2\Big\}$$

(Lean: SAGA.Convex.IsProxPoint f (1/ρ̂) x y and moreauEnv ρ̂ f x). The envelope is continuously differentiable, and its gradient $\nabla f_{(1/\hat\rho)}(x)=\hat\rho(x-y)$ is a subgradient of $f$ at the prox point $y$. With $\hat\rho=2$, the paper's choice, $\|\nabla f_{(1/2)}(x)\|$ small means that $x$ is near a point $y$ that is nearly stationary for $f$.

The method is $x_{k+1}=x_k-h\,f'(x_k)$ for $k\in[0:N]$, where each $f'(x_k)\in\partial f(x_k)$ is arbitrary. One writes $y_k=\mathrm{prox}_{(1/2)f}(x_k)$, $f'(y_k)=2(x_k-y_k)$, assumes a global minimizer $x_\star$ and the initial condition $f(y_0)-f(x_\star)+\|x_0-y_0\|^2\le R^2$, and sets $\kappa=R/L$.

Formalization targets

Goal: Corollary 1 (p. 625)

For the stepsize $h=\sqrt{4\kappa^2(N+1)+1}\,/\,(2(N+1))$, provided $h\le\frac12$,

$$\frac{1}{N+1}\sum_{i=0}^{N}\|\nabla f_{(1/2)}(x_i)\|^2\ \le\ \frac{L^2\big(2\sqrt{4\kappa^2(N+1)+1}-1\big)}{N+1}.$$

The bound holds for every choice of subgradients along the run.

Theorem 1 (p. 623)

For $h\in(0,\frac12]$, $b_{N+1}=0$, $b_k=4+(1-2h)b_{k+1}$ and $c_k=h^2b_{k+1}$, the potentials $\psi_k=b_k\big(f(y_k)-f(x_\star)+\|x_k-y_k\|^2\big)$ satisfy

$$\|f'(y_k)\|^2+\psi_{k+1}-\psi_k\le c_k\|f'(x_k)\|^2\quad(k\in[0:N]),\qquad \frac{1}{N+1}\sum_{i=0}^{N}\|\nabla f_{(1/2)}(x_i)\|^2\le\frac{1}{N+1}\Big(L^2\sum_{i=0}^{N}c_i+b_0R^2\Big).$$

Milestones

In proof order: the Moreau-envelope facts of §6.3.1; the one-step inequality (32) for an arbitrary point; the telescoping display after (32); the closed form (44) of $b_k$ with nonnegativity; Theorem 1; the closed form (45) of its bound in $h$; the majorant (46) with Bernoulli's upper bound; and the minimizer $h^\star_{\mathrm{ub}}$ of (46) with its value.

Significance

The result. Corollary 1 gives an explicit, non-asymptotic rate for the most basic method of nonsmooth nonconvex optimization, with explicit constants and an explicit stepsize. As $N\to\infty$ the bound is asymptotic to $4\kappa L^2/\sqrt{N+1}$, and the paper shows it is strictly below the earlier bound $L^2\,4\kappa/\sqrt{N+1}$ once $N>(9-64\kappa^2)/(64\kappa^2)$. It also bounds $\min_{i\le N}\|\nabla f_{(1/2)}(x_i)\|^2$. It shows that computer-assisted performance estimation can produce closed-form guarantees beyond the convex, interpolable function classes where PEP is usually applied.

Formalizing it. The result is proved on paper twice (pp. 622–627), but nothing about weakly convex functions, their subdifferential or the Moreau envelope in the nonconvex regime is formalized on the platform, and the convergence analysis has not been machine-checked. A complete development formalizes the potential-function proof and supplies reusable facts about weakly convex functions and the Moreau envelope.

Difficulty

The scalar part of the argument ((44)–(46) and the plug-in) is elementary algebra and one Bernoulli inequality. The analytic weight sits in two places. First, the Moreau envelope of a nonconvex function: showing that the real infimum is attained at the prox point, that the envelope is differentiable with gradient $\hat\rho(x-y)$, and that this gradient is a subgradient of $f$ at $y$ with the weak-convexity modulus $1$ (not the modulus $\hat\rho$ that the prox inequality gives directly). Second, inequality (32): it is not a consequence of convexity, since $f$ is not convex, and it must hold for an arbitrary current point and an arbitrary subgradient, with parameters $b_k,c_k$ fixed in advance. The obvious route through descent of $f$ itself fails: $f(x_k)-f(x_\star)$ need not decrease for nonconvex $f$, which is why the potential uses the envelope at the iterates.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin d), and $f$ is real-valued and defined everywhere. The weak-convexity modulus is normalized to $\rho=1$, and the Lean name L is the paper's $\widetilde L$; the general class $\mathcal W_{\rho,L}$ follows by scaling and is not stated. The subdifferential is the weak-convexity inequality above. For weakly convex $f$ it equals the Clarke, Fréchet and limiting subdifferentials, so it is the paper's abstract $\partial f$ in every admissible instance. The convex subdifferential of $f$ is not used: it can be empty for nonconvex $f$ and would make the statements vacuous. The run is given by sequences x g y : ℕ → E, with g k an arbitrary subgradient at x k for $k\le N$, and y k tied to x k by IsProxPoint f (1/2) for $k\le N+1$. $f'(y_k)$ is not free: it is $2(x_k-y_k)$. The Moreau envelope is a real ⨅; it is finite and attained in this regime, and the first milestone proves this. The parameters $b,c$ of Theorem 1 are pinned by hypotheses, not chosen existentially.

Two hypotheses are made explicit. Corollary 1 is stated "in the setup of Theorem 1", which requires $h\in(0,\frac12]$; for the prescribed stepsize this is $4\kappa^2(N+1)+1\le(N+1)^2$, and it is carried as the hypothesis $h\le\frac12$. It fails for $N=0$ and whenever $\kappa$ is large relative to $N$. Inequality (32) is stated for one arbitrary step, under the nonnegativity of the alternate proof's weights ($h\ge0$, $b_{k+1}\ge0$, $hb_{k+1}\le2$). The minimizer $x_\star$ is assumed, as in the paper; the remark on p. 627 that $\inf f>-\infty$ suffices is not used.

Useful contributions include basic lemmas on weakly convex functions (existence of subgradients, strong convexity of the prox subproblem), differentiability of the Moreau envelope for $\hat\rho>\rho$, the weighted-sum identity behind (32), and Bernoulli's upper bound $(1+a)^r\le 1/(1-ra)$ for $a\in[-1,0]$.

Selected references

• S. Das Gupta, B. P. G. Van Parys, E. K. Ryu, Branch-and-bound performance estimation programming: a unified methodology for constructing optimal optimization methods, Mathematical Programming 204 (2024) 567–639. https://doi.org/10.1007/s10107-023-01973-1
• D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM Journal on Optimization 29(1) (2019) 207–239. https://doi.org/10.1137/18M1178244
• Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Mathematical Programming 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
• A. B. Taylor, J. M. Hendrickx, F. Glineur, Smooth strongly convex interpolation and exact worst-case performance of first-order methods, Mathematical Programming 161 (2017) 307–345. https://doi.org/10.1007/s10107-016-0985-6

Motivation

Many large optimization problems arising in networked control, smart grids, distributed estimation and resource allocation have a separable objective with coupled affine constraints: $N$ agents each own a variable $x_i$ and a private cost $f_i$, and only a linear constraint $\sum_i A_ix_i=b$ ties them together. Distributed algorithms for such problems let each agent solve a small local problem and exchange only a few aggregated quantities. For convex problems the standard method is the alternating direction method of multipliers (ADMM), which converges at a linear rate; for nonconvex problems ADMM can diverge (Houska, Frasch and Diehl give a two-variable example in §2 of their paper).

Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton method), which combines the decoupled augmented-Lagrangian subproblems of ADMM with a coupled equality-constrained quadratic program borrowed from sequential quadratic programming (SQP). Their local convergence analysis (§7) rests on one stability result for the decoupled subproblems, Lemma 3, which this mission formalizes. Similar statements are classical for augmented Lagrangian methods: Bertsekas analyzes minimizers of augmented Lagrangians under perturbation of the multiplier (Constrained Optimization and Lagrange Multiplier Methods, 1982, Prop. 4.2.3), and Nocedal and Wright give a related analysis (Numerical Optimization, 2nd ed., 2006, Thm. 17.6).

Setting

Problem (1.1). Given $f_i:\mathbb R^n\to\mathbb R$, $h_i:\mathbb R^n\to\mathbb R^{n_h}$, $A_i\in\mathbb R^{m\times n}$ ($i=1,\dots,N$) and $b\in\mathbb R^m$,

$$\min_{x}\ \sum_{i=1}^N f_i(x_i)\qquad\text{s.t.}\qquad \sum_{i=1}^N A_ix_i=b,\qquad h_i(x_i)\le 0\ \ (i=1,\dots,N).$$

All $f_i$ and $h_i$ are twice continuously differentiable (the paper's standing assumption in §3). The multiplier of the coupling constraint is $\lambda\in\mathbb R^m$, that of $h_i(x_i)\le0$ is $\kappa_i\in\mathbb R^{n_h}$.

A KKT point $(x^*,\lambda^*,\kappa)$ is feasible, satisfies $\nabla f_i(x^*_i)+A_i^\top\lambda^*+\sum_j\kappa_{ij}\nabla h_{ij}(x^*_i)=0$ for every $i$, and has $\kappa\ge0$ with $\kappa_{ij}h_{ij}(x^*_i)=0$. It is regular if

• LICQ holds: the rows of $[A_1\cdots A_N]$ and the block gradients of the active constraints $h_{ij}(x^*_i)=0$ are linearly independent in $\mathbb R^{Nn}$;
• strict complementarity holds: $\kappa_{ij}>0$ on every active constraint;
• the second-order sufficient condition holds: $\sum_i d_i^\top\nabla^2[f_i+\kappa_i^\top h_i](x^*_i)d_i>0$ for every nonzero $d$ in the critical subspace $\{\sum_iA_id_i=0,\ \nabla h_{ij}(x^*_i)^\top d_i=0 \text{ on active }(i,j)\}$.

The decoupled subproblems. In step 1 of ALADIN, given the current primal and dual iterates $(x,\lambda)$, a penalty $\rho>0$ and positive semidefinite scaling matrices $\Sigma_i$, agent $i$ solves

$$\min_{y_i}\ f_i(y_i)+\lambda^\top A_iy_i+\frac\rho2\|y_i-x_i\|_{\Sigma_i}^2\qquad\text{s.t.}\qquad h_i(y_i)\le 0, \tag{3.2}$$

with $\|v\|_{\Sigma}^2=v^\top\Sigma v$. These problems are nonconvex in general and are solved to local optimality.

Formalization targets

Goal: Lemma 3 (p. 1117)

Let $x^*$ be a local minimizer of (1.1) with $(x^*,\lambda^*,\kappa)$ a regular KKT point, and let $\rho>0$ satisfy

$$\nabla^2\big[f_i+\kappa_i^\top h_i\big](x^*_i)+\rho\Sigma_i\succ 0\qquad(i=1,\dots,N).$$

Then for every sufficiently small ball $\mathcal N$ of radius $\varepsilon$ around the origin of $\mathbb R^{Nn}\times\mathbb R^m$ there are constants $\chi,\chi_1,\chi_2<\infty$ such that for all $(x,\lambda)$ with $(x-x^*,\lambda-\lambda^*)\in\mathcal N$ the problems (3.2) have local minimizers $y=(y_1,\dots,y_N)$, unique in $\{x^*\}\oplus\chi\mathcal N$, with

$$\|y-x^*\|\ \le\ \chi_1\|x-x^*\|+\chi_2\|\lambda-\lambda^*\| .$$

The constants are not specified: the goal asserts only the shape of the estimate, not values of $\chi_1,\chi_2$.

Milestones (steps of the paper's proof, p. 1117)

1. The Hessians $\nabla^2[f_i+\kappa'^\top h_i](\xi)+\rho\Sigma_i$ remain positive definite for $(\xi,\kappa')$ near $(x^*_i,\kappa_i)$.
2. At $(x,\lambda)=(x^*,\lambda^*)$, $x^*_i$ is a stationary point with multiplier $\kappa_i$ and a strict local minimizer of the $i$-th subproblem: $\xi_i(x^*,\lambda^*)=x^*_i$.
3. Near $(x^*,\lambda^*)$ the subproblems have locally unique local minimizers $\xi_i(x,\lambda)$ depending continuously differentiably on $(x,\lambda)$.
4. If $\chi_1>\|\partial_x\xi\|$ and $\chi_2>\|\partial_\lambda\xi\|$ at $(x^*,\lambda^*)$, then $\|\xi(x,\lambda)-\xi(x^*,\lambda^*)\|\le\chi_1\|x-x^*\|+\chi_2\|\lambda-\lambda^*\|$ locally.

Significance

Lemma 3 is the bridge between ALADIN and the local theory of SQP. Once the decoupled minimizers are known to exist, to be locally unique, and to stay within a linear distance of $x^*$, the full-step variant of ALADIN behaves locally like an inexact SQP method, and the paper derives its local quadratic convergence estimates (with exact Hessians and a suitably large $\mu$) from this. Without the lemma the local subproblems could jump between distant local minimizers of a nonconvex objective, and no local rate could be claimed.

The result is proved in the paper, in a short paragraph that delegates the main step to the regularity of the KKT point. No machine-checked version of this lemma, of the sensitivity theory of parametric nonlinear programs it rests on, or of ALADIN exists, as far as a search of the Prove2Me catalogue and Mathlib shows. Formalizing it means supplying the argument the paper leaves implicit: a parametric local-minimizer theorem for inequality-constrained problems under LICQ, strict complementarity and a second-order condition.

Difficulty

The obvious argument applies the implicit function theorem to the stationarity condition of (3.2), $\nabla f_i(y_i)+A_i^\top\lambda+\rho\Sigma_i(y_i-x_i)=0$. That works only without inequality constraints. With constraints, the local minimizer satisfies a KKT system involving the multipliers and complementarity, which is not a smooth equation; one has to fix the active set, use strict complementarity to show that it does not change nearby, and use LICQ of the active constraints to make the reduced KKT matrix invertible. The second difficulty is uniqueness: the implicit function theorem gives a unique KKT point near $(x^*_i,\kappa_i)$, but the lemma claims uniqueness among local minimizers within a ball in the primal variable alone, so the multipliers of any nearby local minimizer must be shown to lie near $\kappa_i$. Third, the hypothesis is the positive definiteness of $\nabla^2[f_i+\kappa_i^\top h_i]+\rho\Sigma_i$ on all of $\mathbb R^n$, not only on the critical cone; the subproblems inherit their second-order condition from it rather than from the SOSC of (1.1).

Formalization scope

Vectors are Fin n → ℝ with Mathlib's sup norm, blocks are indexed by Fin N, matrices are Mathlib Matrix over Fin index types, and $\lambda\in$ Fin m → ℝ. Gradients and Hessians enter through Fréchet derivatives (fderiv), with $d^\top\nabla^2g(z)d$ written fderiv ℝ (fderiv ℝ g) z d d. LICQ is stated as linear independence of the active gradients in $\mathbb R^{Nn}$. The "sufficiently small open set $\mathcal N$" is read as every ball of radius $\varepsilon\in(0,\varepsilon_0]$ in the sup norm of $\mathbb R^{Nn}\times\mathbb R^m$, with $\chi,\chi_1,\chi_2$ allowed to depend on $\varepsilon$ but not on $(x,\lambda)$; $y\in\{x^*\}\oplus\chi\mathcal N$ is read through the $x$-component, $\|y-x^*\|<\chi\varepsilon$. Local minimizers are local minimizers on the feasible set and are required to be feasible. The hypotheses $h_i\in C^2$ and $\Sigma_i\succeq0$ come from the paper's standing assumptions (§3 and Algorithm 2, step 1).

A trivializing formalization is ruled out: the goal keeps all four conclusions (local minimality, membership in the $\chi\varepsilon$-ball, uniqueness in that same ball, and the bound), since the bound alone is satisfied by $y=x^*$; and it quantifies over every small ball rather than asserting the result for one neighbourhood. The hypotheses are satisfiable: a sorry-free check with $N=n=m=n_h=1$, $f=0$, $h=-1$, $A=1$, $b=0$, $\Sigma=1$, $\rho=1$ is in the development.

Needed infrastructure: a parametric implicit-function argument for KKT systems with a fixed active set, persistence of LICQ and of strict complementarity under perturbation, and second-order sufficiency for inequality-constrained problems. These pieces are reusable well beyond this mission, for any sensitivity or local-convergence analysis of nonlinear programs (SQP, augmented Lagrangian, interior-point methods). Proofs of any milestone, alternative routes (for instance via Robinson's strong regularity), and general lemmas on second-order sufficient conditions are welcome.

Selected references

• B. Houska, J. Frasch, M. Diehl, An augmented Lagrangian based algorithm for distributed nonconvex optimization, SIAM J. Optim. 26(2), 1101–1127, 2016. https://doi.org/10.1137/140975991
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982, Proposition 4.2.3.
• S. M. Robinson, Strongly regular generalized equations, Math. Oper. Res. 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43

Motivation

Worst-case iteration counts are the standard way to compare unconstrained optimization methods on nonconvex problems. For finding an approximate first-order critical point, a point with $\|\nabla f(x)\|\le\epsilon$, steepest descent needs at most $O(\epsilon^{-2})$ iterations on functions with a Lipschitz gradient. The cubic regularization of Newton's method needs at most $O(\epsilon^{-3/2})$ iterations on functions with a Lipschitz Hessian. This bound was proved by Nesterov and Polyak (2006) for exact global model minimization (doi:10.1007/s10107-006-0706-8). Cartis, Gould and Toint (2009a, 2011) extended it to the adaptive variant ARC with approximate model minimization (doi:10.1007/s10107-009-0286-5).

An upper bound alone leaves open whether a better analysis could lower it. Cartis, Gould and Toint (SIAM J. Optim. 20(6), 2010, doi:10.1137/090774100) settle this for three methods by explicit one- and two-dimensional examples. This mission formalizes the third: the $O(\epsilon^{-3/2})$ bound for ARC is sharp up to an arbitrarily small loss in the exponent.

Timeline:

• 2006: Nesterov and Polyak prove the $O(\epsilon^{-3/2})$ bound for cubic regularization with exact global model minimization.
• 2009–2011: Cartis, Gould and Toint introduce ARC with an adaptive weight and inexact minimization, and prove the same order.
• 2010: the same authors construct functions on which steepest descent, Newton's method and ARC attain their worst-case orders up to $\tau$. The ARC example is in §5 of that paper.

Setting

Let $f:\mathbb R\to\mathbb R$ be twice continuously differentiable, and write $g(x)=f'(x)$, $H(x)=f''(x)$. At an iterate $x_k$, with a regularization weight $\sigma_k>0$, the cubic model (1.3) is

$$m_k(x_k+s)=f(x_k)+g(x_k)\,s+\tfrac12H(x_k)\,s^2+\tfrac13\sigma_k|s|^3 .$$

One iteration of the Adaptive Regularization with Cubics (ARC) algorithm, in the variant considered here, proceeds as follows.

1. Compute a step $s_k$ that globally minimizes $s\mapsto m_k(x_k+s)$.
2. Form the ratio $\rho_k=\dfrac{f(x_k)-f(x_k+s_k)}{f(x_k)-m_k(x_k+s_k)}$.
3. Accept $x_{k+1}=x_k+s_k$ if $\rho_k\ge\eta_1$, and set $x_{k+1}=x_k$ otherwise.
4. Update the weight: $\sigma_{k+1}\in(0,\sigma_k]$ if $\rho_k>\eta_2$ (a very successful iteration), $\sigma_{k+1}\in[\sigma_k,\gamma_1\sigma_k]$ if $\eta_1\le\rho_k\le\eta_2$, and $\sigma_{k+1}\in[\gamma_1\sigma_k,\gamma_2\sigma_k]$ otherwise.

The parameters satisfy $\gamma_2\ge\gamma_1>1$ and $1>\eta_2\ge\eta_1>0$. In Lean the model is SlowConvergence.ARC.model, the ratio rho, and a run is the predicate IsARCRun f γ₁ γ₂ η₁ η₂ x s σ.

The paper fixes $\tau>0$ and sets $\eta=\eta(\tau)=\tfrac12\big(\tfrac2{3-2\tau}-\tfrac23\big)$. It then prescribes iterates $x_0=0$, $x_{k+1}=x_k+s_k$ with $s_k=(1/(k+1))^{1/3+\eta}$, and function values $f_{4,k}$ (5.3). At the iterates it prescribes gradients $g_k=-(1/(k+1))^{2/3+2\eta}$, Hessians $H_k=0$ and weights $\sigma_k=1$ (5.4).

Formalization targets

Goal

For every $\tau\in(0,1)$ there are a function $f$ and a run of ARC on it from $x_0=0$, $\sigma_0=1$, with the following properties:

• $f$ is $C^2$ and bounded below, and $f''$ is bounded and globally Lipschitz;
• the run is valid for every admissible $\gamma_1,\gamma_2,\eta_1,\eta_2$, and every iteration is very successful;
• the gradients satisfy

$$|f'(x_k)|=\Big(\frac1{k+1}\Big)^{\frac2{3-2\tau}}\quad(k\ge0),\qquad\text{so}\qquad |f'(x_k)|\le\epsilon\ \Longrightarrow\ k+1\ \ge\ \Big\lfloor\frac1{\epsilon^{3/2-\tau}}\Big\rfloor\quad(0<\epsilon<1).$$

The goal fixes no Lipschitz constant or Hessian bound; it asserts the existence of the example, which is the paper's claim.

Milestones

• $\eta=2\tau/(9-6\tau)>0$, and (5.4) gives (5.1).
• (5.5)–(5.8): the prescribed data are an ARC run, each step is an exact global model minimizer, and every iteration is very successful.
• (5.9)–(5.11): the coefficients (5.11) solve the Hermite interpolation conditions on $[0,s_k]$.
• $\phi_k\in(0,1)$.
• (5.12): $|p_k'''(t)|\le452$ on $[0,s_k]$, uniformly in $k$.
• $|p_k'''(0)|\le20$.
• The prescribed values $f_{4,k}$ are nonnegative.

Significance

The example shows that the $O(\epsilon^{-3/2})$ upper bound of Nesterov–Polyak and Cartis–Gould–Toint cannot be improved to $O(\epsilon^{-3/2+\tau})$ for any $\tau>0$, even in one dimension and with exact global model minimization. It also shows that adaptive weights do not help: the run is valid for every choice of the algorithm's parameters. Together with the paper's other two examples, it separates the worst-case orders of steepest descent and Newton's method ($\epsilon^{-2}$) from that of ARC ($\epsilon^{-3/2}$). The paper ends by asking whether $\epsilon^{-3/2}$ is optimal among all second-order methods. That question was answered later by Carmon, Duchi, Hinder and Sidford (2020) for a broad algorithm class.

The paper's argument is a construction checked by hand plus a plot of the first sixteen intervals. No machine-checked version of this lower bound is known to exist. A formal proof would certify every interpolation identity, the uniform third-derivative bound and the gluing into a globally $C^2$ function. The upper bounds of Nesterov and Polyak are separate statements on the platform (CubicNewton.Nonconvex.*) and are not proved there.

Difficulty

Checking the algebra at the iterates is routine; the difficulty is the function. The piecewise quintic must be twice continuously differentiable across infinitely many knots. Its second derivative must be Lipschitz with one constant on the whole line, although the intervals shrink like $(k+1)^{-1/3-\eta}$. This requires a third-derivative bound that does not grow with $k$. The obvious first idea is to interpolate values and slopes with cubics; it fails, because the second derivative must vanish at both ends of every interval to match $H_k=0$. A further step is that the knots $x_k$ go to $+\infty$ only because $1/3+\eta<1$, which is where $\tau<1$ enters. Finally, $f$ must be extended to $x<0$ without losing boundedness below or the global Lipschitz bound.

Formalization scope

• Representation. One dimension: f : ℝ → ℝ, $g$ = deriv f, $H$ = deriv (deriv f), $|\cdot|$ for the norm. The model uses the true second derivative of the same $f$, not a free approximation $B_k$. The step is a global minimizer of the model; uniqueness is not required.
• Algorithm. The paper cites but does not restate ARC. The acceptance rule and the weight update are those of Algorithm 2.1 of Cartis, Gould and Toint (2009a). Lean's $a/0=0$ makes $\rho_k=0$ when the predicted decrease vanishes, which never happens on this example.
• Corrections to the printed text. $\tau\in(0,1)$ instead of "any $\tau>0$" (for $\epsilon<1$ the bounds for small $\tau$ imply the others). The count is $k+1$ rather than $k$: the printed "at least $\lfloor1/\epsilon^{3/2-\tau}\rfloor$ iterations" is off by one for iterations, and correct for iterates/function evaluations. The verification (5.5)–(5.8) is stated for all $k\ge0$, not "$k\ge1$". The bound (5.12) is stated by its two ends only, because its middle lines drop absolute values.
• Domain. $f$ is required on all of $\mathbb R$, with every property global. The paper builds $f$ on $[0,\infty)$ and asserts the extension.
• Ruling out trivial versions. The run and the function are existentially quantified in the conclusion, never assumed. The gradient formula is an equality and the run must satisfy every ARC rule for every parameter choice. Hence neither a vacuous run hypothesis nor a degenerate $f$ (e.g. one whose gradients vanish) proves the goal.
• Infrastructure. The milestones are about the explicit data: Data (iterates, values, gradients, the model built from them) and Pieces (the quintics $p_k$, $\phi_k$). Proofs of the polynomial identities and of gluing infinitely many polynomial pieces into a $C^2$ function with a global Lipschitz second derivative are reusable for the paper's other two examples. Proofs of the milestones, of the gluing lemma, and of the goal are all welcome.
• Related platform objects. CubicNewton.Shared.cubicModel and IsCubicStep are the same model and step in $\mathbb R^n$ with $M=2\sigma$; they are not imported here.

Selected references

• C. Cartis, N. I. M. Gould, Ph. L. Toint, On the complexity of steepest descent, Newton's and regularized Newton's methods for nonconvex unconstrained optimization problems, SIAM J. Optim. 20(6), 2010; preprint 15 Oct 2009. doi:10.1137/090774100
• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Math. Program. 127, 2011 (cited as 2009a). doi:10.1007/s10107-009-0286-5
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108, 2006. doi:10.1007/s10107-006-0706-8
• Y. Carmon, J. C. Duchi, O. Hinder, A. Sidford, Lower bounds for finding stationary points I, Math. Program. 184, 2020. doi:10.1007/s10107-019-01406-y

Motivation

Methods for smooth unconstrained minimization, $\min_{x\in\mathbb R^n} f(x)$, are compared by how many evaluations of $f$ and of its gradient they need, in the worst case, to reach an approximately first-order critical point, an iterate with $\|\nabla f(x_k)\|\le\epsilon$. For steepest descent with a Lipschitz gradient the answer is $O(\epsilon^{-2})$ (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Nesterov and Polyak (2006) showed that globally minimizing a cubic regularisation of the second-order model, with the exact Hessian and a global Lipschitz constant, improves this to $O(\epsilon^{-3/2})$.

The adaptive regularisation with cubics (ARC) framework of Cartis, Gould and Toint makes that idea practical: the Hessian is replaced by an approximation $B_k$, the Lipschitz constant by an adaptive weight $\sigma_k$, and the global model minimizer by any step that does at least as well as a Cauchy point. Part I (Math. Program. 127, 2011) proved global convergence; Part II (Math. Program. 130, 2011) counts evaluations. This mission covers the first count of Part II (§§2–3): with only the Cauchy condition on the step, ARC needs $O(\epsilon^{-2})$ iterations, the same order as steepest descent and as trust-region methods (Gratton, Sartenaer and Toint, SIAM J. Optim. 19, 2008).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be continuously differentiable (AF.1), $g(x)=\nabla f(x)$, and $\|\cdot\|$ the Euclidean norm. At iterate $x_k$, with a symmetric matrix $B_k$ and a weight $\sigma_k>0$, the cubic model is

$$m_k(s)=f(x_k)+s^Tg_k+\tfrac12 s^TB_ks+\tfrac13\sigma_k\|s\|^3,\qquad g_k=g(x_k).$$

Algorithm 2.1 (ARC) takes parameters $\gamma_2\ge\gamma_1>1$, $1>\eta_2\ge\eta_1>0$, $\sigma_0>0$ and a starting point $x_0$. At iteration $k$ it

1. picks any step $s_k$ satisfying the Cauchy condition $m_k(s_k)\le m_k(-\alpha g_k)$ for every $\alpha\ge0$;
2. computes $\rho_k=\big(f(x_k)-f(x_k+s_k)\big)/\big(f(x_k)-m_k(s_k)\big)$;
3. sets $x_{k+1}=x_k+s_k$ if $\rho_k\ge\eta_1$ (a successful iteration), and $x_{k+1}=x_k$ otherwise (unsuccessful);
4. picks $\sigma_{k+1}$ in $(0,\sigma_k]$ if $\rho_k>\eta_2$ (very successful), in $[\sigma_k,\gamma_1\sigma_k]$ if $\eta_1\le\rho_k\le\eta_2$, and in $[\gamma_1\sigma_k,\gamma_2\sigma_k]$ otherwise.

For $j\ge0$, $\mathcal S_j$ and $\mathcal U_j$ are the successful and unsuccessful iterations among $0,\dots,j$. The complexity results use three assumptions: AM.1, $\|B_k\|\le\kappa_B$ for all $k$; AF.4, $\|g(x)-g(y)\|\le\kappa_H\|x-y\|$ on an open convex set $X$, with $\kappa_H\ge1$; and a lower bound $f(x_k)\ge f_{\rm low}$. Optionally, (2.10): $\sigma_{k+1}\ge\gamma_3\sigma_k$ on very successful iterations, for some $\gamma_3\in(0,1]$. The constants are

$$\kappa_{HB}=\frac{108\sqrt2}{1-\eta_2}(\kappa_H+\kappa_B),\qquad \alpha_C=\Big[6\sqrt2\max\big(1+\kappa_B,2\max(\sqrt{\sigma_0},\kappa_{HB}\sqrt{\gamma_2})\big)\Big]^{-1},$$ $$\kappa^s_C=\frac{f(x_0)-f_{\rm low}}{\eta_1\alpha_C},\qquad \kappa^u_C=\frac{1}{\log\gamma_1}\max\Big(1,\frac{\gamma_2\kappa_{HB}^2}{\sigma_0}\Big),\qquad \kappa_C=\Big(1-\frac{\log\gamma_3}{\log\gamma_1}\Big)\kappa^s_C+\kappa^u_C.$$

Formalization targets

Goal: Corollary 3.4

Let $\epsilon\in(0,1]$ with $\|g_0\|>\epsilon$, and let $j_1\le\infty$ be the first iteration with $\|g_{j_1+1}\|\le\epsilon$. Then

$$|\mathcal S_{j_1}|\le L^s_1=\big\lceil\kappa^s_C\,\epsilon^{-2}\big\rceil,$$

and, if (2.10) holds,

$$j_1\le L_1=\big\lceil\kappa_C\,\epsilon^{-2}\big\rceil .$$

The constants are kept exactly as printed. The first bound counts gradient evaluations and the second counts all iterations, which is the number of function evaluations.

Milestones

1. Theorem 2.1: under (2.10) and $\sigma_k\le\bar\sigma$, the bound $|\mathcal U_j|\le\lceil-(\log\gamma_3/\log\gamma_1)|\mathcal S_j|+\log(\bar\sigma/\sigma_0)/\log\gamma_1\rceil$, and its variant (2.14) when $\sigma_k\ge\sigma_{\min}$.
2. Theorem 2.2: a model decrease of $\alpha\epsilon^p$ on a set $\mathcal S_o$ of successful iterations gives $|\mathcal S_o|\le\lceil(f(x_0)-f_{\rm low})\epsilon^{-p}/(\eta_1\alpha)\rceil$.
3. Lemma 3.1: the Cauchy decrease (3.3) and the step bound (3.4).
4. Lemma 3.2: $\sqrt{\sigma_k\|g_k\|}>\kappa_{HB}$ makes iteration $k$ very successful.
5. Lemma 3.3: $\sigma_k\le\max(\sigma_0,\gamma_2\kappa_{HB}^2/\epsilon)$ while $\|g_k\|>\epsilon$.
6. (3.20), (3.21), (3.22) of the proof of Corollary 3.4: the decrease $\alpha_C\epsilon^2$, the first half of the corollary, and the bound on $|\mathcal U_{j_1}|$.

Significance

The corollary establishes that the ARC framework, whatever step it takes beyond the Cauchy point and whatever symmetric $B_k$ it uses, is never worse than steepest descent in evaluation count. It is the baseline against which Part II measures its second-order variant ARC(S), whose $O(\epsilon^{-3/2})$ bound is the subject of a separate mission in this series. Theorems 2.1 and 2.2 are generic: they convert any per-iteration model decrease and any bound on $\sigma_k$ into iteration counts, and are reused verbatim for ARC(S).

The results are proved in the paper. No machine-checked proof of any of them exists on Prove2Me or, to our knowledge, elsewhere. The work here is to formalize the known proofs: the Cauchy-point analysis of Part I (quoted, not reproved, in Part II), the Taylor-remainder estimate of Lemma 3.2, and the counting arguments. Formalizing also checks the printed statements: two of them need a small correction (see Formalization scope).

Difficulty

Each step is elementary, but the statements are about a nondeterministic algorithm: $s_k$ and $\sigma_{k+1}$ are choices, so every bound must hold for all admissible choices, not for one convenient run. The constants are explicit, and the ceilings interact: the printed proof of (3.17) adds the ceilings of (3.15) and (3.22), which does not by itself give $\lceil\kappa_C\epsilon^{-2}\rceil$; the bound must be derived from the unrounded estimates. Lemma 3.1 i) requires a careful one-dimensional analysis of $\alpha\mapsto m_k(-\alpha g_k)$ with an indefinite $B_k$. The ratio $\rho_k$ is a quotient, and its denominator must be shown positive before any comparison with $\eta_1$, $\eta_2$ is meaningful.

Formalization scope

The space is EuclideanSpace ℝ (Fin n); $g$ is Mathlib's gradient f; $B_k$ is a continuous linear operator with IsSelfAdjoint, and $\|B_k\|$ is the operator norm. A run is a predicate IsARCRun on the sequences $x,s,\sigma,B$; the Cauchy condition is stated as $m_k(s_k)\le m_k(-\alpha g_k)$ for all $\alpha\ge0$, which is equivalent to comparing with the Cauchy point and avoids defining an argmin. The run is infinite; a run that the paper would stop at $g_k=0$ extends trivially, and every statement only concerns iterations with $\|g_k\|>\epsilon$. Lean's x / 0 = 0 gives $\rho_k=0$ (unsuccessful) when $f(x_k)=m_k(s_k)$; Theorem 2.2 assumes (2.6), $m_k(s_k)<f(x_k)$, up to its horizon, and §3's results need nothing extra because $g_k\neq0$ makes the denominator positive.

"$j_1\le L$" is stated as: every $j$ with $\|g_k\|>\epsilon$ for all $k\le j$ satisfies $j\le L$ (and similarly for $|\mathcal S_j|$). This asserts that $j_1$ is finite without presupposing it. Statements with $j\le\infty$ are given for every finite $j$.

Two corrections to the printed text are built in. In Theorem 2.1 the bound $\sigma_k\le\bar\sigma$ is assumed for $k\le j+1$: as printed ($k\le j$) the theorem fails for $j=0$, iteration $0$ unsuccessful, $\bar\sigma=\sigma_0$. In AF.4 the set $X$ must contain the trial points $x_k+s_k$ as well as the iterates, because Lemma 3.2 applies the Lipschitz bound on the segment $[x_k,x_k+s_k]$.

A trivializing formalization is ruled out: the goal quantifies over every admissible step and weight update rather than one particular choice, keeps (2.10) out of the first conclusion, and keeps every constant as printed rather than replacing it by an existential.

A complete development needs the one-dimensional cubic analysis behind Lemma 3.1, a mean-value bound for $C^1$ functions along a segment, and finite counting over Finset.range. The generic counting results (Theorems 2.1, 2.2) are reusable for every ARC variant. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part II: worst-case function- and derivative-evaluation complexity, Math. Program. 130(2):295–319, 2011 (preprint rev. 15 Sep 2009 used here). https://doi.org/10.1007/s10107-009-0337-y
• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Math. Program. 127(2):245–295, 2011. https://doi.org/10.1007/s10107-009-0286-5
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108(1):177–205, 2006. https://doi.org/10.1007/s10107-006-0706-8
• S. Gratton, A. Sartenaer, Ph. L. Toint, Recursive trust-region methods for multiscale nonlinear optimization, SIAM J. Optim. 19(1):414–444, 2008. https://doi.org/10.1137/050644043
• Yu. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9