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

Many learning and risk-averse decision problems minimize a function of an expectation that is itself passed through another function: $F(x)=f(g(x))$ with $g(x)=\mathbb E[G(x,\xi)]$. Examples are mean–deviation risk measures, stochastic variational inequalities rewritten as minimization, and policy evaluation in reinforcement learning. Only noisy samples of $g$, of its Jacobian and of $\nabla f$ are available, and the plug-in estimate $\nabla g(x)^\top\nabla f(G)$ of $\nabla F(x)$ is biased because $f$ is nonlinear. Classical stochastic gradient analysis does not apply directly.

Timeline of sample complexities for smooth nonconvex two-level problems, measured by the number of samples needed to reach an $\varepsilon$-stationary point:

• 2017 — Wang, Fang and Liu (Math. Program.) introduce stochastic compositional gradient descent with two time scales; the unconstrained nonconvex rate is $O(\varepsilon^{-4})$ in their measure.
• 2017 — Wang, Liu and Fang (JMLR) accelerate it to $O(\varepsilon^{-2.25})$ for smooth unconstrained problems, still with two time scales.
• 2019–2020 — Ghadimi, Ruszczyński and Wang (arXiv:1812.01094, SIAM J. Optim. 2020) propose NASA, a single-time-scale method with one sample per iteration, and prove $O(\varepsilon^{-2})$ for constrained problems. This mission formalizes that result.

Setting

Problem (1.1) is

$$\min_{x\in X} F(x)=f(g(x)),$$

where $f:\mathbb R^m\to\mathbb R$ and $g:\mathbb R^n\to\mathbb R^m$ are continuously differentiable, $X\subseteq\mathbb R^n$ is closed and convex, and nothing is convex. Assumption 2 asks that $f$, $g$, $\nabla f$, $\nabla g$ be Lipschitz with constants $L_f,L_g,L_{\nabla f},L_{\nabla g}$; then $\nabla F$ is Lipschitz with $L_{\nabla F}=L_g^2L_{\nabla f}+L_fL_{\nabla g}$. $F^*$ is the infimum of $F$ over $X$.

For $\beta>0$ the subproblem solution is $\bar y(x,z,\beta)=\operatorname{argmin}_{y\in X}\{\langle z,y-x\rangle+\frac\beta2\|y-x\|^2\}=\Pi_X(x-z/\beta)$, with $\Pi_X$ the Euclidean projection. A pair $(x,z)$ is judged by the optimality measure

$$V(x,z)=\|\bar y(x,z,1)-x\|^2+\|z-\nabla F(x)\|^2,$$

which vanishes exactly when $z=\nabla F(x)$ and $-\nabla F(x)$ lies in the normal cone to $X$ at $x$.

The NASA method (Algorithm 1) keeps three sequences: iterates $x^k\in X$, gradient averages $z^k$ and value averages $u^k$. With parameters $a,b>0$, regularization $\beta>0$ and stepsizes $\tau_k\in(0,1/a]$:

$$x^{k+1}=x^k+\tau_k(\bar y(x^k,z^k,\beta)-x^k),\quad z^{k+1}=(1-a\tau_k)z^k+a\tau_k[J^{k+1}]^\top s^{k+1},\quad u^{k+1}=(1-b\tau_k)u^k+b\tau_kG^{k+1}.$$

Assumption 1 governs the oracle. Given $\mathcal F_k$, the outputs $G^{k+1}$, $J^{k+1}$ and $s^{k+1}$ are conditionally unbiased for $g(x^{k+1})$, $\nabla g(x^{k+1})$ and $\nabla f(u^k)$. Their second moments are bounded by $\sigma_G^2,\sigma_J^2,\sigma_s^2$, and $s^{k+1}$, $J^{k+1}$ are conditionally independent. The analysis rests on the merit function $W(x,z,u)=a(F(x)-F^*)-\eta(x,z)+\frac\gamma2\|g(x)-u\|^2$, where $\eta$ is the optimal value of the subproblem.

Formalization targets

Goal: Theorem 2(c), (3.37)

With $a=b=1$, $\beta=\big(\frac{(1+\alpha)^2}{\alpha}L_g^2+\frac\alpha4\big)L_{\nabla f}$ for some $\alpha>0$, $\tau_0=1$, $\tau_k=1/\sqrt N$ for $k\ge1$, $N\ge2$, and $R$ uniform on $\{1,\dots,N-1\}$:

$$\mathbb E[V(x^R,z^R)]\le\frac4{\sqrt N-1}\Big(\frac2{\alpha L_{\nabla f}}\big[\max(L_1,L_2)+\max(1,\beta^2)\big]\big[W(x^0,z^0,u^0)+\hat\sigma^2\big]+\sigma_J^2\sigma_s^2\Big).$$

