Optimization

Motivation

In two-echelon distribution goods travel from a central depot to intermediate facilities, called satellites, on large first-level vehicles, and from the satellites to customers on smaller second-level vehicles. City logistics schemes that keep heavy trucks out of urban centres are the standard example. The two-echelon capacitated vehicle routing problem (2E-CVRP) asks for the cheapest set of routes on both levels that serves every customer while respecting vehicle, fleet and satellite capacities.

Exact methods for problems of this kind are branch-and-bound or enumeration schemes whose speed depends on the quality of the lower bounds they use. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) built their exact algorithm on a Lagrangean-type relaxation $RF$ of a set-partitioning formulation $F$, rather than on the LP relaxation $LF$ of that formulation. Their Theorem 2 is the justification for that design choice: the best bound $RF$ can deliver is never weaker than $z(LF)$, and can be strictly stronger. This mission formalizes that comparison.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric travel cost $d_{uv}$ (in which the fixed vehicle costs $U_1, U_2$ have already been folded into the depot–satellite and satellite–customer entries), positive integer demands $q_i$, capacities $Q_1 > Q_2 > 0$ for first- and second-level vehicles, a bound $m^1$ on first-level vehicles, $m_k$ second-level vehicles at satellite $k$, a global bound $m^2 \le \sum_k m_k$ on second-level vehicles, a capacity $B_k$ and a unit handling cost $H_k$ for each satellite.

A first-level route $r \in \mathcal M$ leaves the depot, visits a set $R_r$ of satellites and returns; its cost $g_r$ is the cost of that closed walk. A second-level route $l \in \mathcal R_k$ leaves satellite $k$, visits a set $R_{kl}$ of customers and returns; its load is $w_{kl} = \sum_{i \in R_{kl}} q_i \le Q_2$, $a_{ikl}$ counts its visits to customer $i$, and its cost $c_{kl}$ is its closed-walk cost plus $H_k w_{kl}$.

Formulation $F$ uses binaries $x_{kl}$ (route $l$ of satellite $k$ is used), binaries $y_r$, and nonnegative integers $q_{kr}$ (quantity route $r$ delivers to satellite $k \in R_r$). It minimizes $\sum c_{kl}x_{kl} + \sum g_r y_r$ subject to: each customer is covered exactly once (2); at most $m_k$ routes at satellite $k$ (3) and $m^2$ overall (4); the load delivered from satellite $k$ is at most $B_k$ (5); at most $m^1$ first-level routes (6); what first-level routes bring to satellite $k$ equals what its second-level routes carry (7); and $\sum_{k \in R_r} q_{kr} \le Q_1 y_r$ (8).

The LP relaxation $LF$ replaces the integrality of $x, y, q$ by $0 \le x, y \le 1$, $q \ge 0$. Its value is $z(LF)$, equal to $+\infty$ when $LF$ is infeasible.

The relaxation $RF(\beta, \lambda, \mu)$ relaxes (2)–(4) with penalties $\lambda \in \mathbb{R}^{N_C}$, $\mu_k \le 0$ and $\mu_0 \le 0$, and replaces the second-level routes by marginal routing costs $\beta_{ik}$ that must satisfy, for every route $l \in \mathcal R_k$,

$$\sum_{i} a_{ikl}\beta_{ik} \le c_{kl} - \sum_i a_{ikl}\lambda_i - \mu_k - \mu_0. \tag{12}$$

Its variables are binaries $\xi_{ik}$ (customer $i$ is supplied from satellite $k$), $y_r$ and $q_{kr}$; it minimizes

$$\sum_{k,i}\beta_{ik}\xi_{ik} + \sum_r g_r y_r + \sum_i \lambda_i + \sum_k m_k\mu_k + m^2\mu_0$$

subject to single assignment of each customer, flow balance $\sum_{r \in \mathcal M_k} q_{kr} = \sum_i q_i\xi_{ik}$, satellite capacity $\sum_i q_i \xi_{ik} \le B_k$, and (6), (8). A choice $(\beta,\lambda,\mu,\mu_0)$ with $\mu, \mu_0 \le 0$ and (12) is admissible.

Formalization targets

Goal: Theorem 2

$$\max_{\beta,\lambda,\mu}\, z(RF(\beta,\lambda,\mu)) \ \ge\ z(LF), \quad\text{and the inequality can be strict.}$$

Formally: (1) for every instance and route families whose $LF$ is feasible, some admissible $(\beta,\lambda,\mu,\mu_0)$ satisfies $z(LF) \le z(RF(\beta,\lambda,\mu))$; (2) some instance, route families and admissible choice give $z(LF) < z(RF(\beta,\lambda,\mu)) < +\infty$.

Milestones

• §3, remark on $LF$: if every $g_r > 0$, every optimal $LF$ solution has $y_r = (\sum_{k \in R_r} q_{kr})/Q_1$.
• Theorem 2, first clause: the bound, for every instance with $LF$ feasible.
• Theorem 2, second clause: the strict instance.

Significance

Theorem 2 places the relaxation $RF$ in the hierarchy of bounds for the 2E-CVRP. The remark on $LF$ explains its weakness: in the LP relaxation each first-level route is paid for only in proportion to the load it carries, so $z(LF)$ degrades as first-level routing costs grow. $RF$ keeps $y_r$ binary and therefore pays the full cost of every first-level route used, while the second-level routing is priced through $\beta$. The theorem guarantees that optimizing over penalties never loses against the LP bound, which is what makes the bounds LD1 and the further relaxation $\overline{RF}$ of the paper worth computing.

The paper's proof is in its electronic companion and is not reproduced in the article. A formal proof makes the comparison checkable, and fixes the exact conditions under which it holds: the remark on $LF$ needs positive first-level route costs, and the "max" in Theorem 2 is attained only when $LF$ is feasible. Neither part is formalized elsewhere. Linear programming strong duality is available on the platform as LinearOptimization.lp_strong_duality (Bertsimas and Tsitsiklis, Theorem 4.4, Proved); a related but different statement is LinearOptimization.lagrangean_dual_eq_lp_over_hull (Theorem 11.4 there), which concerns the Lagrangean dual of a generic integer program rather than $RF$.

