Convex Optimization

Motivation

Regularized loss minimization over linear predictors is the training problem behind support vector machines, logistic regression, ridge regression and their many variants. Given examples $x_1,\dots,x_n\in\mathbb R^d$, one minimizes an average of convex losses of the predictions $w^\top x_i$ plus a quadratic penalty. Dual coordinate ascent (DCA) solves the Fenchel dual of this problem by optimizing one dual variable at a time; it has been the workhorse of linear SVM solvers such as LIBLINEAR (Hsieh et al., ICML 2008). Before Shalev-Shwartz and Zhang's work, the available analyses of DCA either gave linear rates with constants depending on unknown problem quantities or did not control the duality gap, which is the quantity a practitioner can actually monitor as a stopping criterion.

Shalev-Shwartz and Zhang (2013) analysed stochastic dual coordinate ascent (SDCA), where the coordinate is picked uniformly at random, and proved explicit bounds on the expected duality gap. For Lipschitz losses (hinge loss, absolute loss) the bound is $\tilde O(n+L^2/(\lambda\epsilon))$ iterations, which matches stochastic gradient descent when the accuracy is low and improves on it when $n$ is small compared with $L^2/(\lambda\epsilon)$. This mission formalizes that result, Theorem 1 of the paper, together with the lemmas of its proof.

Timeline. Hsieh, Chang, Lin, Keerthi and Sundararajan (2008) proposed dual coordinate descent for linear SVMs and proved linear convergence with an unspecified constant. Shalev-Shwartz and Zhang (arXiv 2012, JMLR 2013) gave the first explicit duality-gap rates for SDCA, for Lipschitz and for smooth losses. Proximal and accelerated variants followed (Shalev-Shwartz and Zhang, Math. Program. 2016).

Setting

Fix $n\ge1$ examples $x_1,\dots,x_n\in\mathbb R^d$ (Euclidean norm), convex losses $\phi_1,\dots,\phi_n:\mathbb R\to\mathbb R$ and a regularization parameter $\lambda>0$. The primal problem (1) is to minimize

$$P(w)=\frac1n\sum_{i=1}^n\phi_i(w^\top x_i)+\frac\lambda2\|w\|^2 .$$

The convex conjugate of a scalar function is $\phi^*(u)=\sup_z(zu-\phi(z))\in(-\infty,+\infty]$. The dual problem (2) is to maximize, over $\alpha\in\mathbb R^n$,

$$D(\alpha)=\frac1n\sum_{i=1}^n-\phi_i^*(-\alpha_i)-\frac\lambda2\|w(\alpha)\|^2,\qquad w(\alpha)=\frac1{\lambda n}\sum_{i=1}^n\alpha_ix_i .$$

Weak duality gives $D(\alpha)\le P(w)$ for all $\alpha,w$, so the duality gap $P(w(\alpha))-D(\alpha)$ bounds the primal sub-optimality of $w(\alpha)$.

A loss $\phi$ is $L$-Lipschitz if $|\phi(a)-\phi(b)|\le L|a-b|$ for all $a,b$. The paper's standing assumptions are $\|x_i\|\le1$, $\phi_i\ge0$ and $\phi_i(0)\le1$.

Procedure SDCA starts from $\alpha^{(0)}=0$. At iteration $t=1,\dots,T$ it picks a coordinate $i$ uniformly at random, chooses $\Delta\alpha_i$ maximizing

$$-\phi_i^*\bigl(-(\alpha_i^{(t-1)}+\Delta\alpha_i)\bigr)-\frac{\lambda n}{2}\bigl\|w^{(t-1)}+(\lambda n)^{-1}\Delta\alpha_i x_i\bigr\|^2,$$

and sets $\alpha^{(t)}=\alpha^{(t-1)}+\Delta\alpha_ie_i$ and $w^{(t)}=w(\alpha^{(t)})$. The averaging option outputs $\bar\alpha=\frac1{T-T_0}\sum_{t=T_0+1}^T\alpha^{(t-1)}$ and $\bar w=w(\bar\alpha)$. Let $\alpha^*$ maximize $D$ and write $\epsilon_D^{(t)}=D(\alpha^*)-D(\alpha^{(t)})$ for the dual sub-optimality.

Formalization targets

Goal: Theorem 1 (p. 5)

For convex $L$-Lipschitz losses under the standing assumptions, if $\epsilon_P>0$ and

$$T\ \ge\ T_0+n+\frac{4L^2}{\lambda\epsilon_P}\ \ge\ \max\bigl(0,\lceil n\log(0.5\lambda nL^{-2})\rceil\bigr)+n+\frac{20L^2}{\lambda\epsilon_P},$$

then

$$\mathbb E\bigl[P(\bar w)-D(\bar\alpha)\bigr]\le\epsilon_P,\qquad\text{and}\qquad\mathbb E\bigl[D(\alpha^*)-D(\alpha^{(t)})\bigr]\le\epsilon_P/2\ \text{ for all }t\ge T_0 .$$

The constants $4$ and $20$ are the paper's.

Milestones

