Convex Optimization

Distributed optimization over directed, changing networks

In distributed optimization, $n$ agents cooperatively minimize the average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of private cost functions $f_i:\mathbb R^p\to\mathbb R$, exchanging information only with their current neighbours in a communication network. The model covers sensor networks, multi-robot coordination and machine learning with data split across machines, where no node can see the whole objective. In many of these systems communication is one-directional (broadcast radios with unequal ranges, asymmetric links) and the network changes over time.

Directed links raise a specific obstacle: a node cannot in general choose weights that are both row and column stochastic, because it knows its out-degree but not how its messages are combined by others. The push-sum (ratio consensus) protocol of Kempe, Dobra and Gehrke (2003) circumvents this with column stochastic weights and a scalar correction. Nedić and Olshevsky (2015) combined it with diminishing-step subgradient methods over time-varying directed graphs, obtaining sublinear rates. Gradient tracking methods (Xu, Zhu, Soh and Xie, 2015; Qu and Li, 2016) and EXTRA (Shi, Ling, Wu and Yin, 2015) reached linear rates with constant steps on undirected or static graphs. Nedić, Olshevsky and Shi (arXiv 2016, SIAM J. Optim. 2017) proved geometric convergence of gradient tracking over graphs that are both time-varying and directed; this mission formalizes that result.

Setting

The agents are $\{1,\dots,n\}$. At each time $k$ there is a set $\mathcal A(k)$ of arcs; an arc $j\to i$ means agent $j$ can send to agent $i$. The out-degree $d^{\rm out}_j(k)$ counts the agents $i\ne j$ with $j\to i$ in $\mathcal A(k)$.

Assumption 6. There is $\tilde B_\ominus>0$ such that for every $t\ge0$ the union of the arc sets over the window $t\tilde B_\ominus,\dots,(t+1)\tilde B_\ominus-1$ is strongly connected. Put $B_\ominus=2\tilde B_\ominus-1$.

Assumption 7. The mixing matrix $C(k)$ has $C_{ij}(k)=1/(d^{\rm out}_j(k)+1)$ if $i=j$ or $j\to i\in\mathcal A(k)$, and $0$ otherwise; each $C(k)$ is column stochastic.

Each $f_i$ is differentiable with $L_i$-Lipschitz gradient (Assumption 4) and $\mu_i$-strongly convex with $\mu_i\ge0$, some $\mu_i>0$ (Assumption 5). Write $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$, $\bar\kappa=L/\bar\mu$, and $x^*$ for the minimizer of $f$.

Iterates are $n\times p$ matrices whose row $i$ belongs to agent $i$; $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$, and $\|\cdot\|_F$ is the Frobenius norm. Push-DIGing starts from $\mathbf x(0)=\mathbf u(0)$, $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$, $\mathbf v(0)=\mathbf 1$ and iterates, with step size $\alpha>0$ and $V(k)=\operatorname{diag}\{\mathbf v(k)\}$,