Difficulty

$RF$ is not the Lagrangean dual of $F$ in the textbook sense: it changes the variables (customer-to-satellite assignments $\xi$ instead of routes $x$), keeps the assignment constraints, and couples the multipliers through the inequalities (12). So the general fact that a Lagrangean dual is at least the LP bound does not apply directly; one must construct, from the data of $LF$, an admissible $\beta$ that is compatible with the flow-balance and capacity constraints of $RF$. For the strict clause, the instance must satisfy every structural requirement of the model (positive demands, $Q_2 < Q_1$, route loads at most $Q_2$, $m^2 \le \sum_k m_k$), and $RF$ must be feasible, so that the gap is a genuine gap between finite bounds.

Formalization scope

Satellites and customers are Fin ns and Fin nc (0-based). The travel cost is an arbitrary symmetric real matrix; the triangle inequality is not assumed. Demands are positive integers. Route families $\mathcal M$, $\mathcal R$ are arbitrary finite families of nonempty elementary routes (repetitions allowed), with costs computed from $d$ along the closed walk, so the statements cover the paper's families of all routes as a special case. Binary variables are Bool, integer quantities ℕ, $LF$ variables real. Optimal values are infima over the feasible set in EReal, $+\infty$ for an infeasible problem; there is no junk value $0$.

Part 1 of the goal assumes $LF$ feasible: when $LF$ is infeasible the printed relation would read "$\sup = +\infty$", which is not attained by any single choice of penalties. Part 2 requires $z(RF) < +\infty$, which rules out the trivial witness of an instance with $RF$ infeasible; admissibility includes $\mu, \mu_0 \le 0$, without which the supremum is $+\infty$ for trivial reasons.

The definitions (instance, route systems, $F$, $LF$, (12), $RF$) are shared in shape with the two companion missions of this series and are intended for consolidation. Proofs of the bound will need finite-dimensional LP duality; contributions that connect $LF$ to the platform's general-form LP and its strong duality theorem are welcome.

Selected references

• R. Baldacci, A. Mingozzi, R. Roberti, R. Wolfler Calvo, An Exact Algorithm for the Two-Echelon Capacitated Vehicle Routing Problem, Operations Research 61(2), 298–314, 2013. https://doi.org/10.1287/opre.1120.1153
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 4.4, strong duality; Theorem 11.4, Lagrangean duality).

Motivation

Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, $\ell_1$-regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.

Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same $O(n/k)$ expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.

Setting

The space $\mathbb R^N$ is split into $n\ge1$ blocks, $\mathbb R^N=\mathbb R^{n_1}\times\cdots\times\mathbb R^{n_n}$ with $N=\sum_in_i$ and every $n_i\ge1$. A point $x$ is the family of its blocks $x^{(i)}\in\mathbb R^{n_i}$, and $U_ih$ is the point whose $i$-th block is $h$ and whose other blocks are zero. Each block carries a Euclidean norm $\|h\|_{(i)}^2=\langle B_ih,h\rangle$ with $B_i\succ0$ (3.4).

The objective $f:\mathbb R^N\to\mathbb R$ is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing $f'_i(x)=U_i^T\nabla f(x)$ for the $i$-th block of the gradient, there are constants $L_i>0$ with

$$\|f'_i(x+U_ih)-f'_i(x)\|^*_{(i)}\le L_i\|h\|_{(i)}\quad\text{for all }x,\ i,\ h .$$

The weighted norm is $\|x\|_1^2=\sum_iL_i\|x^{(i)}\|_{(i)}^2$ (3.5). The function $f$ is strongly convex in $\|\cdot\|_1$ with constant $\sigma>0$ if $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\sigma2\|y-x\|_1^2$ for all $x,y$ (3.1).

The problem is (4.1), $\min_{x\in Q}f(x)$ with $Q=Q_1\times\cdots\times Q_n$ and each $Q_i\subseteq\mathbb R^{n_i}$ nonempty, closed and convex. Its optimal value is $f^*$, attained at an optimal solution $x_*\in Q$. The constrained coordinate update (4.2) is