The constants $L_1,L_2$ (3.32) and $\hat\sigma^2$ are explicit in the problem data. This is the paper's headline rate, and every other statement of the mission feeds it.

Milestones

1. Lemma 1: $\|\bar y(x,z,1)-x\|\le\max(1,\beta)\|\bar y(x,z,\beta)-x\|$.
2. Lemma 2: $\nabla F$ is $L_{\nabla F}$-Lipschitz.
3. Lemma 3: $\eta$ has an $L_{\nabla\eta}$-Lipschitz gradient in $(x,z)$.
4. (3.21): $\langle z,d\rangle+\beta\|d\|^2\le0$ for the subproblem step $d$.
5. Lemma 4: the pathwise descent inequality $c\sum\tau_k(\|d^k\|^2+\|g(x^k)-u^k\|^2)\le W(x^0,z^0,u^0)+\sum r^{k+1}$.
6. Proposition 1(a): moment bounds on $z^k$ and $d^k$.
7. Proposition 1(b): $\sum\mathbb E[r^{k+1}]\le\hat\sigma^2\sum\tau_k^2$.
8. (3.29): $V(x,z)\le\max(1,\beta^2)\|d\|^2+\|z-\nabla F(x)\|^2$.
9. Theorem 2(a): the weighted gradient-tracking error.
10. Theorem 2(b): the bound on $\mathbb E[V(x^R,z^R)]$ for general admissible stepsizes.

Significance

The result. Theorem 2(c) gives $\mathbb E[V(x^R,z^R)]\le\varepsilon$ after $O(\varepsilon^{-2})$ iterations with one oracle call each. That matches the complexity of stochastic gradient descent on single-level smooth nonconvex problems, so the nested structure costs only constants. The bound holds with constraints, and $z^R$ comes with a certified estimate of $\nabla F(x^R)$. The same merit-function technique underlies later single-time-scale methods for multi-level and conditional stochastic optimization.

Formalizing it. The result is proved on paper, not formalized. A machine-checked proof requires the whole chain, Lemma 4 through Theorem 2, to be stated with constants that the argument actually supports. Several printed constants do not meet that bar (see Formalization scope), so the formalization also certifies a corrected version of the theorem. The deterministic milestones (Lemmas 1–3, (3.21), (3.29)) are general facts about Euclidean projections and value functions of strongly convex subproblems, and other projected-gradient developments can reuse them.

Difficulty

The obvious approach fails. Analyzing $F(x^k)$ alone does not work because the step uses $z^k$, a biased and correlated estimate of $\nabla F(x^k)$, and its error does not vanish at a single time scale. The analysis instead tracks the coupled potential $W$. Each of its three terms needs a different tool: the descent lemma for $F$, the smoothness of the value function $\eta$ (Lemma 3, which needs differentiability of a parametric minimum), and a recursion for $u^k$. These pieces must combine under the single coupling condition (3.16). The probabilistic part is delicate as well. The cross terms vanish only in expectation, they require conditional independence of $J^{k+1}$ and $s^{k+1}$, and their integrability is not automatic. Theorem 2(a) adds a weighted unrolling of the $z$-recursion through the products $\Gamma_k$ and the summation condition (3.30).

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). Jacobians are continuous linear maps with the operator norm, and $\nabla g(x)^\top$ is the adjoint. The projection is a function $P$ with the published predicate SpectralProjGrad.Shared.IsProjOnto X P, and $\bar y(x,z,\beta)=P(x-\beta^{-1}z)$. $\eta$ is the subproblem objective evaluated at $\bar y$, and Lemma 3 places $(x,z)$ in the $L^2$ product WithLp 2 (ℝⁿ × ℝⁿ). $F^*$ is sInf over $X$, and $F$ is assumed bounded below on $X$. The regularization $\beta_k\equiv\beta$ and the stepsizes are deterministic.

The randomness lives on a standard Borel probability space. Assumption 1 is stated with respect to any filtration to which $x^k,z^k,u^k$ are adapted, which includes the paper's natural filtration. It requires square-integrable oracle outputs, so that no conditional-expectation hypothesis is vacuous. Statements printed with conditional expectations on the left and constants on the right (Proposition 1, Theorem 2(a)) are stated in total expectation, which is what the proofs establish. Every conclusion about an expectation includes the integrability of the integrand, so a bound cannot hold because a non-integrable integral defaults to $0$. $\mathbb E[V(x^R,z^R)]$ is the $\tau$-weighted average of $\mathbb E[V(x^k,z^k)]$ over $k=1,\dots,N-1$ (3.34). Lemma 4 is deterministic: it holds along every path of the recursions, whatever the oracle outputs. The recursions tie $y^k$ to the projection and $z^k,u^k$ to the oracle outputs, so the goal cannot be satisfied by arbitrary sequences or by a vacuous oracle.