In the order the proof uses them: the one-coordinate increase (10); the identity $P(w(\alpha))-D(\alpha)=\frac1n\sum_i(\phi_i(w^\top x_i)+\phi_i^*(-\alpha_i)+\alpha_iw^\top x_i)$; Lemma 1 (expected dual increase at least $\frac sn$ times the gap minus $(\frac sn)^2\frac{G}{2\lambda}$); Lemma 2 ($D(\alpha)\le P(w^*)\le P(0)\le1$, $D(0)\ge0$); Lemma 3 ($\phi^*=+\infty$ outside $[-L,L]$); Lemma 4 ($G\le4L^2$); the recursion after (13); the rate (14), $\mathbb E[\epsilon_D^{(t)}]\le\frac{2G}{\lambda(2n+t-t_0)}$; and the averaged duality-gap bound of p. 16.

Significance

Theorem 1 makes the duality gap of SDCA a certified stopping criterion with an explicit iteration count. Because the gap upper-bounds the primal sub-optimality, it also gives a primal guarantee for the averaged output $\bar w$. It covers non-smooth losses, the hinge loss in particular, where linear rates are not available. The analysis pattern, a lower bound on the expected dual increase by the duality gap (Lemma 1) followed by a recursion for the dual sub-optimality, was reused in the analyses of proximal, accelerated and mini-batch dual methods.

The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. The mission produces a formal account of the primal–dual pair of regularized loss minimization with extended-real conjugates, a formal SDCA run with uniformly random coordinates, and the complete chain of lemmas. Lemma 1 is stated with a general strong-convexity modulus $\gamma\ge0$, as in the paper, so it serves the smooth-loss analysis as well.

Difficulty

The obvious first idea is to treat SDCA as stochastic coordinate ascent on a concave function and import a standard rate. That fails: $D$ is neither smooth nor strongly concave for Lipschitz losses, and its domain $\{\alpha:\phi_i^*(-\alpha_i)<\infty\}$ is a box, so the per-coordinate progress cannot be bounded by a gradient norm. The argument instead compares the exact coordinate maximizer with an explicit interpolation towards a sub-gradient, which needs the conjugate's value at a sub-gradient (Fenchel–Young equality) and its infinite values outside $[-L,L]$.

The rate (14) is not a plain geometric recursion. It needs a burn-in phase and then an induction with a step size $s$ that changes with $t$, and the duality gap of the output has to be recovered from the dual progress by Jensen's inequality over the averaged iterates. Everything happens in expectation over the coordinate sequence, while the dual values have to be kept finite along every run.

Formalization scope

Lean conventions:

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), examples and losses are indexed by Fin n, and $w^\top x$ is inner ℝ w x.
• The conjugate is an EReal supremum, and $D$ is EReal-valued. Real values of $D$ are used only where the same statement asserts that they are finite.
• The coordinate step is a free map Δ : (Fin n → ℝ) → Fin n → ℝ constrained by an arg-max predicate (IsSDCAStep). Any maximizer is admissible, and one exists for convex real losses.
• The run is a function of the coordinate sequence js : Fin T → Fin n, started at $\alpha^{(0)}=0$, with $w^{(t)}=w(\alpha^{(t)})$.
• Expectations are uniform averages over coordinate sequences (SAGA.Convex.expectIdx, a published definition).
• $\alpha^*$ is any maximizer of $D$, and $w^*$ any minimizer of $P$.
• The constant $G=\max_tG^{(t)}$ of the proof is pinned to its bound $4L^2$. Theorem 1's burn-in $\max(0,\lceil n\log(0.5\lambda nL^{-2})\rceil)$ is exactly the value of $t_0$ obtained with $G=4L^2$ and $\epsilon_D^{(0)}\le1$.
• Lemmas 1 and 4 are stated for a fixed dual-feasible state. The paper's history-averaged form follows from this.

A real-valued conjugate, which returns $0$ where the supremum is infinite, or an unconstrained step map would make the statements false or vacuous. The EReal conjugate and the arg-max predicate rule both out.

Infrastructure needed: Fenchel–Young for scalar convex functions, the existence of sub-gradients of convex real functions and their bound by the Lipschitz constant, Jensen's inequality for the convex $P$ and the concave $D$, and the algebra of uniform averages over $\{1,\dots,n\}^t$. The conjugate and sub-differential definitions and the duality-gap identity can be reused beyond this mission. Proofs of any milestone are welcome, as are lemmas on EReal sums that keep the finiteness bookkeeping short.

Selected references

• S. Shalev-Shwartz and T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, arXiv:1209.1873v2, 2013; Journal of Machine Learning Research 14:567–599, 2013. https://arxiv.org/abs/1209.1873
• C.-J. Hsieh, K.-W. Chang, C.-J. Lin, S. S. Keerthi and S. Sundararajan, A Dual Coordinate Descent Method for Large-scale Linear SVM, ICML 2008. https://doi.org/10.1145/1390156.1390208
• S. Shalev-Shwartz and T. Zhang, Accelerated Proximal Stochastic Dual Coordinate Ascent for Regularized Loss Minimization, Mathematical Programming 155:105–145, 2016. https://doi.org/10.1007/s10107-014-0839-0

Motivation

Many equilibrium problems in operations research, such as networked Cournot competition, power markets and communication networks, are stochastic Nash games: each player minimizes an expected cost $f_i(x_i,x_{-i})=\mathbb E[\psi_i(x_i,x_{-i};\xi)]$ that depends on the rivals' strategies and on a random vector $\xi$ whose law is accessible only through samples. Best-response schemes, in which every player in turn solves its own optimization problem given the others' latest strategies, are the natural distributed method for such games. In the stochastic setting no player can compute an exact best response, because evaluating $f_i$ requires the expectation itself. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in which each best response is approximated by a finite number of stochastic gradient steps, and they ask how many sampled gradients each player needs to reach an approximate equilibrium.