$$u^{(i)}(x)=\arg\min_{u\in Q_i}\Big[\langle f'_i(x),u-x^{(i)}\rangle+\tfrac{L_i}2\|u-x^{(i)}\|_{(i)}^2\Big],\qquad V_i(x)=x+U_i\big(u^{(i)}(x)-x^{(i)}\big).$$

The uniform coordinate descent method UCDM$(x_0)$ (4.5) draws $i_k$ uniformly from $\{1,\dots,n\}$ and sets $x_{k+1}=V_{i_k}(x_k)$. Its expected objective is $\varphi_k=\mathbb E f(x_k)$, the expectation over $i_0,\dots,i_{k-1}$. The level-set radius $R_1(x_0)$ is the largest $\|\cdot\|_1$-distance between a feasible $x$ with $f(x)\le f(x_0)$ and an optimal solution.

Formalization targets

Goal: Theorem 5

For every $k\ge0$,

$$\varphi_k-f^*\le\frac n{n+k}\Big[\tfrac12R_1^2(x_0)+f(x_0)-f^*\Big],$$

and, if $f$ is strongly convex in $\|\cdot\|_1$ with constant $\sigma>0$,

$$\varphi_k-f^*\le\Big(1-\frac{2\sigma}{n(1+\sigma)}\Big)^k\Big(\tfrac12R_1^2(x_0)+f(x_0)-f^*\Big).\qquad(4.6)$$

Milestones

1. (4.3): the optimality condition $\langle f'_i(x)+L_iB_i(u^{(i)}(x)-x^{(i)}),u-u^{(i)}(x)\rangle\ge0$ for all $u\in Q_i$.
2. (4.4): for feasible $x$, $f(x)-f(V_i(x))\ge\frac{L_i}2\|u^{(i)}(x)-x^{(i)}\|_{(i)}^2$.
3. (4.7): with $r_k=\|x_k-x_*\|_1$, $\ \mathbb E_{i_k}\big(\frac12r_{k+1}^2+f(x_{k+1})-f^*\big)\le\frac12r_k^2+f(x_k)-f^*+\frac1n\langle\nabla f(x_k),x_*-x_k\rangle$.
4. Footnote 2: under (2.2), the strong convexity constant satisfies $\sigma\le1$.

Significance

The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each $Q_i$, the cost of the unconstrained one: $O(n/\epsilon)$ block steps for accuracy $\epsilon$, and $O\big(\frac n\sigma\log\frac1\epsilon\big)$ under strong convexity. The method needs no knowledge of $\sigma$; the same iteration attains whichever rate applies. The Lyapunov function $\frac12\|x-x_*\|_1^2+f(x)-f^*$ of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.

Difficulty

The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease $f(x)-f(T_i(x))\ge(\|f'_i(x)\|^*_{(i)})^2/(2L_i)$ of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion $\varphi_k-\varphi_{k+1}\ge(\varphi_k-f^*)^2/C$ is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming $\sigma\le1$, which is where footnote 2 enters.

Formalization scope

$\mathbb R^N$ is the dependent product Blocks E $=\prod_{i:\mathrm{Fin}\,n}E_i$, each $E_i$ a finite-dimensional real inner product space whose inner product is the paper's $\langle B_i\cdot,\cdot\rangle$. Indices are 0-based. The dual norm is the operator norm of linear functionals, and $f'_i(x)$ is the Fréchet derivative of $f$ composed with the block inclusion. Random draws are explicit index sequences, so $\varphi_k$ is the finite average of $f(x_k)$ over all $n^k$ sequences of draws; no measure theory is involved.

Explicit choices where the paper is silent:

• $n\ge1$, every block nontrivial ($n_i\ge1$), and $L_i>0$ are hypotheses.
• Every $Q_i$ is nonempty, and $x_0\in Q$. The paper leaves both implicit; without $x_0\in Q$ the iterates are infeasible and $\varphi_k-f^*$ can be negative.
• $u^{(i)}(x)$ is a choice among the minimizers of the block subproblem. Under the hypotheses the minimizer exists and is unique, so the choice is the paper's update.
• $R_1(x_0)$ is never computed: the theorem takes any $R$ with $\|x-x_*\|_1\le R$ for every feasible $x$ with $f(x)\le f(x_0)$ and every optimal solution $x_*$. This is equivalent to the paper's bound when $R_1(x_0)$ is finite and avoids the default value of a supremum. The level set is taken inside $Q$, the reading of the p. 7 definition for problem (4.1).
• $f^*$ is the constrained optimum $f(x_*)$ for an optimal solution $x_*\in Q$, not an unconstrained minimum.
• Strong convexity is (3.1) on all of $\mathbb R^N$ in $\|\cdot\|_1$. The linear rate does not assume $\sigma\le1$; footnote 2 derives it.
• Printed typos are corrected in the Lean: $U_i^T$ in (4.2) is $U_i$; $u^i$ in (4.3) is $u^{(i)}$.

A formalization in which the update is an arbitrary point of $Q_i$ or an unprojected gradient step, the draws are not uniform, or $f^*$ is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.

Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. https://core.ac.uk/download/6430808.pdf
• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2) (2012), 341–362. https://doi.org/10.1137/100802001
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Section 2.1, cited in the proof). https://doi.org/10.1007/978-1-4419-8853-9
• P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming 117 (2009), 387–423. https://doi.org/10.1007/s10107-007-0170-0

Motivation

Coordinate descent methods update one block of variables at a time. For problems with millions or billions of variables, where even one full gradient is too expensive to compute or store, a step that touches a single block can be orders of magnitude cheaper than a full gradient step. Nesterov's Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362, doi:10.1137/100802001) gave the first global complexity bounds for randomized coordinate descent on smooth convex functions: choosing the block at random makes the expected progress per step comparable to that of a full gradient step divided by the number of blocks.

Section 5 of the paper asks whether the multistep acceleration of the full gradient method (Nesterov 1983) carries over to the randomized coordinate setting, and answers it with the accelerated coordinate descent method ACDM. This mission formalizes that answer: Theorem 6, the $O(n^2/k^2)$ expected rate of ACDM, together with the lemmas of its proof.

Timeline. Nesterov (1983) introduced the accelerated full-gradient method with rate $O(1/k^2)$. Nesterov (CORE DP 2010/2; SIAM J. Optim. 2012) proved the $O(n/k)$ rate of random block coordinate descent and the $O(n^2/k^2)$ rate of its accelerated variant ACDM. Later work (Lee and Sidford 2013; Fercoq and Richtárik 2015, arXiv:1312.5799; Allen-Zhu, Qu, Richtárik and Yuan 2016, arXiv:1512.09103) made the accelerated scheme efficient per iteration and sharpened its constants.

Setting

The space is $\mathbb R^N=\mathbb R^{n_1}\times\cdots\times\mathbb R^{n_n}$, split into $n\ge1$ blocks. A point $x$ has blocks $x^{(i)}\in\mathbb R^{n_i}$, and $U_ih$ is the point whose $i$-th block is $h$ and whose other blocks vanish. Each block carries a Euclidean norm $\|h\|_{(i)}^2=\langle B_ih,h\rangle$ with $B_i\succ0$.

The objective $f:\mathbb R^N\to\mathbb R$ is convex and differentiable, and has a coordinate-wise Lipschitz gradient: the partial gradient $f'_i(x)=U_i^T\nabla f(x)$ satisfies $\|f'_i(x+U_ih)-f'_i(x)\|^*_{(i)}\le L_i\|h\|_{(i)}$ with constants $L_i>0$. The method weighs blocks by these constants through the norm

$$\|x\|_1^2=\sum_{i=1}^nL_i\|x^{(i)}\|_{(i)}^2 .$$