Corrections to printed constants, each stated in the item's Formalization Note:

• (3.18): the noise term of $r^{k+1}$ carries $\gamma b^2$, not $b^2$. The printed Lemma 4 has a counterexample.
• (3.26): $\hat\sigma^2$ uses $aL_{\nabla F}$, $\max(\sigma_J^2\sigma_s^2,\|z^0\|^2)/\beta^2$ (the $k=0$ term) and $\gamma b^2\sigma_G^2$.
• (3.33): the coefficient of $\max(1,\beta^2)\hat\sigma^2$ is $1/c$, not $a\bar c/c$. The two agree when $a\bar c=1$.
• (3.37): the denominator is $\alpha L_{\nabla f}$, not $\alpha L_{\nabla F}$, since the proof sets $c=\alpha L_{\nabla f}/4$. The proof also fixes $\gamma=\alpha L_{\nabla f}$ in $W$ and $\hat\sigma^2$.
• Proposition 1(a): the bound $\mathbb E\|z^k\|^2\le\sigma_J^2\sigma_s^2$ is false conditionally on $\mathcal F_{k-1}$ and is stated in expectation.
• Hypotheses the proofs use but the statements omit: $\tau_k\le1$, $b\tau_k\le1$, $a\beta\ge c$ and $\gamma b\ge2c$, $\tau_0=1/a$ (Theorem 2(a),(b)), $N\ge2$, and $L_{\nabla f}>0$.

The second claim (3.38) of Theorem 2(c) is excluded: its printed constant is smaller than what the proof gives. Theorem 3 (asymptotics) and the ASA variant of §4 are out of scope. Contributions are welcome at every milestone. Solvers will need Euclidean projection characterizations, differentiability of the squared distance to a convex set, conditional-independence product rules for conditional expectations, and Abel-type summation for the $\Gamma_k$ weights.

Selected references

• S. Ghadimi, A. Ruszczyński, M. Wang, A Single Time-Scale Stochastic Approximation Method for Nested Stochastic Optimization, arXiv:1812.01094v2, 2019; SIAM J. Optim. 30(1), 2020. https://arxiv.org/abs/1812.01094
• M. Wang, E. X. Fang, H. Liu, Stochastic compositional gradient descent: algorithms for minimizing compositions of expected-value functions, Math. Program. 161, 2017. https://doi.org/10.1007/s10107-016-1017-3
• M. Wang, J. Liu, E. X. Fang, Accelerating stochastic composition optimization, JMLR 18(105), 2017. https://jmlr.org/papers/v18/16-504.html
• S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
• A. Ruszczyński, Nonlinear Optimization, Princeton University Press, 2006.

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

Why trade credit terms matter

Most business-to-business sales are not paid in cash on delivery. The supplier lets the buyer pay later, which is trade credit, and often offers a discount for paying early. In the classic "2/10 net 30" the buyer gets 2% off for paying within 10 days and otherwise owes the full price in 30 days. Trade credit is a major source of short-term finance for firms. Empirical work documents both forms of contract: net terms, with one price and no discount, and two-part terms, with an early-payment discount. The discounts are large, and they vary a lot from one buyer to another (Petersen and Rajan 1997; Klapper, Laeven and Rajan 2012). The implied interest rate on a forgone discount is often far above a bank loan's. This raises two questions: why do cash-poor buyers use trade credit at all, and when should a supplier offer a discount?

Yang and Birge (Management Science 2018) answer this in a supplier–retailer model with a financially constrained retailer, who can finance inventory with a bank loan, with trade credit, or with both. Their answer is risk sharing. Trade credit is repaid out of realized sales, so the supplier bears part of the demand risk. She can therefore induce a larger order than a price-only contract does. The model builds on the selling-to-the-newsvendor model of Lariviere and Porteus (2001), and it complements the supplier-versus-bank analysis of Kouvelis and Zhao (2012). This mission formalizes the paper's main result on the structure of the optimal contract.

The model

A retailer buys a single good from a supplier at unit cost $c$ and sells it at unit price $p=1$. Demand is random with density $f$ on $[0,\infty)$. Its distribution function is $F(x)=\int_0^x f$, the complementary distribution function is $\bar F=1-F$, the failure rate is $h=f/\bar F$, and the generalized failure rate is $g(x)=x\,h(x)$. Demand has an increasing failure rate (IFR). The retailer has cash $K>0$.