The deterministic theory of proximal best responses, including the contraction matrix $\Gamma$ used here, is due to Facchinei and Pang (Nash equilibria: the variational approach, 2009, §12.6; reference [19] of the paper). The present mission covers the paper's first scheme, the synchronous one, in which all players update simultaneously.

Setting

There are $N$ players. Player $i$ chooses $x_i$ from a closed, compact, convex, nonempty set $X_i\subseteq\mathbb R^{n_i}$; a profile is $x=(x_1,\dots,x_N)\in X=\prod_iX_i$, and $(z,y_{-i})$ is the profile $y$ with its $i$-th block replaced by $z$. A Nash equilibrium is a profile $x^*\in X$ such that every $x^*_i$ minimizes $f_i(\cdot,x^*_{-i})$ over $X_i$.

Assumption 1 asks that each $f_i$ be convex in $x_i$ and twice continuously differentiable near $X$, that the sampled gradients $\nabla_{x_i}\psi_i(x;\xi)$ be unbiased for $\nabla_{x_i}f_i(x)$, and that $\mathbb E\|\nabla_{x_i}\psi_i(x;\xi)\|^2\le M_i^2$. For $\mu>0$ the proximal best response is

$$\hat x_i(y)=\operatorname*{argmin}_{x_i\in X_i}\Big[f_i(x_i,y_{-i})+\tfrac\mu2\|x_i-y_i\|^2\Big].$$

The $N\times N$ matrix $\Gamma$ has entries $\gamma_{ii}=\mu/(\mu+\zeta_{i,\min})$ and $\gamma_{ij}=\zeta_{ij,\max}/(\mu+\zeta_{i,\min})$, where $\zeta_{i,\min}$ is the least eigenvalue of $\nabla^2_{x_i}f_i$ over $X$ and $\zeta_{ij,\max}$ the largest spectral norm of the mixed block $\nabla^2_{x_ix_j}f_i$ over $X$. Assumption 2 is $a:=\|\Gamma\|<1$ (spectral norm).

Algorithm 1 starts from a deterministic $x_0\in X$. At major iteration $k$ every player computes $x_{i,k+1}\in X_i$ with $\mathbb E[\|x_{i,k+1}-\hat x_i(x_k)\|^2\mid\mathcal F_k]\le\alpha_{i,k}^2$, by running $j_{i,k}$ projected stochastic gradient steps

$$z_{i,t+1}=\Pi_{X_i}\Big[z_{i,t}-\tfrac{1}{\mu(t+1)}\big(\nabla_{x_i}\psi_i(z_{i,t},x_{-i,k};\xi^t_{i,k})+\mu(z_{i,t}-x_{i,k})\big)\Big],\qquad z_{i,1}=x_{i,k},$$

and setting $x_{i,k+1}=z_{i,j_{i,k}}$. A random profile $x$ is an $\epsilon$-NE$_2$ if $\mathbb E\big[(\sum_i\|x_i-x^*_i\|^2)^{1/2}\big]\le\epsilon$.

Formalization targets

Goal: Theorem 1(a)

With $\alpha_{i,k}=\eta^{k+1}$, $\eta\in(0,1)$, $\|x_{i,0}-x^*_i\|\le C$, $c=\max\{a,\eta\}$, $q\in(c,1)$, $D=1/\ln((q/c)^e)$, $Q_i=2M_i^2/\mu^2+2D_{X_i}^2$ and $j_{i,k}=\lceil Q_i/\eta^{2(k+1)}\rceil$, the iterate $x_K$ after $K=\lceil\ln(\sqrt N(C+D)/\epsilon)/\ln(1/q)\rceil$ major iterations is an $\epsilon$-NE$_2$, and player $i$ uses at most

$$\ell_i(\eta)=\frac{Q_i}{\eta^4\ln(1/\eta^2)}\left(\frac{\sqrt N(C+D)}{\epsilon}\right)^{\frac{\ln(1/\eta^2)}{\ln(1/q)}}+\left\lceil\frac{\ln(\sqrt N(C+D)/\epsilon)}{\ln(1/q)}\right\rceil$$

projected stochastic gradient steps. The goal fixes the paper's explicit expression, not its $O(\cdot)$ summary.

Milestones