The function $f$ is strongly convex in this norm with parameter $\sigma\ge0$ if $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\sigma2\|y-x\|_1^2$ for all $x,y$; $\sigma=0$ is plain convexity. A point $x^*$ minimizes $f$, and $f^*=f(x^*)$.

The optimal coordinate step is $T_i(x)=x-\frac1{L_i}U_if'_i(x)^\#$, where $s^\#$ maximizes $\langle s,x\rangle-\frac12\|x\|^2$. ACDM$(x_0)$ keeps two sequences $x_k,v_k$ with $v_0=x_0$ and deterministic scalars $a_0=1/n$, $b_0=2$. At step $k$ it computes $\gamma_k\ge1/n$ from $\gamma_k^2-\gamma_k/n=(1-\gamma_k\sigma/n)a_k^2/b_k^2$, sets $\alpha_k=\frac{n-\gamma_k\sigma}{\gamma_k(n^2-\sigma)}$ and $\beta_k=1-\gamma_k\sigma/n$, forms $y_k=\alpha_kv_k+(1-\alpha_k)x_k$, draws a block $i_k$ uniformly at random, and updates

$$x_{k+1}=T_{i_k}(y_k),\qquad v_{k+1}=\beta_kv_k+(1-\beta_k)y_k-\frac{\gamma_k}{L_{i_k}}U_{i_k}f'_{i_k}(y_k)^\#,$$

$b_{k+1}=b_k/\sqrt{\beta_k}$, $a_{k+1}=\gamma_kb_{k+1}$. The quantity $\phi_k=\mathbb E\,f(x_k)$ is the expectation over the first $k$ draws.

Formalization targets

Goal: Theorem 6, (5.3)

For every $k\ge0$, with $D=2\|x_0-x^*\|_1^2+\frac1{n^2}(f(x_0)-f^*)$,

$$\phi_k-f^*\le\Big(\frac n{k+1}\Big)^2D,$$

and, when $\sigma>0$,

$$\phi_k-f^*\le\sigma D\Big[\Big(1+\tfrac{\sqrt\sigma}{2n}\Big)^{k+1}-\Big(1-\tfrac{\sqrt\sigma}{2n}\Big)^{k+1}\Big]^{-2}\le\Big(\frac n{k+1}\Big)^2D .$$

Milestones

1. (5.1), well-definedness: $\gamma_k\ge1/n$ is the unique such root, $0<\alpha_k,\beta_k\le1$.
2. (5.2): $\gamma_k^2-\gamma_k/n=\beta_ka_k^2/b_k^2=(\beta_k\gamma_k/n)(1-\alpha_k)/\alpha_k$.
3. The potential inequality: $2a_{k+1}^2(\phi_{k+1}-f^*)+b_{k+1}^2\mathbb E r_{k+1}^2\le2a_k^2(\phi_k-f^*)+b_k^2\mathbb E r_k^2$, $r_k=\|v_k-x^*\|_1$.
4. (5.4) $b_{k+1}\ge b_k+\frac\sigma{2n}a_k$ and (5.5) $a_{k+1}\ge a_k+\frac1{2n}b_k$.
5. $a_k\ge\frac1{\sqrt\sigma}[Q_1^{k+1}-Q_2^{k+1}]$ and $b_k\ge Q_1^{k+1}+Q_2^{k+1}$, $Q_{1,2}=1\pm\frac{\sqrt\sigma}{2n}$.
6. $(1+t)^k-(1-t)^k\ge2kt$ for $t\ge0$, hence $Q_1^{k+1}-Q_2^{k+1}\ge\frac{k+1}n\sqrt\sigma$.

Significance

The result. Theorem 6 shows that randomized coordinate descent can be accelerated: the expected error falls as $n^2/k^2$ instead of the $n/k$ of the plain method, so after $k=n\cdot m$ iterations (about $m$ full-gradient equivalents) the error is $O(1/m^2)$, the rate of the accelerated full-gradient method. For $\sigma>0$ the same scheme converges linearly with a ratio governed by $\sqrt\sigma/n$ rather than $\sigma/n$. This is the starting point of the accelerated randomized coordinate methods (APPROX, NU-ACDM, accelerated proximal coordinate gradient) now used in large-scale machine learning.

Formalizing it. The theorem is proved in the paper; to our knowledge neither it nor any accelerated coordinate method has a machine-checked proof. The Lean development pins down a scheme whose correctness rests on a delicate parameter identity and on several conventions left implicit in the text (the range of $\sigma$, the reading of (5.3) at $\sigma=0$).

Difficulty

The plain coordinate descent analysis tracks $f(x_k)$ alone and fails to accelerate: one coordinate step gains only $\frac1n$ of a full gradient step, and a momentum term built naively from coordinate steps does not keep the expected progress. The accelerated proof needs a potential mixing the function gap with a squared distance $\|v_k-x^*\|_1^2$, weighted by the deterministic sequences $a_k^2$ and $b_k^2$; the weights must make the cross terms in $\|y_k-x^*\|_1^2$ and $f(y_k)$ cancel exactly after taking the expectation in the drawn block, which is what the coupled choice of $\gamma_k,\alpha_k,\beta_k$ achieves. The second difficulty is quantitative: the growth of $a_k$ follows from coupled recursions for $a_k$ and $b_k$, not from a closed form.

Formalization scope