The supplier offers a cash price $w_c$ and a credit price $w_t$, with $c\le w_c\le w_t\le 1$. The early-payment discount is $d_t=1-w_c/w_t$. If the retailer's cash does not cover his cash purchases, he borrows from a competitive bank. The bank loan is senior to trade credit. A bank and a supplier recovering a defaulted claim lose fractions $\alpha_b$ and $\alpha_t$ of what they recover, with $\alpha_b,\alpha_t\in[0,1]$.

Default is described by two thresholds. The bank-loan default threshold $\theta_b$ is the demand below which the bank is not repaid in full, and it equals the amount owed to the bank. The trade-credit default threshold $\theta_t\ge\theta_b$ is the demand below which the supplier is not repaid in full. The retailer uses a bank loan iff $\theta_b>0$, and uses trade credit iff $\theta_t>\theta_b$.

The paper shows (p. 13) that the supplier's problem can be written in the thresholds alone. Let

$$\hat F_b(x)=\bar F(x)[1-\alpha_b g(x)],\qquad C(\theta)=\frac{K+\int_0^\theta\hat F_b}{\hat F_b(\theta)}-\theta,$$ $$Q(\theta_b,\theta_t)=\min\{q\ge0:\ q\bar F(q)=[\theta_t+C(\theta_b)]\bar F(\theta_t)\}.$$

The retailer orders $Q$, the prices are $w_t=\bar F(Q)/\bar F(\theta_t)$ and $w_c=\hat F_b(\theta_b)w_t$, and the discount is $d_t=1-\hat F_b(\theta_b)$. The supplier's expected profit is

$$\Pi_s=K+\int_0^{\theta_t}\bar F(x)\,dx-c\,Q(\theta_b,\theta_t)-\Big[\alpha_b\int_0^{\theta_b}x\,dF(x)+\alpha_t\int_{\theta_b}^{\theta_t}(x-\theta_b)\,dF(x)\Big].$$

She maximizes $\Pi_s$ over a domain $\Theta$ of thresholds. A maximizer is an optimal trade credit contract. Net terms correspond to $\theta_b^*=0$, which is $d_t^*=0$. Two-part terms correspond to $\theta_b^*>0$.

Formalization targets

Goal: Proposition 3 (p. 15)

For every optimal contract $(\theta_b^*,\theta_t^*)$:

$$\theta_t^*>0\ \Longrightarrow\ \theta_b^*<\theta_t^*\qquad(\text{trade credit is always used}).$$

If $\alpha_t=0$, or if $K$ is sufficiently large, then $\theta_b^*=0$ and $d_t^*=0$ (net terms, no bank loan). If $\alpha_t>0$ and $K$ is sufficiently small, then

$$0<\theta_b^*<\theta_t^*,\qquad d_t^*>0\qquad(\text{two-part terms, both bank loan and trade credit}).$$

"Sufficiently large" and "sufficiently small" are existential thresholds on $K$ that depend on the data $(f,c,\alpha_b,\alpha_t)$, not on the contract.

Milestones

They are listed in the order the proof uses them:

1. Lemma C.4: $C$ is increasing, and convex when $\alpha_b=0$.
2. Corollary 3: $Q$ increases in $\theta_b$ and in $\theta_t$.
3. Lemma C.8: at $\alpha_b=0$, $\Pi_s$ is concave in $\theta_b$.
4. Lemma C.7: $Q$ increases in $\alpha_b$ and $K$.
5. Lemma C.9: $\Pi_s$ is concave in $\theta_t$.
6. Proposition 6, first sentence: $\Pi_s^*$ decreases in $\alpha_b$ and $\alpha_t$.

Significance

Proposition 3 is the paper's prediction about inventory financing portfolios. Once the supplier sets the terms, a retailer who needs external financing always uses trade credit. Early-payment discounts appear only when supplier default is costly and the retailer is cash-poor. A discount is then the supplier's way of moving part of the financing to the bank. The paper uses this to explain why discounts go to small, risky buyers, as observed by Klapper et al. (2012). The comparative statics of §5 (Propositions 4–6) are built on the same reduced problem.

The result is proved on paper but has not been formalized. The appendix lemmas it rests on (C.4, C.7, C.8, C.9) are stated without proof ("available upon request"). A machine-checked development would therefore settle whether these lemmas hold on the domain where the paper uses them. It would also produce a reusable library: IFR demand with failure rates, the bank-loan pricing kernel $\hat F_b$, and the implicit order quantity $Q$.

Difficulty