1. (5): $\|\hat x_i(y')-\hat x_i(y)\|\le\sum_j\gamma_{ij}\|y'_j-y_j\|$ for $y,y'\in X$.
2. (9): the same in the Euclidean norm of block distances, with factor $a$.
3. A Nash equilibrium is a fixed point: $\hat x(x^*)=x^*$.
4. Lemma 2: $zc^z\le Dq^z$ for $z\ge0$, $0<c<q<1$, $D\ge1/(e\ln(q/c))$.
5. (20): $u_{k+1}\le au_k+\sqrt N\max_i\alpha_{i,k}$, where $u_k$ is the mean Euclidean norm of block errors.
6. Proposition 4: $u_k\le\sqrt N(C+D)q^k$.
7. Lemma 3: $\mathbb E[\|z_{i,t}-\hat x_i(x_k)\|^2\mid\mathcal F_k]\le Q_i/(t+1)$.
8. (30): $\sum_{k=1}^K\beta^k\le\int_1^{K+1}\beta^xdx\le\beta^{K+1}/\ln\beta$ for $\beta>1$.

Significance

Theorem 1(a) shows that the synchronous inexact scheme keeps the linear rate of the exact best-response iteration, with factor arbitrarily close to $\max\{\|\Gamma\|,\eta\}$, and turns it into a sample complexity explicit in $\epsilon$, in the number of players and in the game's constants. Choosing $\eta=\|\Gamma\|$ gives a bound of order $(\sqrt N/\epsilon)^{2+\delta}$ for any $\delta>0$ (Theorem 1(b)), close to the $O(1/\epsilon^2)$ of a single stochastic convex program; the dependence on $N$ is mild, which matters for games with many players. The same building blocks (the contraction (5), Lemma 2, Lemma 3 and (30)) are reused by the randomized and asynchronous schemes of the same paper.

The result is proved in the paper; it has not been machine-checked. A formalization adds a verified proof of the complexity bound together with fully explicit hypotheses: several conditions that the paper leaves implicit or states imprecisely (listed under Formalization scope) are made exact, and the Lean statement records which version of each is used.

Difficulty

The arithmetic of Theorem 1(a) from Proposition 4, Lemma 3 and (30) is routine. The weight lies elsewhere. The contraction (5) is quoted from Facchinei–Pang and not proved in the paper; it needs the variational optimality conditions of the two proximal problems and a mean-value argument along a segment of $X$ for the partial gradient, which mixes the Hessian blocks $\nabla^2_{x_i}f_i$ and $\nabla^2_{x_ix_j}f_i$. Lemma 3 is a conditional-expectation argument about a stochastic approximation recursion: the iterate $z_{i,t}$ must be shown measurable for the nested $\sigma$-fields generated by the samples, and the conditional unbiasedness and moment hypotheses must be combined with the tower property and the projection's nonexpansiveness. Proposition 4 then needs conditional Jensen to pass from (8) to the Euclidean norm of block errors.

Formalization scope

Players are Fin N, player $i$'s space is EuclideanSpace ℝ (Fin (n i)), profiles are dependent functions, and $(z,y_{-i})$ is Function.update y i z. The Euclidean norm of the vector of block distances is written out (blockDist), since Mathlib's norm on profiles is the sup norm; $\|\Gamma\|$ is the operator norm of Matrix.toEuclideanCLM Γ. $\zeta_{i,\min}$ and $\zeta_{ij,\max}$ are the infimum and supremum of Rayleigh-type quotients of the second derivative over $X$ and unit vectors. The proximal BR is any map minimizing the proximal objective on $X$ (unique there), and $\Pi_{X_i}$ is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. The $\sigma$-fields $\mathcal F_k$ and $\sigma\{\mathcal F_k,\xi^{[t-1]}_{i,k}\}$ are generated by the samples. Every expectation carries an integrability hypothesis.

Statement repairs, each recorded in the item's Formalization Note:

• the initial point is deterministic, as Algorithm 1 states, so $\mathbb E\|x_{i,0}-x^*_i\|\le C$ reads $\|x_{i,0}-x^*_i\|\le C$ (the proof's $u_0\le\sqrt NC$ needs this);
• Assumption 1(b) is twice continuous differentiability in the whole profile, which (4) needs for the mixed blocks, and convexity on an open set containing $X_i$;
• in Lemma 3, $\psi_i$ is read as $\nabla_{x_i}\psi_i$, and the second hypothesis is the bound $\mathbb E[\|\nabla_{x_i}\psi_i\|^2\mid\cdot]\le M_i^2$ that the proof uses (the printed equality would force zero sampling noise);
• $0<\epsilon<\sqrt N(C+D)$, without which the ceiling in (27) can be non-positive;
• $D=1/(e\ln(q/c))$, the reading of $\ln((q/c)^e)$ confirmed by Lemma 2's proof.

The goal is not trivialized by deterministic gradients: the sampled gradients are random, constrained only by conditional unbiasedness and a conditional second-moment bound, the proximal BR is tied to $f_i$ by its argmin property, $x^*$ must be a Nash equilibrium, and the norms are Euclidean. A deterministic instance ($N=1$, $f_1(x)=\|x\|^2$ on a ball, exact gradients) satisfies every hypothesis jointly.

Needed infrastructure: optimality conditions for constrained strongly convex minimization, the mean-value inequality for partial gradients of $C^2$ functions on convex sets, conditional expectation of vector-valued functions with the tower property and conditional Jensen, and the nonexpansiveness of Euclidean projection. The contraction (5) and Lemma 3 are reusable beyond this mission. Proofs of any milestone are welcome.

Selected references

• J. Lei, U. V. Shanbhag, J.-S. Pang, S. Sen, On Synchronous, Asynchronous, and Randomized Best-Response Schemes for Stochastic Nash Games, arXiv:1704.04578v2, 2018; published in Mathematics of Operations Research, 2020. https://arxiv.org/abs/1704.04578v2
• F. Facchinei, J.-S. Pang, Nash equilibria: the variational approach, in Convex Optimization in Signal Processing and Communications, Cambridge University Press, 2009 (reference [19] of arXiv:1704.04578v2).
• B. T. Polyak, Introduction to Optimization, Optimization Software, 1987 (reference [38] of the paper).

Motivation

Interior-point methods for conic optimization are best understood on symmetric cones: the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices. On these cones the barrier functions are self-scaled, and Nesterov and Todd showed that every primal-dual pair $(x, s)$ then has a unique scaling point $w$ with $s = F''(w)x$ and $F'(x) = F''(w)F_*'(s)$. The resulting primal-dual algorithms, implemented in solvers such as SeDuMi and MOSEK, combine long steps with good worst-case complexity.

Many models in statistics, geometric programming, entropy maximization and logistic regression need the exponential cone, which is not symmetric. Dahl and Andersen (Math. Program. 194, 2022) designed the primal-dual algorithm behind MOSEK's exponential-cone support. To explain why they cannot simply transplant the Nesterov–Todd construction, they use a property that sits between "self-scaled" and "arbitrary": negative curvature of the barrier. Barriers of symmetric cones have it; a barrier is self-scaled if and only if both it and its conjugate have it (Nesterov–Tunçel, 2016); and barriers with negative curvature still admit a unique scaling point satisfying one secant equation. Dahl and Andersen observe in §5 that the exponential-cone barrier lies outside this class, by an explicit witness. This mission formalizes that observation and the derivative formulas of their Appendix A it rests on.

Timeline:

• 1997–1998: Nesterov and Todd introduce self-scaled barriers and their primal-dual scalings (Math. Oper. Res. 22; SIAM J. Optim. 8).
• 2001: Tunçel generalizes primal-dual scalings to arbitrary convex cones (Found. Comput. Math. 1).
• 2009: Chares studies the exponential cone and its 3-self-concordant barrier (thesis, Université catholique de Louvain).
• 2016: Nesterov and Tunçel characterize self-scaled barriers through negative curvature of the barrier and its conjugate.
• 2022: Dahl and Andersen give a primal-dual algorithm for the exponential cone with Tunçel-type scalings, and note that its barrier does not have negative curvature.

Setting

Points of $\mathbb{R}^3$ are written $x = (x_1, x_2, x_3)$. The exponential cone is the closure

$$K_{\exp} = \operatorname{cl}\{x \in \mathbb{R}^3 \mid x_1 \ge x_2 \exp(x_3/x_2),\ x_2 > 0\},$$

whose interior is $\{x \mid x_2 > 0,\ x_1 > x_2\exp(x_3/x_2)\}$. Its standard barrier is

$$F(x) = -\log\bigl(x_2\log(x_1/x_2) - x_3\bigr) - \log x_1 - \log x_2, \qquad (2)$$

defined and smooth on $\operatorname{int}(K_{\exp})$. Appendix A of the paper writes $F = g + h$ with

$$\psi(x) = x_2\log(x_1/x_2) - x_3,\qquad g(x) = -\log\psi(x),\qquad h(x) = -\log x_1 - \log x_2 .$$

For a smooth $F$ on an open set, $F''(x)$ is its Hessian, a symmetric linear map of $\mathbb{R}^n$, and the third directional derivative is the symmetric linear map

$$F'''(x)[u] = \frac{d}{dt}F''(x + tu)\Big|_{t=0}, \qquad F'''(x)[u, v, v] = \langle F'''(x)[u]\,v, v\rangle .$$

A barrier $F$ of a cone $K$ has negative curvature if for all $x \in \operatorname{int}(K)$ and for $u \in K$

$$F'''(x)[u] \preceq 0,$$

where $\preceq$ is the Loewner order: $\langle F'''(x)[u]\,v, v\rangle \le 0$ for every $v$. The direction $u$ ranges over the closed cone $K$, including its boundary.

Formalization targets

Goal: the exponential-cone barrier does not have negative curvature

$$\neg\Bigl(\forall x \in \operatorname{int}(K_{\exp}),\ \forall u \in K_{\exp},\ \forall v \in \mathbb{R}^3:\ \langle F'''(x)[u]\,v, v\rangle \le 0\Bigr).$$

The goal asserts only the qualitative failure, so it does not depend on the particular witness.

Milestones

1. The witness: $\hat x := (1, e^{-2}, 0) \in \operatorname{int}(K_{\exp})$ and $\hat u := (1, 0, 0) \in K_{\exp}\setminus\operatorname{int}(K_{\exp})$ (§5, p. 356).
2. First-order derivatives (A.1, p. 367): $\psi'(x) = (x_2/x_1,\ \log(x_1/x_2) - 1,\ -1)$, $h'(x) = -(1/x_1, 1/x_2, 0)$, $g'(x) = -\psi'(x)/\psi(x)$, $F' = g' + h'$ on $\operatorname{int}(K_{\exp})$.
3. Second-order derivatives (A.2, p. 367):

$$F''(x) = -\frac{1}{\psi(x)}\Bigl(\psi''(x) - \frac{\psi'(x)\psi'(x)^T}{\psi(x)}\Bigr) + h''(x).$$

4. Third-order directional derivatives (A.3 and (33), p. 368): the closed form of $F'''(x)[u]$ in terms of $\psi$, its derivatives and $h'''(x)[u]$.
5. The matrix at the witness (§5, p. 356):

$$F'''(\hat x)[\hat u] = \begin{bmatrix} -4 & e^2/2 & e^2/2 \\ e^2/2 & 0 & 0 \\ e^2/2 & 0 & -e^4/4 \end{bmatrix}.$$

6. The positive value (§5, p. 356): $F'''(\hat x)[\hat u, \hat v, \hat v] = 4$ for $\hat v := (1, 8e^{-2}, 4e^{-2})$.

Significance

The result. Negative curvature is the property that gives symmetric-cone barriers their long-step Hessian estimates and a unique scaling point with one secant equation. Its failure for the exponential-cone barrier means that none of these consequences can be invoked for the exponential cone. An algorithm for this cone has to obtain its scalings by other means; Dahl and Andersen take them from Tunçel's framework, via the quasi-Newton secant updates of §5. The witness also shows that the failure occurs already for a direction on the boundary of the cone, at an interior point with simple coordinates.

Formalizing it. The claim is proved in the paper by a computation "using the expressions in the appendix", with the details left to the reader. The appendix formulas for the gradient, Hessian and third directional derivative of the exponential-cone barrier are the ones an implementation evaluates, including the higher-order corrector term $-\tfrac12F'''(x)[u, v]$. A machine-checked version certifies these closed forms, including the zero padding of the $2\times2$ "leading parts" in (33), and gives a reusable definition of negative curvature that applies to any cone and barrier. As far as is known, none of these statements has a machine-checked proof.

Difficulty

The obstacle is computational, not conceptual. The barrier is a composition of logarithms with a function $\psi$ that is itself a perspective of the logarithm, so its third derivative is a sum of terms with denominators $\psi(x)^k$, $x_1^k$ and $x_2^k$. Stating it as a derivative of the Hessian map requires showing that the Hessian is differentiable on the open interior, which in turn requires a description of that interior, a set defined as the interior of a closure. The membership claims about $\hat u$ are not definitional either: $\hat u$ lies on the boundary, reached only as a limit of points of the generating set, and its non-interiority needs a neighbourhood argument. Finally, the cone condition on $u$ matters: replacing $u \in K_{\exp}$ by $u \in \mathbb{R}^3$ makes the claim nearly trivial, because $F'''(x)[-u] = -F'''(x)[u]$.

Formalization scope

• Points of $\mathbb{R}^3$ are EuclideanSpace ℝ (Fin 3); the paper's $(x_1, x_2, x_3)$ are (x 0, x 1, x 2), and vectors are written !₂[·, ·, ·].
• $K_{\exp}$ is the closure of the printed set, not its interior or an equivalent description. $F$, $\psi$, $g$, $h$ are defined on all of $\mathbb{R}^3$ by their formulas with Real.log; every statement evaluates them, and their derivatives, only at points of $\operatorname{int}(K_{\exp})$, where all logarithms are the genuine ones. The appendix formulas carry the hypothesis $x \in \operatorname{int}(K_{\exp})$.
• $F''$ is the published SelfScaledIPM.ShortStep.hess (derivative of the gradient), and $F'''(x)[u]$ is fderiv ℝ (hess F) x u. The Loewner order is stated through the quadratic form for every $v$. Matrices act through the standard basis (Matrix.toEuclideanCLM).
• Disclosed deviations from the page: milestone 1 asserts $\hat x \in \operatorname{int}(K_{\exp})$, stronger than the printed $\hat x \in K_{\exp}$ and the form the definition needs. In A.3 the $2\times2$ leading parts $\hat h'''$, $\hat\psi'''$ of (33) are padded with a zero third row and column, and $g''(x)$ is written out by the A.2 formula. Only the first display of A.2 is stated, not the factorization $F''(x) = R(x)R(x)^T$.
• A trivializing formalization would let $u$ range over all of $\mathbb{R}^3$, or read $\preceq 0$ entrywise; both are excluded, and $u$ ranges over the closed cone exactly as in the paper.
• The claim that $F$ is a 3-self-concordant barrier (quoted from Chares) is not part of the mission. The definition of negative curvature applies to any cone in any dimension and can be reused for other barriers. Contributions of calculus lemmas for logarithmic barriers on open sets (differentiability of the Hessian map, interiors of closures of epigraph-type sets) are welcome.

Selected references

• J. Dahl, E. D. Andersen, A primal-dual interior-point algorithm for nonsymmetric exponential-cone optimization, Mathematical Programming 194 (2022), 341–370. https://doi.org/10.1007/s10107-021-01631-4
• Yu. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22 (1997), 1–42. https://doi.org/10.1287/moor.22.1.1
• Yu. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8 (1998), 324–364. https://doi.org/10.1137/S1052623495290209
• L. Tunçel, Generalization of primal-dual interior-point methods to convex optimization problems in conic form, Foundations of Computational Mathematics 1 (2001), 229–254. https://doi.org/10.1007/s102080010008
• Yu. Nesterov, L. Tunçel, Local superlinear convergence of polynomial-time interior-point methods for hyperbolicity cone optimization problems, SIAM Journal on Optimization 26 (2016), 139–170. https://doi.org/10.1137/140978296
• P. R. Chares, Cones and interior-point algorithms for structured convex optimization involving powers and exponentials, PhD thesis, Université catholique de Louvain, 2009.

Motivation

Conic optimization over the exponential cone $K_{\exp}=\operatorname{cl}\{x\in\mathbb R^3: x_1\ge x_2e^{x_3/x_2},\ x_2>0\}$ models entropy, relative entropy, logistic regression, log-sum-exp and geometric programming. Unlike the nonnegative orthant, the second-order cone and the semidefinite cone, the exponential cone is not symmetric (self-scaled), so the Nesterov–Todd primal-dual machinery that makes solvers such as SeDuMi and MOSEK fast does not apply as is. Dahl and Andersen (Math. Program. 194 (2022) 341–370) describe the nonsymmetric-cone algorithm implemented in MOSEK (version 9.2 in the paper's experiments). Its central new ingredient is a corrector for nonsymmetric cones, an analogue of Mehrotra's predictor-corrector that is responsible for much of the practical performance of symmetric-cone solvers. The paper reports that the corrector gives a substantial and consistent reduction in iteration counts across its test sets.

Timeline. Nesterov and Todd (1997, 1998) built primal-dual methods for self-scaled cones. Nesterov, Todd and Ye (1999) and Tunçel (2001) studied primal-dual scalings for general cones, Tunçel proving polynomial complexity of an infeasible method without a corrector under bounded scalings. Skajaa and Ye (2015) gave a homogeneous method for nonsymmetric cones with a Runge–Kutta corrector. Myklebust and Tunçel (2014) analysed BFGS-type scalings. Dahl and Andersen (2022) introduced the third-order corrector studied in this mission.

Setting

Let $A\colon\mathbb R^n\to\mathbb R^m$ be linear with full row rank, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and let $\hat K\subseteq\mathbb R^n$ be a proper cone (pointed, closed, convex, with nonempty interior). A $\hat\vartheta$-logarithmically homogeneous self-concordant barrier (LHSCB) for $\hat K$ is a $C^3$ convex function $\hat F$ on $\operatorname{int}\hat K$ with $|\hat F'''(x)[u,u,u]|\le2(\hat F''(x)[u,u])^{3/2}$ and $\hat F(\tau x)=\hat F(x)-\hat\vartheta\log\tau$. The primal problem minimizes $\langle c,\hat x\rangle$ subject to $A\hat x=b$, $\hat x\in\hat K$; the dual maximizes $\langle b,y\rangle$ subject to $c-A^Ty=\hat s\in\hat K^*$.

The homogeneous model adds $\tau,\kappa\ge0$: $x=(\hat x,\tau)$, $s=(\hat s,\kappa)$, $K=\hat K\times\mathbb R_+$, $F(x)=\hat F(\hat x)-\log\tau$, $\vartheta=\hat\vartheta+1$. With $z=(x,s,y)$, the residual is

$$G(z)=\bigl(A\hat x-b\tau,\ -A^Ty+c\tau-\hat s,\ b^Ty-c^T\hat x-\kappa\bigr),$$

a linear map whose $(y,\hat x,\tau)$-block is skew-symmetric. An iterate has $x\in\operatorname{int}K$, $s\in\operatorname{int}K^*$, and $\mu=\langle x,s\rangle/\vartheta$. The shadow iterates are $\tilde x=-F_*'(s)$ and $\tilde s=-F'(x)$, with $F_*$ the conjugate barrier. A scaling is a nonsingular $W$ with $v=Wx=W^{-T}s$ and $\tilde v=W\tilde x=W^{-T}\tilde s$ (the double secant equations (8)).

The affine direction $\Delta z^a$ solves $G(\Delta z^a)=-G(z)$, $W\Delta x^a+W^{-T}\Delta s^a=-v$ (11). The corrector is $\eta=-\tfrac12F'''(x)[\Delta x^a,(F''(x))^{-1}\Delta s^a]$ (16). For a centering parameter $\gamma>0$, the combined direction $\Delta z$ solves

$$G(\Delta z)=-(1-\gamma)G(z),\qquad W\Delta x+W^{-T}\Delta s=-v+\gamma\mu\tilde v-W^{-T}\eta. \tag{18}$$

Formalization targets

Goal: Lemma 4 (p. 353)

Every solution of (18) satisfies

$$\langle s,\Delta x\rangle+\langle x,\Delta s\rangle=-(1-\gamma)\langle x,s\rangle,\qquad\langle\Delta x,\Delta s\rangle=0,$$

and for all $\alpha\in\mathbb R$

$$G(z+\alpha\Delta z)=(1-\alpha(1-\gamma))G(z),\qquad\langle x+\alpha\Delta x,s+\alpha\Delta s\rangle=(1-\alpha(1-\gamma))\langle x,s\rangle.$$

The goal fixes no constants beyond those of the direction itself. It holds for every solution of (18), not a chosen one.

Milestones

1. §2 homogeneity identities (p. 345): $F'(\tau x)=F'(x)/\tau$, $F''(\tau x)=F''(x)/\tau^2$, $F''(x)x=-F'(x)$, $F'''(x)[x]=-2F''(x)$, $\langle F'(x),x\rangle=-\vartheta$.
2. §2 sum rule for the homogenizing block (pp. 345, 347): $\hat F(\hat x)-\log\tau$ is a $(\hat\vartheta+1)$-LHSCB for $\hat K\times\mathbb R_+$.
3. Lemma 2 (p. 351): the affine direction satisfies $\langle s,\Delta x^a\rangle+\langle x,\Delta s^a\rangle=-\langle x,s\rangle$, $\langle\Delta x^a,\Delta s^a\rangle=0$, and $\langle x+\alpha\Delta x^a,s+\alpha\Delta s^a\rangle=(1-\alpha)\langle x,s\rangle$.
4. Lemma 3 (p. 352): the pure corrector direction ($G(\Delta z^c)=0$, $W\Delta x^c+W^{-T}\Delta s^c=-W^{-T}\eta$) satisfies $\langle s,\Delta x^c\rangle+\langle x,\Delta s^c\rangle=0$ and $\langle\Delta x^c,\Delta s^c\rangle=0$.

Significance

The result. Lemma 4 says that a step of any length along the combined direction reduces the infeasibility residuals and the complementarity gap by exactly the same factor. Starting from a point with $\mu^0=1$, the iterates satisfy $G(z^k)=\mu^kG(z^0)$ and $\langle x^k,s^k\rangle=\mu^k\vartheta$, so the algorithm needs no merit function to balance feasibility against optimality, in contrast with earlier nonsymmetric methods. The lemma also shows that adding the third-order corrector does not cost this property, which is what justifies using the corrector in MOSEK's exponential-cone solver.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of Lemmas 2–4, the §2 homogeneity identities or the barrier sum rule has a machine-checked proof. The mission produces a formal homogeneous model for a general proper cone with a general LHSCB and a formal account of third-derivative calculus for logarithmically homogeneous barriers. Both are reusable in any analysis of interior-point methods for nonsymmetric cones (power cones, generalized power cones, hyperbolicity cones).

Difficulty

The obvious reading of Lemma 4 as bookkeeping with the linear map $G$ stalls at the corrector: the term $W^{-T}\eta$ in (18) involves the third derivative of the barrier, and nothing in linear algebra says how it interacts with the complementarity gap. Controlling it needs the third-derivative calculus of logarithmically homogeneous barriers. In Lean that means relating gradient, the Hessian as fderiv of the gradient, and the third derivative as fderiv of the Hessian, and working with the symmetry of iterated Fréchet derivatives of a $C^3$ function, for which the Mathlib interface is thin. A second obstacle is the augmented barrier: the barrier properties of $\hat F$ must be transported to $\hat F(\hat x)-\log\tau$ on $\mathbb R^{n+1}$ through the splitting $\mathbb R^{n+1}=\mathbb R^n\times\mathbb R$, including the boundary behaviour at the corner $\hat x\in\partial\hat K$, $\tau=0$.

The first identity of Lemma 4 is misprinted in the paper as $=0$. A formalization following the printed statement would be false, not merely awkward.

Formalization scope

Vectors of the augmented space are EuclideanSpace ℝ (Fin (n + 1)); $\hat x$ is the first $n$ coordinates and $\tau$ (resp. $\kappa$) the last. $A$ is a continuous linear map and $A^T$ its Hilbert adjoint; full row rank is surjectivity. Proper cones, the Hessian hess, the barrier class IsLogHomBarrier and the conjugate conj are the published SelfScaledIPM.ShortStep.Setting. That barrier class adds three standard conditions to the paper's two (boundary blow-up, the $\vartheta$-inequality and a positive definite Hessian), which the paper uses implicitly when it writes $(F''(x))^{-1}$ and calls $F$ a barrier. $W$ is a continuous linear equivalence and $W^{-T}$ the adjoint of $W^{-1}$. $F'''(x)[u,w]$ is fderiv ℝ (hess F) x u w and $(F''(x))^{-1}$ is ContinuousLinearMap.inverse. Every inner product includes the homogenizing term $\tau\kappa$.

Repairs, generalizations and specializations, each disclosed in the item statements:

• Repair: Lemma 4's first identity is stated as $-(1-\gamma)\langle x,s\rangle$, as derived in the paper's own proof, instead of the printed $0$.
• Generalization: one proper cone $\hat K$ with one barrier replaces the paper's product $K_1\times\dots\times K_k$. The product with the sum barrier is a special case.
• Generalization: $W$ is any nonsingular map satisfying (8). The paper's block-diagonal scaling with $W_{k+1}=\sqrt{\kappa/\tau}$ is a special case.
• Specialization: the sum rule is stated for $K_2=\mathbb R_+$, $F_2=-\log$, $\vartheta_2=1$, the only case the paper applies.

The directions are predicates ("$\Delta z$ solves (11)"), and the lemmas quantify over all solutions. The hypotheses are satisfiable. For the linear program $n=m=1$, $A=1$, $b=c=1$, $\hat K=\mathbb R_+$, $\hat F=-\log$, $x=s=(1,1)$, $y=0$, $W=I$, system (11) has the unique solution $\Delta x^a=(0,0)$, $\Delta s^a=(-1,-1)$, $\Delta y^a=1$. Statements that hold only because a junk value appears are ruled out: every statement requires $x\in\operatorname{int}K$ and $s\in\operatorname{int}K^*$, where $\log\tau$, the inverse Hessian and the conjugate barrier take their true values. A formalization that drops $\tau,\kappa$ from the inner products, or that fixes one solution of (18) instead of quantifying over all, would be a different lemma and does not count.

Welcome contributions: the general sum rule for products of cones, a Fin.append splitting library for EuclideanSpace, and proofs of the homogeneity identities that can be reused by the series' other missions.

Selected references

• J. Dahl, E. D. Andersen, A primal-dual interior-point algorithm for nonsymmetric exponential-cone optimization, Math. Program. 194 (2022) 341–370. https://doi.org/10.1007/s10107-021-01631-4
• Yu. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
• L. Tunçel, Generalization of primal-dual interior-point methods to convex optimization problems in conic form, Found. Comput. Math. 1 (2001) 229–254. https://doi.org/10.1007/s002080010009
• A. Skajaa, Y. Ye, A homogeneous interior-point algorithm for nonsymmetric convex conic optimization, Math. Program. 150 (2015) 391–422. https://doi.org/10.1007/s10107-014-0773-1
• T. Myklebust, L. Tunçel, Interior-point algorithms for convex optimization based on primal-dual metrics, arXiv:1411.2129 (2014). https://arxiv.org/abs/1411.2129

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