• Space. $\mathbb R^N$ is Blocks E, the dependent product of finite-dimensional real inner-product spaces E i over Fin n (indices $0,\dots,n-1$); $B_i$ is absorbed into the inner product of E i. The dual norm is the operator norm of E i →L[ℝ] ℝ.
• Randomness. Draws are explicit sequences Fin k → Fin n; $\phi_k$ and $\mathbb E r_k^2$ are finite averages over all $n^k$ sequences with weight $n^{-k}$. No measure theory is needed.
• $s^\#$. Theorems hold for every selection satisfying (1.8), not a fixed choice.
• Explicit hypotheses. The paper's standing assumptions become hypotheses: $n\ge1$; $L_i>0$; $f$ differentiable with (2.2); a minimizer $x^*$ exists. The convexity parameter $\sigma$ is any valid one (not necessarily the largest) with $0\le\sigma<n^2$. The paper states $\sigma\ge0$ only; $\sigma<n^2$ is needed because $\alpha_k$ divides by $n^2-\sigma$, and by footnote 2 ($\sigma\le1$) it excludes only $n=1$, $\sigma=1$.
• The case $\sigma=0$ of (5.3). The paper's middle expression is $0\cdot[0]^{-2}$ at $\sigma=0$, read as a limit. Lean would evaluate it to $0$, which would turn the statement into the false claim $\phi_k\le f^*$; the chain is therefore stated for $\sigma>0$, and the outer bound $(n/(k+1))^2D$ separately for all $\sigma\ge0$. Likewise the bound on $a_k$ involving $1/\sqrt\sigma$ is stated for $\sigma>0$.
• The coefficient $\gamma_k$ is the closed-form larger root of the quadratic in step 1; a milestone certifies it is the unique root $\ge1/n$.
• No trivialization. A formalization in which $\sigma=0$ is allowed in the middle bound, or in which $\phi_k$ is computed with a draw distribution other than uniform, or in which the coefficients depend on the draws, is not this theorem.
• Corrections of the printed text. The update of $v_{k+1}$ prints $f'_i(y_k)^\#$; the index is $i_k$. The middle term $b_k^2r_k^2$ of the potential inequality, written after the expectation in $\xi_{k-1}$, is $b_k^2\mathbb E r_k^2$.
• Reusable parts. The block encoding (Blocks, partialGrad, CoordLipschitz, coordStep, wnorm, expect) is shared verbatim with the other missions of this series. The coefficient lemmas (5.2), (5.4), (5.5) and the growth bounds are pure real analysis and welcome as standalone contributions; so is a Lean proof of the block descent inequality (2.3)–(2.4) for Euclidean blocks, which the potential inequality needs.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. Journal version: SIAM J. Optim. 22(2) (2012) 341–362. https://doi.org/10.1137/100802001
• Yu. Nesterov, A method for solving the convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27 (1983) 372–376.
• Y. T. Lee, A. Sidford, Efficient accelerated coordinate descent methods and faster algorithms for solving linear systems, FOCS 2013. https://arxiv.org/abs/1305.1922
• O. Fercoq, P. Richtárik, Accelerated, parallel and proximal coordinate descent, SIAM J. Optim. 25(4) (2015) 1997–2023. https://arxiv.org/abs/1312.5799
• Z. Allen-Zhu, Z. Qu, P. Richtárik, Y. Yuan, Even faster accelerated coordinate descent using non-uniform sampling, ICML 2016. https://arxiv.org/abs/1512.09103
• S. Bubeck, Convex optimization: algorithms and complexity, Found. Trends Mach. Learn. 8 (2015), §3.7 (Nesterov's accelerated gradient descent, formalized on Prove2Me as ConvexOptAlg.NesterovSmooth.theorem_3_19). https://arxiv.org/abs/1405.4980

Motivation

Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem

$$(\mathrm P)\qquad \min\ f(x)\quad\text{s.t.}\quad \|x\|_0\le s,$$

where $f$ is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and its solutions are not characterized by the classical KKT theory.

Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) introduced a hierarchy of necessary optimality conditions for (P) and matched each condition with an algorithm whose limit points satisfy it. Iterative hard thresholding (Blumensath and Davies 2008) reaches $L$-stationarity for $L>L(f)$; the greedy sparse-simplex method reaches coordinate-wise minimality, but each of its iterations calls up to $O(sn)$ one-dimensional minimizations. This mission formalizes the paper's compromise between the two: the partial sparse-simplex method, which examines only two candidate moves per saturated iteration, and whose limit points are $L_2(f)$-stationary.

Setting

Vectors live in $\mathbb R^n$ with the Euclidean norm; $e_i$ is the $i$-th unit vector. For $x\in\mathbb R^n$:

• the $\ell_0$ norm $\|x\|_0$ is the number of nonzero components of $x$;
• the support is $I_1(x)=\{i: x_i\ne0\}$, and $I_0(x)=\{i: x_i=0\}$ is its complement;
• $C_s=\{x:\|x\|_0\le s\}$ is the feasible set, for an integer $0<s<n$;
• $M_s(x)$ is the $s$-th largest of $|x_1|,\dots,|x_n|$, counted with multiplicity; $M_s(x)=0$ exactly when $\|x\|_0<s$.

The objective $f$ is continuously differentiable and bounded below (Assumption 1, standing throughout the paper). Assumption 2 asks that $\nabla f$ be Lipschitz with some constant $L(f)$. A constant $L_2$ satisfies the local Lipschitz condition (2.15) if for every pair $i\ne j$, every $x$ and every $d$ supported in $\{i,j\}$,

$$\big\|\nabla_{i,j}f(x)-\nabla_{i,j}f(x+d)\big\|\le L_2\|d\|,\qquad \nabla_{i,j}f(x)=(\nabla_if(x),\nabla_jf(x)).$$

The paper's local Lipschitz constant $L_2(f)=\max_{i\ne j}L_{i,j}(f)$ satisfies it, and $L_2(f)\le L(f)$.

The projection $P_{C_s}(y)$ is the set of points of $C_s$ nearest to $y$. For $L>0$, a point $x^*$ is an $L$-stationary point (Definition 2.3) if

$$x^*\in C_s\quad\text{and}\quad x^*\in P_{C_s}\!\Big(x^*-\tfrac1L\nabla f(x^*)\Big).\qquad[\mathrm{NC}_L]$$

The partial sparse-simplex method (p. 25) starts at $x^0\in C_s$. If $\|x^k\|_0<s$, it moves to the best point $x^k+te_i$ over all $i$ and $t$ if that strictly decreases $f$, and stops otherwise. If $\|x^k\|_0=s$, it compares two candidates and takes the better one, preferring the second on ties:

1. re-optimize one support coordinate: $x^k+T^1_ke_{i^1_k}$, the best point $x^k+te_i$ over $i\in I_1(x^k)$, $t\in\mathbb R$;
2. swap: zero out the support coordinate $m_k$ of smallest absolute value and optimize along the off-support coordinate $i^2_k$ with the largest $|\nabla_if(x^k)|$, giving $x^k-x^k_{m_k}e_{m_k}+T^2_ke_{i^2_k}$.

Formalization targets

Goal: Theorem 3.4

Under Assumption 2, with $L_2>0$ satisfying (2.15), every accumulation point $x^*$ of a sequence generated by the partial sparse-simplex method satisfies

$$x^*\in P_{C_s}\!\Big(x^*-\frac1{L_2}\nabla f(x^*)\Big),$$

that is, $x^*$ is an $L_2(f)$-stationary point.

Milestones

1. Lemma 2.6 (Local Descent Lemma). For every $d$ supported in two coordinates,

$$f(x+d)\le f(x)+\nabla f(x)^Td+\frac{L_2}{2}\|d\|^2 .$$

2. (4.10). If $\|x^k\|_0=s$, then $f(x^k)-f(x^{k+1})\ge\frac1{2L_2}\max_{i\in I_1(x^k)}(\nabla_if(x^k))^2$.
3. (4.13). If $\|x^k\|_0=s$, then

$$f(x^k)-f(x^{k+1})\ge M_s(x^k)\Big[\max_{i\in I_0(x^k)}|\nabla_if(x^k)|-L_2M_s(x^k)\Big]+x^k_{m_k}\nabla_{m_k}f(x^k).$$

4. Lemma 4.1. $f(x^k)-f(x^{k+1})\ge\frac1{2L_2}\max_i(\nabla_if(x^k))^2$ when $\|x^k\|_0<s$ (4.6), and $f(x^k)-f(x^{k+1})\ge A(x^k)$ when $\|x^k\|_0=s$ (4.7), with

$$A(x)=\max\Big\{\frac1{2L_2}\max_{i\in I_1(x)}(\nabla_if(x))^2,\ M_s(x)\Big[\max_{i\in I_0(x)}|\nabla_if(x)|-\max_{i\in I_1(x)}|\nabla_if(x)|-L_2M_s(x)\Big]\Big\}.$$

5. Lemma 2.2. For $L>0$, $[\mathrm{NC}_L]$ holds iff $\|x\|_0\le s$, $|\nabla_if(x)|\le LM_s(x)$ on $I_0(x)$ and $\nabla_if(x)=0$ on $I_1(x)$.

Significance

The theorem shows that a cheap index-selection rule does not cost optimality strength relative to iterative hard thresholding: every limit point satisfies $[\mathrm{NC}_{L_2(f)}]$, and since $L_2(f)\le L(f)<L$, this is a stronger necessary condition than the $[\mathrm{NC}_L]$ guaranteed by IHT with stepsize $1/L$. In the paper's numerical comparison (Example 3.3 contd., Table 3) the method performs much better than IHT and only slightly worse than the greedy method, at a fraction of the greedy method's cost per iteration. The decrease estimates of Lemma 4.1 are the quantitative content: they turn each iteration into a lower bound on the objective decrease in terms of the violation of $L_2$-stationarity.

The results are proved in the paper; to our knowledge none is machine-checked. This mission produces a formal model of the method (with its selection rules as inequality predicates, so every run is covered), the local descent lemma for two-sparse directions, and a checked proof of Theorem 3.4. The printed proof of the case $\|x^*\|_0<s$ contains two gaps (see Difficulty); a formal proof settles the argument.

Difficulty

The decrease estimates follow from the local descent lemma applied at well-chosen trial points, but passing to the limit is delicate. When $\|x^*\|_0=s$, the supports of the subsequence eventually coincide with $I_1(x^*)$ and $A$ becomes continuous there; when $\|x^*\|_0<s$, the iterates along the subsequence may still have $s$ nonzeros, and $A(x^k)\to0$ does not by itself force $\nabla f(x^*)=0$, because $M_s(x^k)\to0$ kills the second term of $A$. The swap move optimizes along a single off-support coordinate $i^2_k$, chosen by the derivative at $x^k$ and not at the shifted point $x^k-x^k_{m_k}e_{m_k}$ where the optimization happens. The printed display (4.19) claims the bound for the maximum over all of $I_0(x^k)$ at the shifted point, which the argument does not give, and the final display takes a minimum of two bounds that each hold on only one class of indices. Theorem 3.4 itself is not affected, but a complete proof cannot follow those two displays as printed.

Formalization scope

Lean works in EuclideanSpace ℝ (Fin n) (indices $0,\dots,n-1$), with $f$ of class $C^1$ and $\nabla f$ = gradient f. Conventions fixed by the formalization:

• $0<s<n$, so $I_1(x)$ and $I_0(x)$ are nonempty whenever $\|x\|_0=s$.
• $L_2$ is any constant with $0<L_2$ satisfying (2.15), read with $d$ supported in $\{i,j\}$; the paper's $L_2(f)$ is one such constant. Positivity is required because (4.6), (4.10) and $A$ divide by $L_2$.
• Assumption 1 and Assumption 2 (LipschitzWith Lf (gradient f)) are hypotheses.
• The method's minimizers and maximizers are inequality predicates, not computed values; the theorem holds for every run. A STOP is modelled by $x^{k+1}=x^k$.
• Two misprints of the printed box (arXiv v1) are corrected: "for every $i\in I_1(x^*)$" is read as $I_1(x^k)$, and "$i^1_k\in\operatorname{argmax}\{f_i\}$" as argmin, as the prose on p. 24 and the proof of (4.10) require. With the literal argmax the goal is not what the paper proves.
• Maxima over index sets are suprema in $\mathbb R_{\ge0}$, equal to the maxima on nonempty sets.
• "Accumulation point" is MapClusterPt xstar atTop x.
• Theorem numbers and page numbers are those of the arXiv v1 source (arXiv:1203.4580v1), which is the file this mission cites; the published SIAM version is typeset differently.