The order quantity $Q$ is defined implicitly, as the smaller root of a unimodal equation, and the paper's arguments differentiate through it with the implicit function theorem. Every derivative of $\Pi_s$ therefore involves $1/(\bar F(Q)[1-g(Q)])$, which blows up at the edge of $\Theta$ where $Q=g^{-1}(1)$. The density is only assumed continuous, so $\hat F_b$ and $C$ need not be differentiable when $\alpha_b>0$. Monotonicity and concavity have to be argued from the integral forms, or under a smoothness assumption the paper does not state.

The obvious argument for "sufficiently large $K$" also fails. It perturbs the optimum at $K$ just below $M^*=g^{-1}(1)\bar F(g^{-1}(1))$, but there the domain shrinks to a sliver near $\theta_t=0$, and the derivative of $\Pi_s$ in $\theta_t$ at $\theta_t=0$ can be negative. For exponential demand it tends to $-\infty$ as $K\to M^*$. The proof's claim that $\theta_t^*>0$ there is not part of the theorem. Part 1 for general $\alpha_b$ is reduced to $\alpha_b=0$ through Proposition 6, which requires comparing optima over domains that themselves depend on $\alpha_b$.

Formalization scope

All objects live in TradeCredit.Terms.Model.

Demand. Demand is a density $f:\mathbb R\to\mathbb R$ that is continuous on $[0,\infty)$, positive on $[0,\infty)$, zero on $(-\infty,0)$, integrable with total mass $1$, and has a weakly increasing failure rate on $[0,\infty)$. $F$ is the interval integral of $f$ from $0$. The normalizations are $p=1$ and $s=0$. The parameters satisfy $0<c<1$, $\alpha_b,\alpha_t\in[0,1]$ and $K>0$.

Domain. $\Theta$ is the printed set of Corollary 3 ($\theta_t\ge\theta_b\ge0$ and $[\theta_t+C(\theta_b)]\bar F(\theta_t)\le M^*$) plus two pinned constraints: $\theta_t\le Q(\theta_b,\theta_t)$ (that is, $w_t\le1$) and $c\le w_c$. These are the image under (11) of §3.1's $c\le w_c\le w_t\le 1$, which the printed $\Theta$ omits.

Statements. $Q$ is the infimum of the nonnegative roots. "The optimal contract" means every maximizer of $\Pi_s$ on $\Theta$. Existence of a maximizer is not asserted; the paper does not prove it. Monotonicity is weak, and concavity is Mathlib's ConcaveOn on the sections of $\Theta$. Proposition 6 is stated by comparing attained values with $\Pi_s^*=\sup_\Theta\Pi_s$.

Not in scope. The retailer's best response (Proposition 1) and the bijection between thresholds and contracts are not formalized. The goal is about the paper's own reduced problem. Lemma 1's first-order conditions are not a milestone: as printed they fail at a corner optimum $\theta_b^*=\theta_t^*=0$, and they need $C'$, which is not defined under a merely continuous density.

Ruling out trivialization. The large-$K$ clause quantifies over $K\in[\underline K,M^*)$ with $\underline K<M^*$. For $K\ge M^*$ the domain $\Theta$ has no point with $\theta_t>0$ and every "for every optimal contract" statement holds vacuously, so a large-$K$ clause that reached only those values would be empty.

Welcome contributions. Lemmas on IFR densities (positivity of $\bar F$, finiteness of the mean, monotonicity of $g$ and existence of $g^{-1}(1)$), the root structure of $q\bar F(q)$, and boundedness of $\Pi_s$ on $\Theta$ are reusable beyond this paper.

Source. The source PDF is the authors' accepted manuscript (LBS Research Online, eprint 801). All page numbers are the manuscript's.

Selected references

• S. A. Yang, J. R. Birge, Trade Credit, Risk Sharing, and Inventory Financing Portfolios, Management Science 64(8), 2018. https://doi.org/10.1287/mnsc.2017.2799
• M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4), 2001. https://doi.org/10.1287/msom.3.4.293.9971
• P. Kouvelis, W. Zhao, Financing the Newsvendor: Supplier vs. Bank, and the Structure of Optimal Trade Credit Contracts, Operations Research 60(3), 2012. https://doi.org/10.1287/opre.1120.1040
• M. A. Petersen, R. G. Rajan, Trade Credit: Theories and Evidence, Review of Financial Studies 10(3), 1997. https://doi.org/10.1093/rfs/10.3.661
• L. Klapper, L. Laeven, R. Rajan, Trade Credit Contracts, Review of Financial Studies 25(3), 2012. https://doi.org/10.1093/rfs/hhr122

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