$$\mathbf u(k+1)=C(k)(\mathbf u(k)-\alpha\mathbf y(k)),\quad \mathbf v(k+1)=C(k)\mathbf v(k),\quad \mathbf x(k+1)=V(k+1)^{-1}\mathbf u(k+1),$$ $$\mathbf y(k+1)=C(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

The constants of the rate are $\tilde\tau=n^{-(2+nB_\ominus)}$, $Q_1=2n(1+\tilde\tau^{-nB_\ominus})/(1-\tilde\tau^{nB_\ominus})$, $\|V^{-1}\|^1_{\max}=\sup_{k,i}1/v_i(k)$ and, for an integer $B$,

$$\delta=Q_1\big(1-\tilde\tau^{nB_\ominus}\big)^{\frac{B-1}{nB_\ominus}},\qquad J_2=3Q_1\|V^{-1}\|^1_{\max}\bar\kappa B\big(\delta+Q_1(B-1)\big)(1+\sqrt n)\big(1+4\sqrt n\sqrt{\bar\kappa}\big).$$

Formalization targets

Goal: Theorem 18

For $n\ge2$, $B\ge B_\ominus$ with $\delta<1$, and every step size

$$0<\alpha<\frac{1.5(1-\delta)^2}{\bar\mu J_2},$$

there is $C>0$ with $\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k$ for all $k$, where $0<\lambda<1$ is

$$\lambda=\sqrt[2B]{1-\alpha\bar\mu/1.5}\ \text{ if }\ \alpha\le\frac{1.5\big(\sqrt{J_2^2+(1-\delta^2)J_2}-\delta J_2\big)^2}{\bar\mu J_2(J_2+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\alpha\bar\mu J_2/1.5}+\delta}\ \text{ otherwise}.$$

Milestones

The paper's proof runs a small gain argument around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf h}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$, $\mathbf z$ are gradient increments, $\mathbf h(k)=V(k)^{-1}\mathbf y(k)$ and $\check{\ }$ is the deviation from the row average. The milestones are the paper's own statements: the equivalent recursion (48) in terms of the row stochastic $\tilde R(k)=V(k+1)^{-1}C(k)V(k)$; the bound (49) $\|V^{-1}\|^1_{\max}\le n^{nB_\ominus}$ and row stochasticity of $\tilde R(k)$; Lemma 13 ($B$-step contraction by $\delta$); Lemmas 14–17 (the four arrows); Lemma 8 (an error bound for inexact gradient descent); Theorem 3 (the small gain theorem) and Lemma 4.

Significance

The theorem gives a geometric rate, with explicit constants, for a first-order method that uses only out-degree information, constant step sizes, one gradient per agent per round, and networks that are directed and need only be strongly connected jointly over windows. Before it, linear rates for distributed gradient methods required undirected or static graphs. The explicit $\lambda$ quantifies how the rate degrades with $n$, $B_\ominus$ and the condition number $\bar\kappa$. The result is proved in the paper; to the extent known, no machine-checked proof exists. A formalization yields a checked statement of the rate together with reusable components: the ergodic-norm small gain theorem, the push-sum weight bound, and the inexact gradient lemma, which also serve the companion DIGing mission on undirected graphs.

Difficulty

The natural Lyapunov approach fails: with asymmetric, time-varying weights there is in general no quadratic function that decreases at every step, and the consensus error contracts only over windows of $B$ iterations. The analysis therefore works with ergodic norms $\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ and chains four inequalities. Two further inputs come from outside the paper: the lower bound $v_i(k)\ge n^{-nB_\ominus}$ (Corollary 2(b) of Nedić–Olshevsky 2015) and the contraction of products of row stochastic matrices with entries bounded below on arcs (Lemma 5 of Nedić–Ozdaglar 2010), both of which a complete development has to prove.

Formalization scope

Stacked iterates are functions Fin n → EuclideanSpace ℝ (Fin p); agents are indexed from 0 and time from 0. An arc $j\to i$ is a pair (j, i) in a finite set A k. The weights $\mathbf v(k)$ are defined from $C$ alone, so $\|V^{-1}\|^1_{\max}$ is a constant of the graph sequence; it enters statements as a number with the hypothesis that it is the least upper bound of $\{1/v_i(k)\}$, never as a real supremum. Real powers are Real.rpow. The ergodic norm is the truncated maximum; the untruncated supremum is replaced by its pointwise meaning.

Four hypotheses are added to the page, each disclosed in the statements:

1. Assumption 7 includes the self-weight $C_{jj}(k)=1/(d^{\rm out}_j(k)+1)$. The printed rule assigns weights on arcs only, which makes column sums $d/(d+1)$; the paper's agent updates (p. 21) and analysis use the push-sum convention.
2. The step-size interval is open on the right: at $\alpha=1.5(1-\delta)^2/(\bar\mu J_2)$ the printed formula gives $\lambda=1$.
3. $B\ge B_\ominus$, required by Lemma 13, makes "large enough" precise.
4. $n\ge2$: at $n=1$ the constant $Q_1$ has a zero denominator.

The goal states only the hypotheses of Theorem 18 and the rate; it does not assume any of the arrows, gains, auxiliary parameters $\beta,\eta$ or ergodic-norm bounds, so it cannot be discharged by assembling hypotheses.

A complete development needs matrix-product contraction bounds for push-sum, Frobenius-norm calculus on stacked matrices, and strong convexity estimates for inexact gradient steps. The small gain theorem, Lemma 8 and the push-sum lemmas are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27 (2017) 2597–2633; arXiv:1607.03218v3. https://arxiv.org/abs/1607.03218 — https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Automat. Control 60 (2015) 601–615. https://arxiv.org/abs/1303.2289
• A. Nedić, A. Olshevsky, Stochastic gradient-push for strongly convex functions on time-varying directed graphs, arXiv:1406.2075, 2014. https://arxiv.org/abs/1406.2075
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, Proc. 44th IEEE FOCS, 2003, 482–491. https://doi.org/10.1109/SFCS.2003.1238221
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: an exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25 (2015) 944–966. https://arxiv.org/abs/1404.6264
• G. Qu, N. Li, Harnessing smoothness to accelerate distributed optimization, arXiv:1605.07112, 2016. https://arxiv.org/abs/1605.07112
• J. Xu, S. Zhu, Y. C. Soh, L. Xie, Augmented distributed gradient methods for multi-agent optimization under uncoordinated constant stepsizes, Proc. 54th IEEE CDC, 2015, 2055–2060.

Motivation

In distributed optimization, $n$ agents each hold a private function $f_i:\mathbb R^p\to\mathbb R$ and must jointly solve

$$\min_{x\in\mathbb R^p}\ f(x)=\frac1n\sum_{i=1}^n f_i(x)$$

by exchanging vectors only with their current neighbours in a communication network. The setting covers distributed estimation and learning in sensor networks, formation control and power-system control, where no agent can see all the data and no central coordinator is available. Often the network changes over time: links appear and fail, and agents move.

The classical method, distributed gradient descent (DGD), mixes neighbours' iterates and takes a local gradient step. With a fixed step size it does not converge to the optimum, because at a consensual optimum the local gradients $\nabla f_i(x^*)$ need not vanish; exact convergence requires diminishing steps and is then sublinear. Nedić, Olshevsky and Shi (arXiv:1607.03218, SIAM J. Optim. 2017) introduced DIGing, which adds a second variable that tracks the network-wide average gradient, and proved that it converges R-linearly (geometrically) to the exact optimum with a fixed step size, over time-varying undirected graphs, with an explicit rate.

Setting

An $n\times p$ matrix $\mathbf x$ is stored by its rows; row $i$ is agent $i$'s copy $x_i\in\mathbb R^p$, and $\|\mathbf x\|_F$ is the Frobenius norm. Write $\bar x=\frac1n\sum_ix_i$ and $\check{\mathbf x}=\mathbf x-\mathbf 1\bar x^\top$ (the consensus violation). The stacked gradient $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$.

Objectives. Each $f_i$ is differentiable with $L_i$-Lipschitz gradient, $L_i>0$ (Assumption 4), and satisfies $f_i(x)\ge f_i(y)+\langle\nabla f_i(y),x-y\rangle+\frac{\mu_i}2\|x-y\|^2$ with $\mu_i\ge0$, at least one $\mu_i>0$ (Assumption 5). Put $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$ and $\bar\kappa=L/\bar\mu$. Then $f$ has a unique minimizer $x^*$.

Network. At time $k$ the agents communicate over an undirected graph $E(k)$ and mix with a matrix $W(k)$. Let $W_B(k)=W(k)W(k-1)\cdots W(k-B+1)$ and $\delta(k)=\sigma_{\max}\{W_B(k)-\frac1n\mathbf 1\mathbf 1^\top\}$. Assumption 1 requires: $W_{ij}(k)=0$ when $i\ne j$ and $(j,i)\notin E(k)$; every $W(k)$ is doubly stochastic; and for some positive integer $B$, $\delta=\sup_{k\ge B-1}\delta(k)<1$.

DIGing (Algorithm 1) with step size $\alpha>0$: $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$ and

$$\mathbf x(k+1)=W(k)\mathbf x(k)-\alpha\mathbf y(k),\qquad \mathbf y(k+1)=W(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

Formalization targets

Goal: Theorem 10

Let $J_1=3\bar\kappa B^2(1+4\sqrt n\sqrt{\bar\kappa})$. For every step size $0<\alpha<1.5(1-\delta)^2/(\bar\mu J_1)$ there is $C>0$ with

$$\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k\quad\text{for all }k,$$

where $0<\lambda<1$ is the explicit rate

$$\lambda=\sqrt[2B]{1-\frac{\alpha\bar\mu}{1.5}}\ \text{ if }\ \alpha\le\frac{1.5(\sqrt{J_1^2+(1-\delta^2)J_1}-\delta J_1)^2}{\bar\mu J_1(J_1+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\frac{\alpha\bar\mu J_1}{1.5}}+\delta}\ \text{ otherwise.}$$

Milestones

The proof runs a small gain argument in the ergodic norm $\|\mathbf s\|_F^{\lambda,K}=\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf y}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$ and $\mathbf z(k)$ are the gradient differences. The milestones are the paper's own lemmas: Lemma 2 (the $B$-step consensus contraction); Lemmas 5, 6, 7 and 9 (the four arrows); Lemma 8 (an error bound for inexact gradient descent, used by Lemma 9); Theorem 3 (the small gain theorem); Lemma 4 (a bounded ergodic norm gives an R-linear rate).

Companions

The existence and uniqueness of $x^*$ (p. 9); Corollary 11, the polynomial-in-$n$ rate $\lambda(\tau)=\sqrt[B]{1-\tau^2/(128B^2n^{4.5}\bar\kappa^{1.5})}$ under the concrete graph and weight Assumptions 2–3; and Proposition 1, the optimality conditions behind the algorithm.

Significance

Theorem 10 gives geometric convergence of a fixed-step method to the exact optimum over networks that may be disconnected at every instant, provided they are jointly well mixed over windows of $B$ steps. Its rate is explicit in $B$, $n$, $\delta$, $\bar\mu$ and $\bar\kappa$, and Corollary 11 turns it into an iteration count polynomial in $n$. Gradient tracking of this kind has since become a standard building block of decentralized optimization and learning algorithms, and the small-gain analysis in the ergodic norm is reused for other methods with time-varying or directed communication; the companion mission in this series treats Push-DIGing over directed graphs with the same machinery.

The result is proved in the paper. As far as is known it has not been machine-checked. A formalization provides checked versions of the paper's reusable components: the small gain theorem in the ergodic norm, the error bound for inexact gradient descent on a sum of strongly convex functions, and the consensus contraction for products of doubly stochastic matrices. It also pins down the conventions the paper leaves implicit, such as the sign of the mixing weights and the endpoint of the step-size interval.

Difficulty

DIGing does not decrease any obvious quantity monotonically: the distance to the optimum can grow while the gradient tracker is still far from consensus, and over a time-varying graph a single mixing step need not contract at all; only products of $B$ matrices do. A one-step Lyapunov argument therefore fails. The paper's way around this is to bound each quantity of the cycle by the previous one in the ergodic norm, with gains that depend on $\lambda$, and to choose $\lambda$ and $\alpha$ so that the product of the four gains is below one. The algebra of that choice, which produces the two-regime formula for $\lambda$, is delicate: the constraints $\delta<\lambda^B<1$, $\sqrt{1-\alpha\bar\mu\beta/(\beta+1)}\le\lambda$ and the gain condition (37) pull in opposite directions. Lemma 8 needs a careful one-step analysis of gradient descent with perturbed gradient evaluations.

Formalization scope

A stacked matrix is Fin n → EuclideanSpace ℝ (Fin p); $\|\cdot\|_F$, $\bar x$, $\check{\mathbf x}$, $\mathbf 1c^\top$ and the ergodic norm (6) are defined in DIGing.Undir.Common; $W_B(k)$, $\sigma_{\max}$ (the operator norm on Euclidean $\mathbb R^n$), $\delta(k)$, Assumptions 1–3, DIGing, $J_1$ and the rate are in DIGing.Undir.Setting. The constants $L_i,\mu_i$ are parameters. $\delta$ is given as the least upper bound of $\{\delta(k):k\ge B-1\}$, and the optimum $x^*$ by its optimality. Agents and iterations are indexed from $0$. Roots are Real.rpow.

Two hypotheses differ from the printed text, both disclosed in the item notes. Doubly stochastic includes nonnegative entries (Mathlib's doublyStochastic); the paper uses the term in this sense, and Lemma 6 is false for signed matrices with unit row and column sums. The right endpoint $\alpha=1.5(1-\delta)^2/(\bar\mu J_1)$, printed as included, is excluded: there the rate formula gives $\lambda=1$. Corollary 11 assumes $p\ge1$, the paper's standing range (p. 4).

The goal assumes nothing about the arrows, the gains, the auxiliary parameters $\beta,\eta$ or the ergodic norm of the iterates; its only rate hypothesis is $0<\alpha<1.5(1-\delta)^2/(\bar\mu J_1)$, and its conclusion includes $\lambda<1$, so a bounded-sequence reading is ruled out.

A complete development needs: products and the spectral norm of doubly stochastic matrices; the ergodic norm and its monotonicity in $K$; basic smooth strongly convex analysis (existence of the minimizer, $\mu_i\le L_i$, co-coercivity); and real-power algebra for the choice of $\lambda$. The small gain theorem, Lemma 8 and Lemma 2 are reusable beyond this mission, and are shared with the Push-DIGing mission of this series. Corollary 11's proof additionally uses a bound $\delta\le1-\tau/(2n^2)$ from the consensus literature; formalizing it is a welcome separate contribution. Proofs of any milestone, and alternative arguments for the arrows, are welcome.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27(4), 2017. https://arxiv.org/abs/1607.03218 (v3 is the version formalized)
• A. Nedić, A. Olshevsky, A. Ozdaglar, J. N. Tsitsiklis, On distributed averaging algorithms and quantization effects, IEEE Trans. Automat. Control 54(11), 2009. https://doi.org/10.1109/TAC.2009.2031203
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25(2), 2015. https://arxiv.org/abs/1404.6264
• A. Nedić, A. Ozdaglar, Distributed subgradient methods for multi-agent optimization, IEEE Trans. Automat. Control 54(1), 2009. https://doi.org/10.1109/TAC.2008.2009515

Motivation

DC programming is the minimization of a function $f = g - h$ that is a difference of two convex functions. The class contains every $C^2$ function on a compact convex set and most nonconvex models of sparse learning, clustering, combinatorial relaxations and robust optimization, and its standard method, the DC Algorithm (DCA), replaces $h$ by its affine minorant at the current iterate and solves a convex program at each step. DCA was introduced by Pham Dinh Tao in 1985 and developed jointly with Le Thi Hoai An from 1994 on (Pham Dinh & Le Thi 1998); the survey of Le Thi & Pham Dinh 2018 collects thirty years of that work.

DCA is guaranteed to reach critical or strongly critical points, notions that depend on the chosen decomposition $g - h$, while a decomposition-free notion, directional (d-)stationarity of $f$ itself, is what a user of a nonconvex model usually wants. Ahn, Pang & Xin 2017 warned that DC criticality can be much weaker than d-stationarity. Theorem 1 of the 2018 survey (p. 9) states when the two coincide. Its proof is omitted in the paper ("can be easily deduced … It is omitted here").

Setting

Let $X = \mathbb R^n$ with the canonical inner product $\langle\cdot,\cdot\rangle$. Functions take values in $\mathbb R\cup\{\pm\infty\}$. The effective domain of $\varphi$ is $\operatorname{dom}\varphi = \{x : \varphi(x) < +\infty\}$, and $\Gamma_0(X)$ is the set of proper, lower semicontinuous, convex functions $X \to \mathbb R\cup\{+\infty\}$.

The standard DC program is

$$(P_{dc})\qquad \alpha = \inf\{f(x) := g(x) - h(x) : x\in X\},\qquad g, h\in\Gamma_0(X),$$

with the convention $+\infty - (+\infty) = +\infty$, and $\alpha$ is assumed finite. Finiteness of $\alpha$ forces $\operatorname{dom} g\subset\operatorname{dom} h$, so $\operatorname{dom} f = \operatorname{dom} g$.

The subdifferential of $\varphi$ at $x$ is

$$\partial\varphi(x) = \{y\in X : \varphi(x) < +\infty,\ \varphi(v) \ge \varphi(x) + \langle y, v - x\rangle\ \ \forall v\in X\}.$$

A point $x$ is strongly critical for $f = g - h$ if $\emptyset \ne \partial h(x)\subset\partial g(x)$.

The directional derivative of $\varphi$ at $x\in\operatorname{dom}\varphi$ in direction $u$ is $\varphi'(x;u) = \lim_{t\downarrow 0}(\varphi(x+tu) - \varphi(x))/t$. For convex $\varphi$ it equals $\inf_{t>0}(\varphi(x+tu)-\varphi(x))/t$. A point $x\in\operatorname{dom} f$ is d-stationary for $f$ if $f'(x;u)\ge 0$ for every $u\in X$. The support function of $C\subset X$ is $\chi^*_C(u) = \sup_{y\in C}\langle u, y\rangle$, with $\chi^*_\emptyset \equiv -\infty$. Finally, $\operatorname{ri} C$ is the relative interior of $C$, its interior inside the affine hull $\operatorname{aff} C$.

Formalization targets

Goal: Theorem 1(iii)

For $x\in\operatorname{ri}(\operatorname{dom} g)\cap\operatorname{ri}(\operatorname{dom} h)$,

$$x \text{ is d-stationary for } f \iff \emptyset\ne\partial h(x)\subset\partial g(x).$$

Milestones

1. Theorem 1(i): for $x\in\operatorname{dom} g$ with $\partial h(x)\ne\emptyset$,

$$f'(x;u) = g'(x;u) - h'(x;u)\qquad \forall u\in X.$$

2. Theorem 1(ii), first sentence: under the same hypotheses, $x$ is d-stationary iff $g'(x;u)\ge h'(x;u)$ for all $u$.
3. Theorem 1(iv): for $x\in\operatorname{ri}(\operatorname{dom} g)$ with $\partial h(x)\ne\emptyset$, d-stationarity implies strong criticality.
4. Theorem 1(v): for $x\in\operatorname{ri}(\operatorname{dom} h)$, strong criticality implies d-stationarity.

Companion statements

• Theorem 1(ii), second sentence: for $x\in\operatorname{dom} g$, if $g'(x;\cdot) = \chi^*_{\partial g(x)}$ and $h'(x;\cdot) = \chi^*_{\partial h(x)}$, then d-stationarity and strong criticality coincide.
• Theorem 1(vi): if $\operatorname{aff}(\operatorname{dom} g) = \operatorname{aff}(\operatorname{dom} h)$, then $\operatorname{ri}(\operatorname{dom} g)\subset\operatorname{ri}(\operatorname{dom} h)$ and the equivalence holds on $\operatorname{ri}(\operatorname{dom} g)$.

Part (iii) is the goal because it is the equivalence the paper uses to justify DCA, stated under a hypothesis symmetric in $g$ and $h$; (vi) is the more general companion.

Significance

The theorem connects the output of DCA with a stationarity notion intrinsic to $f$. Without it, the strong criticality certified by DCA would be a property of a decomposition rather than of the problem, and different decompositions of the same $f$ could certify different points. With it, at points in the relative interiors of the domains, every strongly critical point is d-stationary, and conversely no d-stationary point is missed by the criticality test.

Parts (i) and (ii) are stated in the paper without proof, and so is the rest of Theorem 1; none of it has a machine-checked proof. The mission produces a formal statement of all six parts with the extended-real conventions made explicit. Three of the printed parts are false as stated without the nonemptiness of $\partial h(x)$; the formal versions add that hypothesis and record a counterexample for each, so the formalization also corrects the printed statement.

Difficulty

The obvious argument writes $f'(x;u) = g'(x;u) - h'(x;u)$ and reads off both directions from $g'\ge h'$. Two steps of it fail. First, the difference can be $-\infty - (-\infty)$ or $+\infty - (+\infty)$, and the limit defining $f'$ need not be the difference of the limits; the nonemptiness of $\partial h(x)$ is exactly what rules out the first case. Second, passing from "$g'(x;\cdot)\ge h'(x;\cdot)$" to "$\partial h(x)\subset\partial g(x)$" needs $h'(x;\cdot)$ to equal the support function of $\partial h(x)$, which holds in the relative interior of $\operatorname{dom} h$ but fails on its relative boundary, where $h'(x;\cdot)$ need not be lower semicontinuous. The relative interior, not the interior, is essential: the domains may be lower-dimensional.

Formalization scope

$X$ is EuclideanSpace ℝ (Fin n), and every function maps into EReal. The published definitions TaoAnDCA.GlobalOpt.Setting supply $\operatorname{dom}$ (effDom), the DC objective with $+\infty - (+\infty) = +\infty$ (dcSub), the subdifferential (subdiff) and $\alpha$ (primalValue); $\Gamma_0(X)$ is the published IsProperClosedConvex. Every statement carries the standing assumptions of Theorem 1 as binders: $g, h\in\Gamma_0(X)$, $\alpha\ne-\infty$ and $\alpha\ne+\infty$. The mission's definitions are:

• convDirDeriv: the convex directional derivative by the paper's infimum formula, in EReal;
• HasDirDerivE: the predicate that the one-sided limit along $t\downarrow 0$ exists in EReal and equals a given value;
• IsDStationary: $x\in\operatorname{dom}\varphi$ and, for every direction, the limit exists and is $\ge 0$;
• IsStronglyCritical: both $\partial h(x)\ne\emptyset$ and $\partial h(x)\subset\partial g(x)$;
• supportFn: the extended-real support function, $-\infty$ on $\emptyset$.

The relative interior is Mathlib's intrinsicInterior ℝ, the affine hull is affineSpan ℝ. The subgradient inequality has the standard sign; display (1) of the paper prints the opposite sign, a slip. The only hypothesis added to the page is $\partial h(x)\ne\emptyset$, in parts (i), (ii) first sentence and (iv), each of which is false without it; parts (ii) second sentence, (iii), (v) and (vi) are stated as printed.

The statement admits trivializing formalizations, which this one rules out. Strong criticality without the nonemptiness of $\partial h(x)$ is vacuous wherever $\partial h(x) = \emptyset$. A d-stationarity defined through limUnder, a real-valued derivative, or "every limit is nonnegative" holds vacuously where the limit does not exist. And $g - h$ written in raw EReal would give $+\infty - (+\infty) = -\infty$.

A complete development needs the monotonicity of convex difference quotients in EReal, limit arithmetic for extended reals, and the formula $\varphi'(x;\cdot) = \chi^*_{\partial\varphi(x)}$ for $\varphi\in\Gamma_0(\mathbb R^n)$ at points of $\operatorname{ri}(\operatorname{dom}\varphi)$ (Rockafellar 1970, Theorem 23.4), together with the nonemptiness of $\partial\varphi$ there. These results on extended-real convex functions are reusable well beyond DC programming, and contributions of them as separate theorems are welcome.

Selected references

• H. A. Le Thi, T. Pham Dinh, DC programming and DCA: thirty years of developments, Mathematical Programming Ser. B 169 (2018), 5–68. https://doi.org/10.1007/s10107-018-1235-y
• T. Pham Dinh, H. A. Le Thi, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM Journal on Optimization 8 (1998), 476–505. https://doi.org/10.1137/S1052623494274313
• M. Ahn, J.-S. Pang, J. Xin, Difference-of-convex learning: directional stationarity, optimality, and sparsity, SIAM Journal on Optimization 27 (2017), 1637–1665. https://doi.org/10.1137/16M1084754
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

In decentralized optimization, $n$ agents connected by a communication network jointly minimize a sum of private functions without a central coordinator: each agent sees only its own $f_i$ and talks only to its neighbours. Applications include sensor networks, distributed estimation, multi-agent control and learning over data spread across machines. The simplest method in this setting is decentralized gradient descent (DGD), in which every agent averages its neighbours' iterates and then takes a local gradient step. DGD and its relatives were analysed by Nedić and Ozdaglar (IEEE TAC 2009) and many later papers, almost always under the assumption that the (sub)gradients are bounded.

K. Yuan, Q. Ling and W. Yin (arXiv:1310.7063v3; SIAM J. Optim. 26(3), 2016) removed that assumption for DGD with a fixed stepsize. They showed that a stepsize bound depending on the spectrum of the mixing matrix keeps the gradients bounded, that the agents stay within $O(\alpha/(1-\beta))$ of their mean, and that for convex smooth $f_i$ the objective error of the mean decreases at rate $O(1/(\alpha k))$ until it reaches a neighbourhood of size $O(\alpha/(1-\beta))$. This mission formalizes that last result, Theorem 2 of the paper, together with the lemmas its proof rests on.

Setting

Consider $n \ge 2$ agents on a connected undirected graph $G$. Agent $i$ holds a function $f_i : \mathbb R^p \to \mathbb R$, and the agents solve

$$\min_{x \in \mathbb R^p} f(x) = \sum_{i=1}^n f_i(x), \qquad (2)$$

with solution set $\mathcal X^*$, assumed nonempty.

A mixing matrix $W = [w_{ij}]$ is symmetric and doubly stochastic, and $w_{ij} \ne 0$ only if $i = j$ or $i$ and $j$ are neighbours. Its eigenvalues are $1 = \lambda_1(W) \ge \lambda_2(W) \ge \dots \ge \lambda_n(W) \ge -1$, and

$$\beta = \max\{|\lambda_2(W)|, |\lambda_n(W)|\}. \qquad (5)$$

Assumption 1 (p. 4): (a) each $f_i$ is convex, bounded below, and differentiable with an $L_{f_i}$-Lipschitz gradient, $L_{f_i} > 0$; (b) the network is connected and $W$ is symmetric, doubly stochastic, with $\beta < 1$.

DGD with stepsize $\alpha$, started from $x_{(i)}(0) = 0$, is

$$x_{(i)}(k+1) = \sum_{j=1}^n w_{ij}\, x_{(j)}(k) - \alpha \nabla f_i(x_{(i)}(k)), \qquad i = 1, \dots, n. \qquad (4)$$

Stacked vectors $[x_{(i)}] = [x_{(1)}; \dots; x_{(n)}] \in \mathbb R^{np}$ carry the Euclidean norm. Write $h(k) = [\nabla f_1(x_{(1)}(k)); \dots; \nabla f_n(x_{(n)}(k))]$, $\bar x(k) = \frac1n\sum_i x_{(i)}(k)$, $g(k) = \frac1n\sum_i\nabla f_i(x_{(i)}(k))$, $\bar g(k) = \frac1n\sum_i \nabla f_i(\bar x(k))$, $\bar f = \frac1n f$, $L_h = \max_i L_{f_i}$, $L_{\bar f} = \frac1n\sum_i L_{f_i}$, $f_i^o = \inf f_i$ and

$$D = \sqrt{2L_h\textstyle\sum_{i=1}^n\big(f_i(0) - f_i^o\big)}. \qquad (10)$$

The paper reads DGD as unit-step gradient descent on the Lyapunov function

$$\xi_\alpha([x_{(i)}]) = -\tfrac12\textstyle\sum_{i,j} w_{ij}\, x_{(i)}^\top x_{(j)} + \sum_i\big(\tfrac12\|x_{(i)}\|^2 + \alpha f_i(x_{(i)})\big). \qquad (8)$$

For a minimizer $[\tilde x_{(i)}]$ of $\xi_\alpha$ and a solution $x^* \in \mathcal X^*$, set

$$C = \frac{1}{\sqrt n}\Big(\|[x_{(i)}(0) - \tilde x_{(i)}]\| + \|[\tilde x_{(i)} - x^*]\|\Big), \qquad \bar r(k) = \bar f(\bar x(k)) - \bar f(x^*). \qquad (17)$$

Formalization targets

Goal: Theorem 2 with the constants of its proof

Let $0 < \alpha \le \min\{(1+\lambda_n(W))/L_h,\ 1/L_{\bar f}\}$ and $T = C\sqrt2\cdot\alpha L_h D/(1-\beta)$. Then

$$\bar r(k) > T \ \Longrightarrow\ \bar r(k+1) \le \bar r(k) - \frac{\alpha}{4C^2}\,\bar r(k)^2,$$

and, for $k \ge 1$, if $\bar r(j) > T$ for every $j < k$, then

$$\bar r(k) \le \frac{4C^2}{\alpha k}.$$

The paper prints these as $\bar r(k+1) \le \bar r(k) - O(\alpha\bar r^2(k))$ and $\bar r(k) \le O(1/(\alpha k))$. The constants are the ones its proof fixes: the recursion with $\alpha/(2C^2)$ (milestone below) and the threshold condition "$(\alpha/(2C^2))\bar r^2(k) > 2\cdot\alpha^3D^2L_h^2/(2(1-\beta)^2)$", under which the error term absorbs half of the quadratic decrease. That gives $\alpha/(4C^2)$, and "$1/\bar r(k)$ increases at $\Omega(\alpha k)$" with this constant gives $4C^2/(\alpha k)$.

Milestones

1. Theorem 1, (10): for $0 < \alpha \le (1+\lambda_n(W))/L_h$, $\|h(k)\| \le D$ for every $k$.
2. Lemma 1: if $\|h(s)\| \le B$ for all $s$, then $\|x_{(i)}(k) - \bar x(k)\| \le \alpha B/(1-\beta)$.
3. Lemma 2: $\|\nabla f_i(x_{(i)}(k)) - \nabla f_i(\bar x(k))\| \le \alpha B L_{f_i}/(1-\beta)$ and $\|g(k) - \bar g(k)\| \le \alpha B L_h/(1-\beta)$.
4. (15): $\bar x(k+1) = \bar x(k) - \alpha g(k)$.
5. (17): $\|[x_{(i)}(k) - \tilde x_{(i)}]\| \le \|[x_{(i)}(0) - \tilde x_{(i)}]\|$ and $\|\bar x(k) - x^*\| \le C$.
6. $\bar r(k+1) \le \bar r(k) - \frac{\alpha}{2}\|\bar g(k)\|^2 + \frac{\alpha^3D^2L_h^2}{2(1-\beta)^2}$.
7. $\bar r(k+1) \le \bar r(k) - \frac{\alpha}{2C^2}\bar r(k)^2 + \frac{\alpha^3D^2L_h^2}{2(1-\beta)^2}$.

Significance

Theorem 2 is the convex, non-strongly-convex case of the paper's analysis. It says that DGD with a constant stepsize behaves like centralized gradient descent, with rate $O(1/k)$, until it reaches a floor of size $O(\alpha/(1-\beta))$. The floor shrinks with the stepsize and grows as the spectral gap $1-\beta$ of the network closes, which makes the trade-off between speed, accuracy and network connectivity explicit. The result is proved without bounded gradients; the boundedness comes out of the stepsize condition through the Lyapunov function. It is the baseline that exact methods such as EXTRA (Shi et al. 2015) were designed to improve on.

The paper's proof is complete in its main lines but informal in places: the rate is stated with $O(\cdot)$, the constant $C$ is written with a $k$-dependent $x^*(k)$, and the minimizer of $\xi_\alpha$ is asserted to exist on grounds that do not suffice. To our knowledge no part of this analysis (DGD, mixing matrices with spectral bounds, the Lyapunov reformulation) has been machine-checked. A formal proof fixes the constants, records the needed hypotheses, and supplies decentralized-optimization infrastructure that Mathlib lacks.

Difficulty

The obvious approach treats the mean $\bar x(k)$ as gradient descent on $\bar f$ with the exact gradient $\bar g(k)$, which fails: by (15) the mean moves along $g(k)$, the average of gradients taken at different points. Controlling $g(k) - \bar g(k)$ needs the consensus bound of Lemma 1, which in turn needs the gradients to be bounded, and no assumption bounds them. They are bounded only because DGD is unit-step gradient descent on $\xi_\alpha$ and the stepsize condition makes that descent monotone (Theorem 1). Lemma 1 also needs the operator-norm identity $\|W^m - \frac1n\mathbf 1\mathbf 1^\top\| = \beta^m$ for a symmetric doubly stochastic $W$, a spectral fact about sorted eigenvalues. Finally, the recursion in $\bar r$ needs a bound on $\|\bar x(k) - x^*\|$ that is uniform in $k$, which comes from Fejér monotonicity of the iterates with respect to a minimizer of $\xi_\alpha$, not from anything about $\bar f$.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p) and stacked vectors are PiLp 2 (fun _ : Fin n => ℝᵖ), so every stacked norm ($\|h(k)\|$, $D$, $C$) is Euclidean on $\mathbb R^{np}$, not the sup norm. Gradients are Mathlib's gradient. DGD is a recursively defined sequence started at $0$, not an arbitrary sequence with a property. $\lambda_n(W)$ and $\beta$ come from the eigenvalues of the symmetric $W$ sorted with multiplicity (eigenvalues₀). $f_i^o$ is $\inf f_i$, and $L_h$ is a supremum over the finite index set, i.e. a maximum.

Conventions and additions, each disclosed in the item statements:

• $n \ge 2$ is part of Assumption 1 (so that $\lambda_2(W)$ exists); $\alpha > 0$ (a stepsize).
• A minimizer $[\tilde x_{(i)}]$ of $\xi_\alpha$ is a hypothesis. The paper derives its existence from minimizers of the $f_i$, which Assumption 1 does not provide.
• $C$ uses one fixed $x^* \in \mathcal X^*$, chosen before $k$; that $x^*$ also defines $\bar f^* = \bar f(x^*)$. On the page $x^*$ in (17) is $x^*(k)$, which would make $C$ depend on $k$.
• Theorem 1's convergence sentence is not posed; it fails at the boundary stepsize $\alpha = (1+\lambda_n(W))/L_h$. Only the bound (10) is posed, for every $k \ge 0$.
• Lemmas 1 and 2 take a generic gradient bound $B$ in place of $D$.

Trivializing formalizations are ruled out. The iterates are the DGD recursion itself. The threshold in the rate is required at every earlier step, not only at step $k$. $C$ does not depend on $k$. The constants $\alpha/(4C^2)$ and $4C^2/(\alpha k)$ are explicit, not an existential placed before the data. A sorry-free instance ($n = 2$, $W = \frac12\mathbf 1\mathbf 1^\top$, constant $f_i$) shows that the goal's hypotheses can all hold together.

A complete development needs: the operator norm of $W^m - \frac1n\mathbf 1\mathbf 1^\top$ via the spectral theorem, the descent lemma and co-coercivity for $L$-smooth convex functions on Euclidean space, $\|\nabla g\|^2 \le 2L(g - \inf g)$ for $L$-smooth functions bounded below, and Fejér monotonicity of gradient descent. These are reusable well beyond this mission. Contributions to any milestone are welcome; Lemmas 1–2 and (15) do not use convexity.

Selected references

• K. Yuan, Q. Ling, W. Yin, On the Convergence of Decentralized Gradient Descent, SIAM J. Optim. 26(3), 2016, https://doi.org/10.1137/130943170; preprint arXiv:1310.7063v3 (the version cited throughout). https://arxiv.org/abs/1310.7063
• A. Nedić, A. Ozdaglar, Distributed Subgradient Methods for Multi-Agent Optimization, IEEE Trans. Automat. Control 54(1):48–61, 2009. https://doi.org/10.1109/TAC.2008.2009515
• Y. Nesterov, Gradient Methods for Minimizing Composite Objective Function, CORE report, 2007 (reference [21] of the paper, cited for the gradient-descent facts); journal version Math. Program. 140:125–161, 2013. https://doi.org/10.1007/s10107-012-0629-5
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An Exact First-Order Algorithm for Decentralized Consensus Optimization, SIAM J. Optim. 25(2):944–966, 2015. https://doi.org/10.1137/14096668X

Decentralized consensus optimization

In decentralized consensus optimization, $n$ agents connected by a communication network cooperatively solve

$$\min_{x\in\mathbb R^p}\ \bar f(x)=\frac1n\sum_{i=1}^n f_i(x),$$

where agent $i$ privately holds the convex function $f_i$ and may only exchange vectors with its neighbours. The model covers distributed estimation and learning over sensor networks, multi-agent control and decentralized machine learning, where no agent may collect all the data. The classical method, decentralized gradient descent (DGD), lets every agent average its neighbours' iterates and take a local gradient step. With a fixed step size DGD stalls at a neighbourhood of the solution whose size is proportional to the step, so exact convergence requires diminishing steps and is slow.

Shi, Ling, Wu and Yin (arXiv:1404.6264; SIAM J. Optim. 25 (2015)) introduced EXTRA, an "exact first-order algorithm" that keeps a fixed step size and still converges to the exact solution. This mission formalizes the second main result of that paper: under restricted strong convexity, EXTRA converges linearly. The companion mission of the series covers the sublinear rates for general convex objectives.

Setting

Agent $i$ keeps a local copy $x_{(i)}\in\mathbb R^p$; the stacked variable $\mathbf x\in\mathbb R^{n\times p}$ has these copies as rows, with Frobenius inner product $\langle\mathbf x,\mathbf y\rangle_F=\sum_i\langle x_{(i)},y_{(i)}\rangle$. Write $\mathbf f(\mathbf x)=\sum_i f_i(x_{(i)})$, let $\nabla\mathbf f(\mathbf x)$ be the matrix with rows $\nabla f_i(x_{(i)})$, and for a symmetric matrix $M$ let $\|\mathbf x\|_M^2=\operatorname{trace}(\mathbf x^{\mathsf T}M\mathbf x)$.

Two symmetric mixing matrices $W,\tilde W\in\mathbb R^{n\times n}$ satisfy Assumption 1: their off-diagonal entries vanish between non-neighbours of a connected graph; $\operatorname{null}\{W-\tilde W\}=\operatorname{span}\{\mathbf 1\}$ and $\tilde W\mathbf 1=\mathbf 1$; and $\tilde W\succ0$, $\frac{I+W}{2}\succeq\tilde W\succeq W$. Each $f_i$ is convex with $L_{\mathbf f}$-Lipschitz gradient (Assumption 2), and the problem has a solution $x^*$ (Assumption 3). With step size $\alpha>0$, EXTRA is

$$\mathbf x^1=W\mathbf x^0-\alpha\nabla\mathbf f(\mathbf x^0),\qquad \mathbf x^{k+2}=(I+W)\mathbf x^{k+1}-\tilde W\mathbf x^k-\alpha\big[\nabla\mathbf f(\mathbf x^{k+1})-\nabla\mathbf f(\mathbf x^k)\big].$$

Each agent uses only its own gradient and its neighbours' iterates.

The analysis uses $U=(\tilde W-W)^{1/2}$, the auxiliary sequence $\mathbf q^k=\sum_{t=0}^kU\mathbf x^t$, an optimal pair $(\mathbf q^*,\mathbf x^*)$ with $\mathbf x^*=\mathbf 1(x^*)^{\mathsf T}$, $\mathbf q^*=U\mathbf p$, $U\mathbf q^*+\alpha\nabla\mathbf f(\mathbf x^*)=0$, and the stacked pair $\mathbf z^k=(\mathbf q^k;\mathbf x^k)$, $\mathbf z^*=(\mathbf q^*;\mathbf x^*)$ measured in $\|\mathbf z\|_G^2=\|\mathbf q\|_F^2+\|\mathbf x\|_{\tilde W}^2$.

A gradient map $\nabla h$ is restricted strongly convex with respect to $\tilde x$ with constant $\mu>0$ if $\langle\nabla h(x)-\nabla h(\tilde x),x-\tilde x\rangle\ge\mu\|x-\tilde x\|^2$ for all $x$. The condition is imposed on the penalized function

$$\mathbf g(\mathbf x)=\mathbf f(\mathbf x)+\frac{1}{4\alpha}\|\mathbf x\|^2_{\tilde W-W},\qquad \nabla\mathbf g(\mathbf x)=\nabla\mathbf f(\mathbf x)+\frac1{2\alpha}(\tilde W-W)\mathbf x .$$

Formalization targets

Goal: Theorem 3.7 (p. 15)

If $\mathbf g$ is restricted strongly convex with respect to $\mathbf x^*$ with constant $\mu_{\mathbf g}>0$ and $\alpha<2\mu_{\mathbf g}\lambda_{\min}(\tilde W)/L_{\mathbf f}^2$, then there is $\delta>0$ such that for all $k$

$$\|\mathbf z^k-\mathbf z^*\|_G^2\ \ge\ (1+\delta)\,\|\mathbf z^{k+1}-\mathbf z^*\|_G^2,$$

and consequently $\|\mathbf x^k-\mathbf x^*\|_{\tilde W}^2=O\big((1+\delta)^{-k}\big)$. The goal asserts the existence of a contraction factor, not a particular value of $\delta$, so it survives any improvement of the constants.

Milestones

1. the summed form (3.5) of EXTRA and Lemma 3.2, the error recursion

$$(I+W-2\tilde W)(\mathbf x^{k+1}-\mathbf x^*)+\tilde W(\mathbf x^{k+1}-\mathbf x^k)=-U(\mathbf q^{k+1}-\mathbf q^*)-\alpha[\nabla\mathbf f(\mathbf x^k)-\nabla\mathbf f(\mathbf x^*)];$$

2. the descent inequality (3.29), for every tunable $\eta>0$;
3. the dual bound (3.35), controlling $\|\mathbf q^{k+1}-\mathbf q^*\|_F^2$ by primal quantities through $\sigma_{\max}$ and the smallest nonzero eigenvalue $\tilde\lambda_{\min}(\tilde W-W)$;
4. the critical inequality (3.30) for every $\delta$ below the explicit minimum (3.38), under $\eta\in(0,2\mu_{\mathbf g})$ and $\alpha L_{\mathbf f}^2<\eta\lambda_{\min}(\tilde W)$ (3.39).

A companion item states Proposition 3.6: $\bar f$ is restricted strongly convex at $x^*$ if and only if $\mathbf g$ is at $\mathbf 1(x^*)^{\mathsf T}$.

Significance

Theorem 3.7 is what separates EXTRA from DGD: a fixed step size gives linear convergence to the exact solution, with the strong convexity requirement placed on $\mathbf g$, not on the individual $f_i$ (Remark 1). By Proposition 3.6 this is the same as restricted strong convexity of the global objective $\bar f$, so agents with merely convex local losses still converge linearly. EXTRA is an early member of the family of exact decentralized methods (gradient tracking, NIDS, exact diffusion), whose linear-rate analyses use Lyapunov functions of the same primal–dual type.

The result is proved in the paper. Neither it nor any other decentralized optimization rate is formalized in Mathlib or on the platform. A formal development would produce a reusable layer for stacked variables, Frobenius geometry, matrix-weighted norms and mixing-matrix assumptions, on which other decentralized algorithms could be stated.

Difficulty

The obvious Lyapunov function $\|\mathbf x^k-\mathbf x^*\|^2$ does not contract: EXTRA is a primal–dual method in disguise, and the primal error alone can increase. The contraction holds only for the joint quantity $\|\mathbf z^k-\mathbf z^*\|_G^2$, and the descent inequality (3.29) controls only the primal part of $\|\mathbf z^{k+1}-\mathbf z^*\|_G^2$. The dual error $\mathbf q^{k+1}-\mathbf q^*$ must be bounded separately. That bound (3.35) works only because $\mathbf q^{k+1}-\mathbf q^*$ lies in the range of $\tilde W-W$, where $\tilde W-W$ is invertible with smallest nonzero eigenvalue $\tilde\lambda_{\min}$. Restricted strong convexity of $\mathbf g$ also gives curvature only toward the single point $\mathbf x^*$, not between arbitrary pairs.

Formalization scope

Stacked variables are Fin n → EuclideanSpace ℝ (Fin p). The sup norm Lean puts on this type is never used: Frobenius quantities go through an explicit inner product frob, and $\|\mathbf x\|_M^2$ is the quadratic form frob x (mix M x), also for indefinite $M$ as in (3.29). $\lambda_{\min}$, $\lambda_{\max}$, $\tilde\lambda_{\min}$ and $\sigma_{\max}$ are pinned by their characterisations (an eigenvalue that is extreme among all eigenvalues). $U$ is any symmetric positive semidefinite matrix with $U^2=\tilde W-W$. Assumptions 1–3 are standing hypotheses of every item except Proposition 3.6, which assumes only Assumptions 1 and 2, as printed. Assumption 2 uses one common Lipschitz constant $L_{\mathbf f}$. The step-size conditions are multiplied out ($\alpha L_{\mathbf f}^2<2\mu_{\mathbf g}\lambda_{\min}(\tilde W)$), so that $L_{\mathbf f}=0$ is not turned into $\alpha<0$ by Lean's $x/0=0$. The gradients of $\bar f$ and $\mathbf g$ are written as explicit formulas.

The goal does not mention $\eta$, $\theta$, the minimum (3.38) or (3.30). A version assuming those intermediate inequalities would be trivial, and so would one with a free $\delta$ allowed to depend on $k$. The printed "In addition" sentence of Proposition 3.6 ($\mu_{\mathbf g}\ge\mu_{\bar f}$) is false; the companion item states the direction proved in Appendix A.

The infrastructure needed is: Frobenius inner products of stacked variables, quadratic-form bounds by extreme eigenvalues, the range/nullspace argument for symmetric positive semidefinite matrices, and the elementary inequality $\|\mathbf a+\mathbf b\|^2\le\theta\|\mathbf a\|^2+\frac{\theta}{\theta-1}\|\mathbf b\|^2$. Proofs of any milestone, and reusable lemmas on matrix-weighted norms, are welcome.

Selected references

• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An Exact First-Order Algorithm for Decentralized Consensus Optimization, SIAM J. Optim. 25(2) (2015) 944–966; arXiv:1404.6264v4. https://arxiv.org/abs/1404.6264
• A. Nedić, A. Ozdaglar, Distributed Subgradient Methods for Multi-Agent Optimization, IEEE Trans. Automat. Control 54(1) (2009) 48–61. https://doi.org/10.1109/TAC.2008.2009515
• K. Yuan, Q. Ling, W. Yin, On the Convergence of Decentralized Gradient Descent, SIAM J. Optim. 26(3) (2016) 1835–1854; arXiv:1310.7063. https://arxiv.org/abs/1310.7063
• M.-J. Lai, W. Yin, Augmented ℓ1 and Nuclear-Norm Models with a Globally Linearly Convergent Algorithm, SIAM J. Imaging Sci. 6(2) (2013) 1059–1091 (the source of the restricted strong convexity notion). https://doi.org/10.1137/120863290