The run predicate is satisfiable and does not force a STOP: on $n=2$, $s=1$, $f(x)=(x_1-1)^2+x_2^2$, the constant sequence at $(1,0)$ is a run. The conclusion is the projection condition itself, not the coordinate form (2.5), so it cannot be met by an empty or degenerate reading of stationarity.

Reusable parts: the local descent lemma for two-sparse directions, Lemma 2.2 (the coordinate characterization of $[\mathrm{NC}_L]$, shared with the IHT mission of this series), and the order statistic $M_s$. Contributions of proofs for any milestone are welcome, as is the companion result Lemma 3.3 (limit points are BF vectors without Assumption 2).

Selected references

• A. Beck, Y. C. Eldar, Sparsity Constrained Nonlinear Optimization: Optimality Conditions and Algorithms, SIAM J. Optim. 23(3), 2013. https://doi.org/10.1137/120869778 (source used: arXiv:1203.4580v1, https://arxiv.org/abs/1203.4580v1)
• T. Blumensath, M. E. Davies, Iterative thresholding for sparse approximations, J. Fourier Anal. Appl. 14(5), 2008. https://doi.org/10.1007/s00041-008-9035-z

Motivation

Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a nonlinear search space: a sphere, a Stiefel or Grassmann manifold, a space of curves modulo reparametrization. Projecting iterates of a Euclidean method back onto the constraint set loses the geometry, so one designs methods that move along the manifold itself. Riemannian line-search methods do this by replacing the update $x_{k+1}=x_k+\alpha_kp_k$ with $x_{k+1}=R_{x_k}(\alpha_kp_k)$ for a retraction $R$, and by carrying old search directions to the new tangent space with a transport.

Nonlinear conjugate gradient (NCG) methods are a natural candidate on manifolds: they need only first derivatives and store one previous direction. In the Euclidean case, Al-Baali showed in 1985 that the Fletcher–Reeves method with strong Wolfe step lengths and $c_2<\tfrac12$ satisfies $\liminf_k\|\nabla f(x_k)\|=0$ (doi:10.1093/imanum/5.1.121); Nocedal and Wright give the standard textbook proof (Lemma 5.6 and Theorem 5.7 in Numerical Optimization). Ring and Wirth (doi:10.1137/11082885X, SIAM J. Optim. 2012) transfer this analysis to Riemannian manifolds, possibly infinite-dimensional, which is the setting of their application to shape spaces. The mission formalizes that transfer.

Setting

$\mathcal M$ is a smooth manifold modelled on a real Hilbert space $E$, with a Riemannian metric $g_x$ on each tangent space $T_x\mathcal M$ and norm $\|\cdot\|_x$. For $f:\mathcal M\to\mathbb R$, $\mathrm Df(x)$ is its differential, a continuous linear functional on $T_x\mathcal M$ with dual norm $\|\mathrm Df(x)\|_x$, and the gradient $\nabla f(x)\in T_x\mathcal M$ is its Riesz representative, $g_x(\nabla f(x),v)=\mathrm Df(x)v$.

A retraction is a family of smooth maps $R_x:T_x\mathcal M\to\mathcal M$ with $R_x(0)=x$ and $\mathrm DR_x(0)=\mathrm{id}$. Its transport is $T^{R_x}_{x,R_x(v)}=\mathrm DR_x(v):T_x\mathcal M\to T_{R_x(v)}\mathcal M$.

A run of Algorithm 1 consists of points $x_k$, directions $p_k\in T_{x_k}\mathcal M$ and steps $\alpha_k>0$ with $x_{k+1}=R_{x_k}(\alpha_kp_k)$. With $0<c_1<c_2<1$, the Wolfe conditions at $(x,p,\alpha)$ are

$$f(R_x(\alpha p))\le f(x)+c_1\alpha\,\mathrm Df(x)p,\tag{1a}$$ $$\mathrm Df(R_x(\alpha p))\,T^{R_x}_{x,R_x(\alpha p)}p\ge c_2\,\mathrm Df(x)p,\tag{1b}$$

and the strong Wolfe conditions replace (1b) by

$$\bigl|\mathrm Df(R_x(\alpha p))\,T^{R_x}_{x,R_x(\alpha p)}p\bigr|\le -c_2\,\mathrm Df(x)p.\tag{2}$$

The angle $\theta_k$ between $p_k$ and $-\nabla f(x_k)$ is given by $\cos\theta_k=-\mathrm Df(x_k)p_k/(\|\mathrm Df(x_k)\|_{x_k}\|p_k\|_{x_k})$.

The Fletcher–Reeves direction is

$$p_0=-\nabla f(x_0),\qquad p_{k+1}=-\nabla f(x_{k+1})+\beta_{k+1}\,T^{R_{x_k}}_{x_k,x_{k+1}}p_k,\qquad \beta_{k+1}=\frac{\|\mathrm Df(x_{k+1})\|_{x_{k+1}}^2}{\|\mathrm Df(x_k)\|_{x_k}^2}.$$

Formalization targets

Goal: Proposition 15

For a non-terminating Fletcher–Reeves run with strong Wolfe steps and $0<c_1<c_2<\tfrac12$, if the transport is non-expansive on the search directions, $\|T^{R_{x_k}}_{x_k,x_{k+1}}p_k\|_{x_{k+1}}\le\|p_k\|_{x_k}$, $f$ is bounded below, and the pull-backs $f\circ R_{x_k}$ are Lipschitz continuously differentiable on $\mathrm{span}\{p_k\}$ with a uniform constant, then

$$\liminf_{k\to\infty}\|\mathrm Df(x_k)\|_{x_k}=0.$$

Milestones

1. Theorem 2 (Zoutendijk). For Wolfe steps along descent directions, $f$ bounded below and the line-Lipschitz condition, $\sum_k\cos^2\theta_k\|\mathrm Df(x_k)\|_{x_k}^2<\infty$.
2. Lemma 14. For a Fletcher–Reeves run with strong Wolfe steps and $c_2<\tfrac12$,

$$-\frac1{1-c_2}\le\frac{\mathrm Df(x_k)p_k}{\|\mathrm Df(x_k)\|_{x_k}^2}\le\frac{2c_2-1}{1-c_2}.$$

3. The angle sandwich (proof of Proposition 15): $\frac{1-2c_2}{1-c_2}\frac{\|\mathrm Df(x_k)\|}{\|p_k\|}\le\cos\theta_k\le\frac1{1-c_2}\frac{\|\mathrm Df(x_k)\|}{\|p_k\|}$.
4. Square summability: $\sum_k\|\mathrm Df(x_k)\|^4/\|p_k\|^2<\infty$.
5. Growth bound: $\|p_k\|^2\le\frac{1+c_2}{1-c_2}\|\mathrm Df(x_k)\|^4\sum_{j=0}^k\|\mathrm Df(x_j)\|^{-2}$.

Significance

Proposition 15 guarantees that Riemannian Fletcher–Reeves, with any retraction whose transport does not enlarge the search direction, cannot stall at a positive gradient level: some subsequence of the gradient norms tends to zero. Together with strict convexity in the sense of the paper's Proposition 4 this gives convergence of the iterates to the minimizer, and it justifies the use of the method on the shape spaces of the paper's §4. The hypothesis on the transport is the only new ingredient compared with the Euclidean theorem, and the paper's Remark 7 notes that convergence can no longer be guaranteed without it.

The result is proved in the paper. As far as is known, neither Zoutendijk's theorem on a manifold nor the Fletcher–Reeves convergence theorem has a machine-checked proof; Euclidean versions of both appear elsewhere on the platform, but the Riemannian statements, with retraction, transport and tangent-space-dependent norms, are new. The mission produces the line-search interface on a Riemannian manifold (retraction, transport, Wolfe conditions) in a form reusable by other Riemannian methods.

Difficulty

Each search direction is built from a vector in a different tangent space. The transported direction $\mathrm DR_{x_k}(\alpha_kp_k)p_k$ lives in $T_{R_{x_k}(\alpha_kp_k)}\mathcal M$, and only the step equation identifies it with a vector of $T_{x_{k+1}}\mathcal M$; norms, inner products and differentials all depend on the base point, so every Euclidean manipulation has to be carried through that identification. Zoutendijk's theorem has to connect two different descriptions of the same step: the curvature condition (1b) is stated with the differential of $f$ at the new point applied to the transported direction, while the Lipschitz hypothesis concerns the one-variable pull-back $t\mapsto f(R_{x_k}(tp_k))$. They agree only because the transport is the derivative of the retraction, and the agreement is a chain rule for manifold derivatives, which has to be established in Mathlib's mfderiv framework for maps out of a tangent space. The growth bound cannot use $\|T p\|=\|p\|$; it needs the non-expansiveness hypothesis exactly where the Euclidean argument uses the identity.

Formalization scope

The manifold is a Mathlib manifold modelled on a real Hilbert space E, with Mathlib's RiemannianBundle on its tangent spaces; tangent-space norms and inner products are the Riemannian ones and $\mathrm Df(x)$ is mfderiv. Geodesic completeness, separability, the distance and the Levi-Civita connection, standing assumptions of the paper, are not used by any statement and are dropped. The gradient is given as a field with its Riesz property. One retraction family is used for every step (the paper allows a different retraction at each step), the steps are positive, and indices start at $0$.

The following readings are explicit:

• The Fletcher–Reeves run is assumed never to stop ($\mathrm Df(x_k)\neq0$), since $\beta_{k+1}$ divides by $\|\mathrm Df(x_k)\|^2$.
• Descent of the Fletcher–Reeves directions is not assumed; it follows from Lemma 14.
• "Lipschitz continuously differentiable on $\mathrm{span}\{p_k\}$ with constant $L$" is read for $h_k(t)=f(R_{x_k}(tp_k))$: $h_k$ is differentiable and $|h_k'(s)-h_k'(t)|\le L|s-t|\,\|p_k\|^2$, with $L>0$.
• The hypotheses of Theorem 2 (lower bound on $f$, line-Lipschitz condition), which the proof of Proposition 15 invokes but whose statement does not list, are added to Proposition 15 and to the square-summability milestone.
• The $\liminf$ is stated as: for every $\varepsilon>0$ and $N$ there is $k\ge N$ with $\|\mathrm Df(x_k)\|<\varepsilon$; sums are stated with Summable.

The transport in the conclusion and in the Fletcher–Reeves update is the derivative of the retraction, not an arbitrary linear map; with an arbitrary map, condition (1b) would no longer be a statement about the pull-back $f\circ R_{x_k}$, and Zoutendijk's theorem would fail. A run predicate that no sequence satisfies would make the goal vacuous; the one-dimensional run $\mathcal M=\mathbb R$, $R_x(v)=x+v$, $f(x)=x^2/2$, $c_1=0.1$, $c_2=0.45$, $x_{k+1}=0.4x_k$ satisfies every hypothesis.

The paper's other main result, R-linear convergence of Riemannian BFGS (Proposition 10), is a separate mission, and its superlinear-rate results (Propositions 5, 7, 8, 12, Corollary 13), which require parallel transport and the exponential map, are out of scope. Contributions welcome: proofs of the chain rule identities for retractions (reusable for any Riemannian line search), of Zoutendijk's theorem, and of the milestones in order.

Selected references

• W. Ring, B. Wirth, Optimization Methods on Riemannian Manifolds and Their Application to Shape Space, SIAM J. Optim. 22(2), 596–627, 2012. https://doi.org/10.1137/11082885X
• M. Al-Baali, Descent property and global convergence of the Fletcher–Reeves method with inexact line search, IMA J. Numer. Anal. 5(1), 121–124, 1985. https://doi.org/10.1093/imanum/5.1.121
• J. Nocedal, S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006 (Lemma 5.6, Theorem 5.7). https://doi.org/10.1007/978-0-387-40065-5
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244