Operations Research

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Corollary 3.4

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

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

and, if (2.10) holds,

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

Betweenness centrality measures how much of the communication in a network passes through a node. Freeman's original measure (Freeman 1977) counts the fraction of shortest paths between each pair of nodes that pass through it, and Brandes' algorithm (Brandes 2001) made it computable on large graphs. Variants replace shortest paths by maximum flows (Freeman, Borgatti and White 1991), random walks (Newman 2005) or load-splitting rules (Goh, Kahng and Kim 2001), and group variants measure the traffic that passes through a set of nodes (Everett and Borgatti 1999).

Dolev, Elovici and Puzis (technical report 2009, J. ACM 2010) define routing betweenness centrality (RBC): given the actual routing scheme of a communication network and its traffic matrix, the RBC of a node is the expected number of packets that pass through it. Each of the measures above is a special choice of routing scheme. The application is the placement of traffic monitors: the RBC of an ordered sequence of monitors is the expected number of packets sampled by all of them in order, which measures, for example, redundant inspection along a path.

Setting

Let $V$ be a finite set of nodes. A routing scheme assigns to every source $s$, current node $u$, next node $v$ and target $t$ a number $R(s,u,v,t)$, the probability that $u$ forwards to $v$ a packet with source address $s$ and target address $t$. Routing decisions are independent. The scheme is assumed to be

• nonnegative;
• total: every node $u\ne t$ forwards a packet targeted at $t$ with total probability one, $\sum_v R(s,u,v,t)=1$, and the target forwards nothing;
• loop-free: for every pair $(s,t)$ the directed graph with an arc $a\to b$ whenever $R(s,a,b,t)>0$ is acyclic;
• source-oblivious where stated: $R(s,u,v,t)$ does not depend on $s$.

A route from $s$ to $t$ is a sequence of nodes from $s$ to $t$ whose every hop has positive forwarding probability; its probability is the product of the hop probabilities. For nodes $s,t,v$ and a sequence $S=(s_1,\dots,s_k)$:

• the pairwise dependency $\delta_{s,t}(v)$ is the total probability of the routes from $s$ to $t$ that visit $v$;
• the sequence dependency $\tilde\delta_{s,t}(S)$ is the total probability of the routes from $s$ to $t$ that visit $s_1$, then $s_2$, …, then $s_k$ (consecutive repetitions in $S$ collapsed).

A traffic matrix $T(s,t)$ gives the number of packets sent from $s$ to $t$, and sampling rates $\rho_v\in[0,1]$ give the fraction of passing packets a monitor at $v$ samples. The target dependency is $\delta_{\bullet,t}(v)=\sum_{s}\delta_{s,t}(v)T(s,t)$, and the RBC of the sequence $S_\rho$ of distinct nodes is

$$\tilde\delta_{\bullet,\bullet}(S_\rho)=\prod_{r\in S}\rho_r\cdot\sum_{s,t\in V}\tilde\delta_{s,t}(S)\,T(s,t).$$

Formalization targets

Goal: sequence RBC as a sum over targets of chained dependencies

For a source-oblivious scheme and a sequence $S=(s_1,\dots,s_k)$ of distinct nodes, $k\ge1$,

$$\prod_{r\in S}\rho_r\cdot\sum_{s,t\in V}\tilde\delta_{s,t}(S)\,T(s,t)=\sum_{t\in V}\delta_{\bullet,t}(s_1)\,\rho_{s_1}\prod_{i=1}^{k-1}\delta_{s_i,t}(s_{i+1})\,\rho_{s_{i+1}}.$$

The right side is the value returned by the paper's Algorithm 6. The identity contains no running time and no constant: it states the exact equality the algorithm relies on.

Milestones

1. Proposition 1: for a loop-free scheme (not necessarily source-oblivious), two different orderings of the same set of nodes cannot both have positive sequence dependency.
2. Lemma 1 (Dependency chaining): for $s\ne t$, $\tilde\delta_{s,t}((s_1,\dots,s_k))=\delta_{s,t}(s_1)\cdot\tilde\delta_{s_1,t}((s_2,\dots,s_k))$.
3. Eq. (16): for $s\ne t$, $\tilde\delta_{s,t}((s_1,\dots,s_k))=\delta_{s,t}(s_1)\prod_{i=2}^k\delta_{s_{i-1},t}(s_i)$.
4. Eq. (17): $\tilde\delta_{\bullet,t}((s_1,\dots,s_k))=\delta_{\bullet,t}(s_1)\prod_{i=2}^k\delta_{s_{i-1},t}(s_i)$.
5. Eq. (1) (off the goal's path): $\delta_{s,t}(s)=1$ and $\delta_{s,t}(v)=\sum_{u}\delta_{s,t}(u)R(s,u,v,t)$ for $v\ne s$, the sum over predecessors $u$ of $v$.
6. Eq. (9) (off the goal's path): $\delta_{\bullet,t}(v)=T(v,t)+\sum_u\delta_{\bullet,t}(u)R(\oslash,u,v,t)$ for source-oblivious schemes.

Significance

The goal reduces the RBC of a sequence of $k$ monitors to $O(nk)$ arithmetic on precomputed single-node quantities, instead of a pass over the routing graph of every source–target pair. This is what makes repeated evaluation of candidate monitor sequences, as in greedy or search-based placement, affordable on large networks. Eqs. (1) and (9) are the recursions behind the paper's algorithms for the RBC of single nodes; Eq. (9) replaces the loop over all source–target pairs by a loop over targets.

The paper's proof of Lemma 1 is an argument about conditional probabilities of informally described events. A formalization fixes what "the probability that a packet passes through $S$" means, as a sum over a finite set of routes, and checks the factorization against that definition, including the corner cases the prose passes over: sequences with repeated nodes, a first node equal to the source or to the target, and the source $s=t$ in the sum over all sources. No machine-checked version of these identities is known.

Difficulty

Dependency chaining is a Markov property: after the packet reaches $s_1$, its future does not depend on its past. The obvious argument splits every route through $s_1$ into a prefix ending at $s_1$ and a suffix starting there. Two points need care. First, the suffix must be a route of a packet with source $s_1$, which is where source-obliviousness enters; for source-dependent routing the lemma is false. Second, the prefix probabilities must sum to $\delta_{s,t}(s_1)$ while the suffix probabilities sum to one, which requires that no packet is lost: this is where totality of the forwarding probabilities and loop-freeness (every walk reaches the target in at most $|V|$ steps) are needed. The passage from Lemma 1 to the goal then requires the sum over all sources, including $s=t$, where Lemma 1 does not apply.

Formalization scope

Nodes form a type V with [Fintype V] [DecidableEq V]; probabilities, traffic and sampling rates are real numbers; sequences are Lean lists, indexed from $0$. Routes are repetition-free lists, and every dependency is a finite sum over them; no infinite sums, suprema or measure theory are used. The definitions file bundles the standing assumptions in IsRoutingScheme and source-obliviousness in IsSourceOblivious.

The paper's probabilities are informal. The following readings are explicit:

• every non-target node forwards with total probability one (implicit in the paper; without it Lemma 1 fails);
• the target forwards nothing;
• the paper's convention $R(\oslash,v,v,\oslash)=1$ is not adopted (it contradicts loop-freeness); collapsing consecutive repetitions in $S$ reproduces its only use;
• the "don't care" source $\oslash$ of Eq. (9) is an arbitrary fixed node, harmless under source-obliviousness;
• the printed index slips in Eqs. (16) and (17) are corrected;
• no sign condition is imposed on $T$; $0\le\rho_v\le1$ is kept in the goal as on the page.

Defining $\tilde\delta$ by the recursion (3) or the product (16), the target sequence dependency by (17), or the sequence RBC as the sum over targets of the chained product would make the goal true by definition; every dependency here is a sum of route probabilities, and the RBC of a sequence is the double sum of Eq. (4).

The running-time claims of the paper are out of scope. Lemma 2 of the paper (p. 17) is false as printed for a nonempty monitor set and is not posed. Contributions welcome: proofs of the milestones, a general lemma that the total route probability from any node is one under a total loop-free scheme (reusable for absorbing Markov chains on finite DAGs), and the prefix–suffix decomposition of routes.

Selected references

• S. Dolev, Y. Elovici, R. Puzis, Routing Betweenness Centrality, Technical Report #2009-09, Ben-Gurion University of the Negev, 2009; J. ACM 57(4), 2010. https://doi.org/10.1145/1734213.1734219
• L. C. Freeman, A set of measures of centrality based on betweenness, Sociometry 40(1), 1977. https://doi.org/10.2307/3033543
• U. Brandes, A faster algorithm for betweenness centrality, J. Math. Sociology 25(2), 2001. https://doi.org/10.1080/0022250X.2001.9990249
• L. C. Freeman, S. P. Borgatti, D. R. White, Centrality in valued graphs: a measure of betweenness based on network flow, Social Networks 13, 1991. https://doi.org/10.1016/0378-8733(91)90017-N
• M. E. J. Newman, A measure of betweenness centrality based on random walks, Social Networks 27, 2005. https://doi.org/10.1016/j.socnet.2004.11.009
• K.-I. Goh, B. Kahng, D. Kim, Universal behavior of load distribution in scale-free networks, Phys. Rev. Lett. 87, 2001. https://doi.org/10.1103/PhysRevLett.87.278701
• M. G. Everett, S. P. Borgatti, The centrality of groups and classes, J. Math. Sociology 23(3), 1999. https://doi.org/10.1080/0022250X.1999.9990219

Motivation

Bounded-confidence opinion dynamics model a population in which each agent repeatedly moves its opinion towards the opinions of those agents whose views lie within a fixed distance of its own. Introduced in discrete time by Krause (1997) and studied as the Hegselmann–Krause model, these systems are a standard test case for multi-agent coordination with state-dependent communication: who talks to whom depends on the current state, so the interaction graph changes over time and the linear consensus theory does not apply. Simulations show that opinions settle into clusters that are further apart than the confidence radius, and that the distances between clusters are larger than the radius would force. Explaining those distances is a long-standing question in the area (Lorenz 2007).

Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 2010) study the continuous-time version, first for finitely many agents and then for a continuum of agents. The continuum model is the limit of a large population and captures the intercluster distances observed in simulations. This mission formalizes the continuum part of the paper, Section 3: well-posedness for regular initial opinions, convergence to clusters, and the intercluster distance bound of Theorem 6.

Setting

Agents are indexed by $I=[0,1]$ with Lebesgue measure. An opinion function $\tilde x : I\to\mathbb R$ gives the opinion $\tilde x(\alpha)$ of agent $\alpha$. Write $Y$ for the bounded measurable opinion functions and $X$ for the nondecreasing bounded ones. For $m,M>0$, $X_m$ is the set of $\tilde x\in X$ whose increase rate $\frac{\tilde x(\beta)-\tilde x(\alpha)}{\beta-\alpha}$ is at least $m$ for all $\beta\ne\alpha$, and $X^M$ the set with rate at most $M$. A function is regular if it lies in $X_m^M=X_m\cap X^M$ for some $m,M>0$; the uniform profile $\tilde x(\alpha)=\alpha$ is regular.

Two agents are connected when their opinions differ by less than $1$. The interaction operator is

$$\mathcal L(\tilde x)(\alpha)=\int_0^1 \chi_{\tilde x}(\alpha,\gamma)\bigl(\tilde x(\gamma)-\tilde x(\alpha)\bigr)\,d\gamma,\qquad \chi_{\tilde x}(\alpha,\gamma)=\mathbf 1\bigl[|\tilde x(\alpha)-\tilde x(\gamma)|<1\bigr].$$

Given an initial condition $\tilde x_0$, a solution of (3.2) is a measurable $x : I\times[0,\infty)\to\mathbb R$, $(\alpha,t)\mapsto x_t(\alpha)$, with each $x_t\in Y$ and

$$x_t(\alpha)=\tilde x_0(\alpha)+\int_0^t \mathcal L(x_\tau)(\alpha)\,d\tau\qquad\text{for every } t\ge 0 \text{ and every }\alpha\in I .$$

The differential form (3.1) is $\frac{d}{dt}x_t(\alpha)=\mathcal L(x_t)(\alpha)$.

$F$ is the set of nondecreasing $\tilde s$ whose distinct values are pairwise more than $1$ apart; $\bar F$ the set of nondecreasing $\tilde s$ whose values, for almost every pair of agents, are equal or at least $1$ apart. A fixed point is an $\tilde s\in X$ for which (3.2) started at $\tilde s$ has the unique solution $x_t=\tilde s$. A cluster of $\tilde s$ is a value $A$ held by a set of agents of positive measure $W_A$, its weight.

Formalization targets

Goal: Theorem 6

For a regular $\tilde x_0$, a solution $x$ of (3.2), and $\tilde s=\lim_{t\to\infty}x_t$ almost everywhere: any two distinct clusters $A\ne B$ of $\tilde s$ satisfy

$$|B-A|\ \ge\ 1+\frac{\min\{W_A,W_B\}}{\max\{W_A,W_B\}},$$

and $\tilde s$ agrees almost everywhere with a member of $F$ that is a fixed point.

Milestones

1. Lemma 1: $\|\mathcal L(\tilde x)-\mathcal L(\tilde y)\|_\infty\le(2+8/m)\|\tilde x-\tilde y\|_\infty$ for $\tilde x\in X_m$, $\tilde y\in Y$.
2. Lemma 2: $-(\tilde x(\beta)-\tilde x(\alpha))\le\mathcal L(\tilde x)(\beta)-\mathcal L(\tilde x)(\alpha)$, and $\le\frac 2m(\tilde x(\beta)-\tilde x(\alpha))$ on $X_m$.
3. Theorem 4: for $\tilde x_0\in X_m^M$, (3.1) and (3.2) have a unique common solution, with $\frac{x_t(\beta)-x_t(\alpha)}{\beta-\alpha}\ge me^{-t}$ and $x_t$ regular for every $t$.
4. Lemma 3: for a nondecreasing solution, $\int_0^c x_t$ converges for every $c$.
5. Proposition 2: $x_t(\alpha)$ converges outside a countable set of agents.
6. Proposition 3(a)–(c): a.e. limits lie in $\bar F$; $F$ consists of fixed points; nondecreasing fixed points lie in $\bar F$.
7. Theorem 5: $x_t\to\tilde y\in\bar F$ almost everywhere, and $F\subseteq\{\text{fixed points}\}\subseteq\bar F$.

Significance

Theorem 6 turns the qualitative picture "opinions freeze into clusters at least one unit apart", which already follows from Theorem 5, into a quantitative statement depending on the cluster weights: two clusters of equal weight are at least $2$ apart, and a light cluster can sit closer to a heavy one. This matches the intercluster distances observed in simulations of large populations and yields Corollary 1 of the paper, a necessary condition for the stability of an equilibrium in the $L^1$ sense. Theorem 4 is of independent interest: the right-hand side of (3.1) is discontinuous in the state, a two-valued initial profile admits two different solutions, and well-posedness holds only under the slope bounds.

The results are proved in the paper. Nothing in this mission has a machine-checked proof yet. Formalizing it means building a small theory of integral equations with a state-dependent, discontinuous kernel on $L^\infty$-type spaces of opinion profiles: a contraction argument on short intervals, its continuation, monotone convergence of partial integrals, and an a.e. limit argument with Fatou's lemma and Fubini.

Difficulty

The obvious route to Theorem 4, Picard–Lindelöf, fails: $\mathcal L$ is not Lipschitz on $Y$, because a small perturbation of opinions can switch the connection indicator on a set of positive measure. Lemma 1 restores the Lipschitz property only at functions with a positive increase rate, so existence and uniqueness require a contraction on a carefully chosen set of profiles together with a proof that the dynamics keep the increase rate positive (Lemma 2), and a continuation argument whose step size shrinks as the lower slope decays. For Theorem 6, convergence alone gives only $|B-A|\ge 1$; the extra $\min/\max$ term comes from agents trapped between two clusters, whose existence relies on the continuity in $\alpha$ of every $x_t$, which the a.e. limit $\tilde s$ does not have.

Formalization scope

Opinion functions are ℝ → ℝ, and only their values on Set.Icc 0 1 matter; a trajectory is x : ℝ → ℝ → ℝ with x t α $=x_t(\alpha)$, time real with $t\ge0$. Lebesgue measure on $I$ is volume.restrict (Set.Icc 0 1), and $\bar F$ uses its product measure. The slope conditions are written multiplied out for $\alpha<\beta$. Explicit readings of the paper's phrases:

• "solution of (3.2)": joint measurability on $I\times[0,\infty)$, $x_t\in Y$, integrability of $\tau\mapsto\mathcal L(x_\tau)(\alpha)$ on $[0,t]$ (implicit in the paper), and the equation for every $t\ge0$ and every $\alpha\in I$ (footnote 6), not almost every $\alpha$.
• "the solution": any solution; Theorem 4 makes it unique.
• "converges": Tendsto … atTop (𝓝 l) to a real limit; "except possibly for a countable set": a countable exceptional set; "a.e.": almost everywhere for Lebesgue measure on $I$.
• "$\tilde y\in\bar F$" and "$\tilde s\in F$" for an a.e.-defined limit: some representative equal almost everywhere belongs to the set.
• "any two clusters": two distinct values of positive weight; weights are measures of level sets.
• "fixed point": existence and uniqueness of the constant solution.
• Theorem 4's printed upper bound $Me^{4t/m}$ is replaced by "$x_t$ is regular for every $t$", because the paper's proof establishes the printed constant only on the first time interval; the lower bound $me^{-t}$ is kept.

A trivializing formalization is ruled out: clusters are distinct with positive weight, regularity requires a positive lower slope, the solution predicate forbids the junk value of a non-integrable time integral, and $\tilde x(\alpha)=\alpha$ is checked to be regular, so no hypothesis is vacuous.

The development needs an integral-equation solution theory for a discontinuous kernel, the Banach fixed point theorem (Mathlib ContractingWith), Grönwall-type estimates, countability of discontinuities of monotone functions, Fatou's lemma and Fubini. Lemmas 1 and 2 and the lower bound in Theorem 4 are reused by the companion mission on the discrete-to-continuum approximation (Theorem 7). Contributions are welcome on every milestone, and in particular on the slope estimates, which are self-contained.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188
• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, On Krause's multi-agent consensus model with state-dependent connectivity, IEEE Trans. Automat. Control 54(11), 2009, 2586–2597. https://doi.org/10.1109/TAC.2009.2031211
• J. Lorenz, Continuous opinion dynamics under bounded confidence: A survey, Internat. J. Modern Phys. C 18(12), 2007, 1819–1838. https://doi.org/10.1142/S0129183107011789
• U. Krause, Soziale Dynamiken mit vielen Interakteuren. Eine Problemskizze, in Modellierung und Simulation von Dynamiken mit vielen interagierenden Akteuren, Bremen, 1997, 37–51.

Motivation

Many problems in statistical learning, signal processing and distributed optimization minimize a sum of a large number $m$ of convex components over a convex set: a data-fit term per sample plus a regularizer or constraint per sample. When $m$ is large, a method that processes one component per iteration is often far cheaper per step than one that evaluates the whole sum. Incremental methods do exactly this. The incremental subgradient method of Nedić and Bertsekas (SIAM J. Optim., 2001) takes a subgradient step on one component at a time; the incremental proximal method replaces some of these steps by proximal steps, which are more stable and are cheap when a component has a closed-form proximal map (an $\ell_1$ term, an indicator of a simple set).

Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization (Report LIDS-P-2847, MIT, 2010, revised 2011; Math. Program. 129 (2011), doi:10.1007/s10107-011-0472-0), combines the two: each component is split as $F_i=f_i+h_i$, with a proximal step on $f_i$ and a subgradient step on $h_i$, followed by a projection. The paper analyzes two ways of choosing the component at each iteration, a fixed cyclic order and a randomized order. This mission covers the randomized order (§4 of the paper); its companion mission covers the cyclic order.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty closed convex set and let $f_i,h_i:\mathbb R^n\to\mathbb R$, $i=1,\dots,m$, be convex. The problem is

$$\text{minimize } F(x)=\sum_{i=1}^m\bigl(f_i(x)+h_i(x)\bigr)\quad\text{subject to } x\in X,$$

with optimal value $F^*=\inf_{x\in X}F(x)$, possibly $-\infty$, and optimal set $X^*=\{x^*\in X\mid F(x^*)=F^*\}$, possibly empty. $P_X$ is the Euclidean projection on $X$ and $\tilde\nabla f(x)$ a subgradient of $f$ at $x$.

At iteration $k$ a component index $\omega_k\in\{1,\dots,m\}$ is drawn and, with stepsize $\alpha_k>0$, one of three updates is applied:

$$z_k=P_X\bigl(x_k-\alpha_k\tilde\nabla f_{\omega_k}(z_k)\bigr),\qquad x_{k+1}=P_X\bigl(z_k-\alpha_k\tilde\nabla h_{\omega_k}(z_k)\bigr),\qquad(42)$$ $$z_k=x_k-\alpha_k\tilde\nabla f_{\omega_k}(z_k),\qquad x_{k+1}=P_X\bigl(z_k-\alpha_k\tilde\nabla h_{\omega_k}(z_k)\bigr),\qquad(43)$$ $$z_k=x_k-\alpha_k\tilde\nabla h_{\omega_k}(x_k),\qquad x_{k+1}=P_X\bigl(z_k-\alpha_k\tilde\nabla f_{\omega_k}(x_{k+1})\bigr).\qquad(44)$$

The implicit equations are proximal steps: in (42), $z_k$ minimizes $f_{\omega_k}(x)+\frac1{2\alpha_k}\|x-x_k\|^2$ over $X$. The randomized order means that $\omega_k$ is uniformly distributed over $\{1,\dots,m\}$ and independent of the past history $\mathcal F_k=\{x_k,z_{k-1},x_{k-1},\dots,z_0,x_0\}$ (Assumptions 3(a), 4(a)). The growth conditions (Assumptions 3(b), 4(b)) ask for a constant $c$ bounding, with probability 1 and for every component $i$, the norms of the subgradients used by the step that would be taken if $\omega_k$ were $i$, and the decrease of $f_i$, $h_i$ along that step by $c$ times its length.

Formalization targets

Goal: Proposition 9

If $\alpha_k\to0$ and $\sum_k\alpha_k=\infty$, then

$$\liminf_{k\to\infty}F(x_k)=F^*\quad\text{with probability 1},$$

and if in addition $X^*\neq\emptyset$ and $\sum_k\alpha_k^2<\infty$, then with probability 1 the iterates $x_k$ converge to some $x^*\in X^*$ (which may depend on the sample path).

Milestones

1. Eq. (58). For every $x^*\in X^*$ and every $k\ge0$,

$$E\{\|x_{k+1}-x^*\|^2\mid\mathcal F_k\}\le\|x_k-x^*\|^2-\frac{2\alpha_k}{m}\bigl(F(x_k)-F^*\bigr)+5\alpha_k^2c^2.$$

2. Proposition 2, the supermartingale convergence theorem: if $E\{Y_{k+1}\mid\mathcal F_k\}\le Y_k-Z_k+W_k$ for nonnegative adapted $Y_k,Z_k,W_k$ and $\sum_kW_k<\infty$ almost surely, then almost surely $\sum_kZ_k<\infty$ and $Y_k$ converges.
3. Eq. (59). If $\sum_k\alpha_k^2<\infty$, then for each $x^*\in X^*$, almost surely, $\sum_k\frac{2\alpha_k}{m}(F(x_k)-F^*)<\infty$ and $\|x_k-x^*\|$ converges.
4. Proposition 7 (constant stepsize $\alpha$): almost surely $\inf_{k\ge0}F(x_k)=F^*$ if $F^*=-\infty$, and $\inf_{k\ge0}F(x_k)\le F^*+\frac{5\alpha mc^2}{2}$ otherwise.
5. Proposition 8 (constant stepsize, $X^*\neq\emptyset$, $\epsilon>0$): the first index $N$ with $F(x_N)<F^*+\frac{5\alpha mc^2+\epsilon}{2}$ is almost surely finite and $E\{N\}\le m\,\mathrm{dist}(x_0;X^*)^2/(\alpha\epsilon)$.

Significance

Proposition 9 says that a randomized incremental method with a diminishing stepsize solves the problem exactly, almost surely, under conditions that do not require differentiability, bounded level sets, or strong convexity. Propositions 7 and 8 quantify the constant-stepsize regime: the error bound is $O(\alpha mc^2)$, smaller by a factor of $m$ than the worst case of the cyclic order (Proposition 4 of the paper). This is the paper's argument for randomization, and the same comparison recurs in the later literature on stochastic and incremental methods.

The results are proved in the paper. As far as known, none of them is machine-checked: Mathlib has conditional expectation, filtrations and Doob's martingale convergence theorem, but not the Robbins–Siegmund almost-supermartingale theorem in the form used here, and no incremental or stochastic proximal method has a formal convergence proof on the platform. The mission produces a formal model of a randomized algorithm with implicit (proximal) steps, a formal Robbins–Siegmund special case, and a complete a.s. convergence proof that other stochastic-approximation formalizations can reuse.

Difficulty

The deterministic estimate behind (58) is the one of the cyclic analysis with the sampled component in place of the cyclic one. The new difficulty is the conditioning step: $E\{F_{\omega_k}(z_k)\mid\mathcal F_k\}=\frac1m\sum_iF_i(z_k^i)$ needs the step that would be taken for each component $i$ to be a function of the past, and $\omega_k$ to be independent of it, and both must be stated so that the conditional expectation is that of an integrable function. The obvious route from (59) to part 2 of the goal fails: (59) gives, for each $x^*$, an event of probability 1, and $X^*$ is in general uncountable, so the events cannot be intersected directly. Part 1 must also handle $F^*=-\infty$, where no point of $X^*$ is available.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); components are indexed by Fin m ($0,\dots,m-1$), with $m\ge1$.
• $X$ is nonempty, closed and convex and $f_i,h_i$ are real-valued convex (the paper's standing assumptions of p. 4), stated as explicit hypotheses; stepsizes are positive.
• $P_X$ is a predicate (nearest point of $X$); subgradients are given by the subgradient inequality. The iterations (42)–(44) are their subgradient forms, with the subgradient of $f_i$ the one that makes the implicit equation hold, which is the paper's proximal step.
• $F^*$ is an infimum in EReal, so $F^*=-\infty$ is represented and the $\liminf$ and $\inf$ statements are in EReal.
• The run carries, for each $k$ and each component $i$, the would-be step from $x_k$; the realized step is the one for $i=\omega_k$. The bounds (45)–(48) are required for all $i$, as in the paper.
• "Independent of the past history" is formalized as independence of $\sigma(\omega_k)$ from $\mathcal F_k=\sigma(x_0,\dots,x_k,z_0,\dots,z_{k-1})$. Added hypotheses that make it meaningful: the iterates are measurable, the would-be step at $k$ is $\mathcal F_k$-measurable, and $x_0$ is a fixed vector.
• Proposition 2 adds integrability of $Y_k$ (Lean's conditional expectation of a non-integrable function is $0$).
• Proposition 8 uses the paper's own $N$ (the first entry time into the level set of its proof), not an arbitrary random variable, and adds the hypothesis $x_0\in X$, which its proof uses.

A formalization in which the would-be steps may depend on $\omega_k$, or in which $\omega_k$ is only assumed uniform, would let a step pick its component adversarially; the measurability and independence hypotheses rule this out, and none of the hypotheses is unsatisfiable (a sorry-free instance with $m=2$ is checked locally).

Needed infrastructure: the Robbins–Siegmund special case (Proposition 2), conditional expectation of a function of an independent uniform index and a past-measurable quantity, and existence of a countable dense subset of a closed set in $\mathbb R^n$. The supermartingale theorem and the conditioning lemma are reusable beyond this mission. Proofs of the milestones, of the goal, and of reusable lemmas about projections and proximal steps are welcome.

Selected references

• D. P. Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization, Report LIDS-P-2847, MIT, 2010 (revised March 2011); Mathematical Programming 129 (2011) 163–195. https://doi.org/10.1007/s10107-011-0472-0
• A. Nedić and D. P. Bertsekas, Incremental Subgradient Methods for Nondifferentiable Optimization, SIAM Journal on Optimization 12 (2001) 109–138. https://doi.org/10.1137/S1052623499362111
• H. Robbins and D. Siegmund, A Convergence Theorem for Non Negative Almost Supermartingales and Some Applications, in Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• J. Neveu, Discrete Parameter Martingales, North-Holland, 1975 (the paper's reference [43] for Proposition 2).
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996 (the paper's reference [7] for Proposition 2).

Motivation

Bounded-confidence opinion dynamics model a population in which each individual revises an opinion, represented by a real number, by looking only at opinions close to its own. The best-known example is the discrete-time model of Krause (1997), also called the Hegselmann–Krause model, in which every agent moves to the average of the opinions within distance 1 of its own. Such models are studied in the social sciences as models of consensus formation and polarization, and in control theory as prototypes of multiagent systems with state-dependent interaction topology: the communication graph is not given in advance but is determined by the state itself, which is what rendezvous algorithms for mobile robots and flocking models share (Lorenz 2007; Olfati-Saber, Fax, Murray 2007).

Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 48 (2010)) study the continuous-time, symmetric counterpart of Krause's model. Each opinion is continuously attracted by every other opinion differing from it by less than 1, with an intensity proportional to the difference. Simulations show convergence to clusters, groups of agents sharing a common value, with distinct clusters at distance at least 1 and typically close to 2. This mission formalizes the first of the paper's results: convergence to clusters at least 1 apart for finitely many agents.

Timeline.

• 1997: Krause introduces the discrete-time bounded-confidence model.
• 2003: Jadbabaie, Lin and Morse prove convergence results for nearest-neighbour coordination with switching topologies (IEEE TAC 48).
• 2009: Blondel, Hendrickx and Tsitsiklis analyse Krause's discrete-time model and the observed intercluster distance of about 2 (IEEE TAC 54).
• 2010: the present paper. For the continuous-time model with n agents it proves that every proper solution converges to an equilibrium with clusters at least 1 apart (Theorem 2). It also proves that almost every initial condition is proper (Theorem 1, proof sketched) and gives a continuum-agent analysis with a sharper intercluster bound.

Setting

There are $n$ agents, labelled $1,\dots,n$. Agent $i$ holds a real opinion $x_i(t)$ at each time $t\ge 0$, and $x_i$ is a continuous function of time. Agent $j$ is a neighbour of agent $i$ at time $t$ when $|x_i(t)-x_j(t)|<1$; the inequality is strict, and every agent is its own neighbour. The intended dynamics are

$$\dot x_i(t)=\sum_{j:\,|x_i(t)-x_j(t)|<1}\bigl(x_j(t)-x_i(t)\bigr).\tag{1.1}$$

The right-hand side jumps whenever a pair of opinions crosses distance 1, so (1.1) usually has no differentiable solution. The model is therefore the integral equation

$$x_i(t)=x_i(0)+\int_0^t\sum_{j:\,|x_i(\tau)-x_j(\tau)|<1}\bigl(x_j(\tau)-x_i(\tau)\bigr)\,d\tau\qquad(t\ge0,\ i=1,\dots,n).\tag{2.1}$$

Solutions of (2.1) need not be unique. The two-agent initial condition $(-\tfrac12,\tfrac12)$ is a fixed point, but the agents can also start attracting each other immediately. An initial condition $\tilde x\in\mathbb R^n$ is proper if (a) (2.1) has exactly one solution $x$ with $x(0)=\tilde x$; (b) the set of times at which $x$ is not differentiable is at most countable and has no accumulation point; and (c) agents that meet stay together: $x_i(t)=x_j(t)$ implies $x_i(t')=x_j(t')$ for all $t'\ge t$. That solution is then a proper solution.

The set of equilibria is

$$F=\bigl\{\tilde s\in\mathbb R^n:\ \text{for all } i,j,\ \tilde s_i=\tilde s_j\ \text{or}\ |\tilde s_i-\tilde s_j|\ge 1\bigr\}.$$

The average opinion is $\bar x(t)=\frac1n\sum_i x_i(t)$, and $V(x(t))=\sum_i\bigl(x_i(t)-\bar x(t)\bigr)^2$ is the sum of squared differences from it.

Formalization targets

Goal: Theorem 2

Every proper solution $x$ of (2.1) converges to a limit in $F$:

$$\exists\,x^*\in F:\qquad \lim_{t\to\infty}x(t)=x^*,$$

that is, all limits exist and two agents with different limits end at distance at least 1.

Milestones, in the order the argument uses them

1. Order preservation (§2.1, p. 5218): if $x_i(t)\ge x_j(t)$ for some $t$, then $x_i(t')\ge x_j(t')$ for every $t'\ge t$.
2. Proposition 1 (p. 5218): $\bar x$ is constant, $V(x(t))$ is nonincreasing, and outside a countable set of times $dV/dt$ is negative when $x(t)\notin F$ and zero when $x(t)\in F$.
3. Monotone partial sums (2.3) (p. 5219): for a sorted initial condition and every $k$, outside a countable set of times the derivative of $\sum_{i\le k}x_i(t)$ equals $\sum_{i\le k}\sum_{j>k:\,|x_i-x_j|<1}(x_j-x_i)\ge 0$, and $\sum_{i\le k}x_i(t)$ is nondecreasing in $t$.
4. Convergence of each opinion (p. 5219): every $x_i(t)$ has a limit as $t\to\infty$.

Significance

The result. Theorem 2 establishes the clustering behaviour seen in simulations for every proper solution. The paper's Theorem 1 states that almost every initial condition is proper, so the conclusion covers almost every initial condition. The lower bound 1 on the distance between clusters is the baseline that the paper's continuum analysis improves to $1+\min\{W_A,W_B\}/\max\{W_A,W_B\}$. Average preservation and the decrease of $V$ (Proposition 1) are the structural facts that the continuum model also has.

Formalization. Theorem 2 is proved in the paper; no machine-checked version exists on Prove2Me or, as far as is known, elsewhere. The mission produces a Lean definition of solutions of a discontinuous integral equation with a state-dependent neighbour graph, and a convergence proof for it. The remaining work is to formalize the known argument, from the integral equation to the existence and location of the limit.

Difficulty

The obvious approach treats (1.1) as an ODE and differentiates along trajectories. That fails because the right-hand side is discontinuous in the state. A solution is only an integral solution, it may fail to be differentiable, and derivative identities such as (2.3) hold only outside an exceptional set of times. Every step from a derivative sign to a monotonicity or limit statement therefore has to go through the integral equation, not the differential one. A second obstacle is that pairs of agents at distance exactly 1 sit on the discontinuity of the interaction rule. This is where uniqueness fails (footnote 3 of the paper) and why conditions (a)–(c) are hypotheses. A decreasing Lyapunov function $V$ alone does not give convergence of the trajectory to a single point, so Proposition 1 does not by itself settle Theorem 2.

Formalization scope

Agents are Fin n. Time is ℝ, and only values at $t\ge 0$ enter. A trajectory is x : ℝ → Fin n → ℝ. A solution of (2.1) is continuous on $[0,\infty)$ and satisfies (2.1) for every $t\ge 0$ and every $i$, with the neighbour set Finset.univ.filter (fun j => |x τ i - x τ j| < 1). The integrand is also required to be interval-integrable on $[0,t]$; for a continuous trajectory this always holds. Explicit readings of the paper's phrases:

• "unique solution" in (a) is uniqueness among all solutions of (2.1), with no sortedness or differentiability assumed;
• condition (b) is "for every $T$, the non-differentiability times in $[0,T]$ form a finite set", which is equivalent for subsets of $[0,\infty)$;
• "converges to a limit" is Tendsto x atTop (𝓝 xstar) in Fin n → ℝ, with real time;
• "with the exception of a countable set of times" is the existence of a countable set $S$ outside which the derivative of $V(x(t))$ exists and has the stated sign;
• "constant" and "nonincreasing" are on $[0,\infty)$;
• Proposition 1 assumes $n\ge1$ so that $\bar x$ is meaningful.

The paper's sortedness convention ("we assume … that the components of proper initial conditions are sorted") is a hypothesis only of the partial-sum milestone. Theorem 2 is stated for every proper solution. A formalization that dropped condition (a), restricted solutions to sorted, differentiable or eventually constant trajectories, or replaced (2.1) by the differential equation would prove a different, and in parts trivial, statement. These are excluded.

The work needs interval integrals and the fundamental theorem of calculus for integrands with jumps, monotonicity from almost-everywhere derivative signs, and bounded monotone convergence. The definition of solutions of (2.1) and the equilibrium set is reusable for the stability results of the same paper (Theorem 3), which are not part of this mission. Contributions are welcome at every milestone, as are alternative convergence proofs, such as the paper's reference [9], that avoid symmetry.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188
• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, On Krause's multi-agent consensus model with state-dependent connectivity, IEEE Trans. Automat. Control 54(11), 2009, 2586–2597. https://doi.org/10.1109/TAC.2009.2031211
• A. Jadbabaie, J. Lin, A. S. Morse, Coordination of groups of mobile autonomous agents using nearest neighbor rules, IEEE Trans. Automat. Control 48(6), 2003, 988–1001. https://doi.org/10.1109/TAC.2003.812781
• J. Lorenz, Continuous opinion dynamics under bounded confidence: a survey, Internat. J. Modern Phys. C 18(12), 2007, 1819–1838. https://doi.org/10.1142/S0129183107011789
• R. Olfati-Saber, J. A. Fax, R. M. Murray, Consensus and cooperation in networked multi-agent systems, Proc. IEEE 95(1), 2007, 215–233. https://doi.org/10.1109/JPROC.2006.887293
• U. Krause, Soziale Dynamiken mit vielen Interakteuren. Eine Problemskizze, in Modellierung und Simulation von Dynamiken mit vielen interagierenden Akteuren, Universität Bremen, 1997, 37–51.

Motivation

Online covering models decisions that must be made as requirements arrive. A planner knows the cost of each available resource, but learns the requirements one at a time and cannot undo an allocation already made. This occurs, for example, when requests for network service or elements needing coverage appear over time. The central question is how much more an online fractional allocation can cost than a best allocation chosen after all requirements are known. Buchbinder and Naor study this question through a paired covering and packing linear program and give an online scheme for arbitrary nonnegative constraint coefficients, not only incidence coefficients in $\{0,1\}$ (Buchbinder and Naor, 2009, §§2–4).

The result targeted here is Theorem 4.1 of that paper. It concerns the fractional covering scheme of §4, before the separate extension to box constraints in §4.1. The theorem is a statement about the particular phased scheme, so the scheme's state and update rule form part of the mathematical setting. The online requirement also matters: after each new constraint, earlier allocations remain in force (Buchbinder and Naor, 2009, pp. 4, 8).

Setting

Let $I$ be a finite nonempty set of $n$ primal variables and let $k=0,\ldots,m-1$ index constraints in arrival order. The known cost of variable $i$ is $c_i>0$. Constraint $k$ has coefficient $a_{ik}\ge0$ for variable $i$; when it arrives, the online algorithm learns its coefficients. The normalized offline covering problem minimizes $\sum_i c_i z_i$ over $z_i\ge0$ subject to $\sum_i a_{ik}z_i\ge1$ for every constraint considered. Its packing dual maximizes $\sum_k y_k$ over $y_k\ge0$ subject to $\sum_k a_{ik}y_k\le c_i$ for each $i$. The finite data and sign conventions are those of Figure 1 (Buchbinder and Naor, 2009, pp. 3–4).

The scheme accepts a parameter $B>0$ and asks for coverage only to $1/B$. It maintains a sequence of phases. The first phase bound $\alpha_1$ is $B^{-1}$ times the least ratio $c_i/a_{i0}$ among the positive coefficients of the first constraint. The bound doubles at a restart. Within a phase, the vector $y$ begins at zero, the initial primal allocation is $x_i=\alpha/(2nc_i)$, and the allocation subsequently follows the exponential expression on page 8. The current phase may need to process constraints already seen in earlier phases. Old phase vectors are retained: the actual online allocation is the coordinatewise maximum of the current and all finished phase vectors. Thus resetting a phase does not retract an earlier allocation (Buchbinder and Naor, 2009, p. 8).

Formalization targets

Theorem 4.1: coverage and competitive cost

For every nonempty arrival prefix of length $J$, a run of the phased scheme exists. Every completed run has output $x$ satisfying

$$\sum_i a_{ik}x_i\ge\frac1B\qquad(k<J),$$

and, for every nonnegative offline comparison vector $z$ satisfying $\sum_i a_{ik}z_i\ge1$ for each $k<J$,

$$\sum_i c_i x_i\le\frac{8\log(2n)}{B}\sum_i c_i z_i.$$

The paper states the ratio as $O(\log n/B)$. Its closing display on page 9 yields the explicit factor $8\log(2n)/B$ used here. The benchmark uses the unscaled covering constraints of Figure 1; replacing them with constraints at $1/B$ would change the guarantee (Buchbinder and Naor, 2009, Theorem 4.1 and proof, pp. 8–9).

The four claims within its proof

The milestone list follows the four claims printed under Theorem 4.1. A finished phase has dual objective at least $B\alpha_r/(2\log(2n))$; every phase dual vector satisfies the packing constraints; the sum of phase primal costs through the current phase is less than $2\alpha_r$; and the actual allocation covers every arrived constraint to $1/B$. These are statements about the phase records of the scheme, including a partly processed round that ends in a restart (Buchbinder and Naor, 2009, pp. 8–9).

Significance

The theorem gives a cost guarantee for a general online covering problem while allowing arbitrary nonnegative coefficients. It separates the cost paid by an allocation from the level of coverage requested through $B$. Its four claims identify the quantities that make the guarantee meaningful: the dual vector certifies a lower bound for an offline comparison, the phase costs control the online expenditure, and the output remains feasible as constraints arrive. The same primal–dual setting is used elsewhere in the paper for online packing and for applications of covering and packing methods (Buchbinder and Naor, 2009, §§3–5).

The paper proves Theorem 4.1. This mission asks for a machine-checked account of the known result and of the scheme to which it applies. A published formal restatement, OnlinePrimalDual.GeneralPacking.theorem14_3, already gives a ratio conclusion under an assumed ratio bound and an assumed weak-duality inequality; those hypotheses contain the main work needed here. The present goal instead quantifies over runs generated by the update rule and asks both that a run exists and that all such runs satisfy the guarantees. The published general instance definition is reused, so the finite covering and packing data have a shared interface.

Difficulty

An online allocation cannot be evaluated solely from its final vector. A phase restart resets the working dual vector and restarts the constraint scan, while allocations from completed phases still affect the actual output. A statement about arbitrary vectors with a presumed cost bound would leave out this behavior. The continuous update also requires a precise stopping event when coverage or the phase cost reaches its threshold. The cost guarantee is sensitive to which condition wins if both occur together, and to whether a phase can restart indefinitely. Those details must be represented before any claim about completed phases has the paper's meaning (Buchbinder and Naor, 2009, pp. 8–9).

Formalization scope

Lean uses OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) for the coefficient matrix and costs. A nonempty finite type $I$ represents the $n$ primal variables; Fin m supplies the ordered constraints. The theorem assumes $m\ge1$, $B>0$, and a positive coefficient in every constraint. The last condition makes each arriving constraint coverable and makes the first ratio minimum nonempty; zero coefficients are omitted from that minimum. The paper treats infeasible all-zero rows implicitly. The minimum is over a finite nonempty set, so the real infimum in the Lean definition equals the ordinary minimum. All sums are finite and all logarithms are natural.

The run is an event relation with three events: arrival of one new constraint after all known constraints have been processed, completion of a covered round at its first stopping time, and restart at the cost cap while coverage remains deficient. A restart doubles $\alpha$, records the old phase, resets the dual variables, and resumes at the first known constraint. The state records the current phase and all finished phases; the output takes their coordinatewise maximum. A simultaneous coverage and cost event counts as covered. Reaching the cost cap models the continuous stopping time behind the paper's wording that the cost “exceeds” the bound. The theorem asserts run existence, so a ratio claim cannot hold merely because the run relation has no witness.

The explicit $O(\cdot)$ instantiation in this mission is $8\log(2n)/B$, from the page 9 closing display. The first-phase case is bounded there by $1/B$ times the optimum and is included in the same stated coefficient. The comparison vector must satisfy the original level-one constraints. Theorem 4.2, which adds upper bounds on variables and appears in §4.1, is outside this mission. The run definition, phase-cost and coverage functions, and the four claims are reusable infrastructure for later work on continuous online primal–dual schemes.

Selected references

• Niv Buchbinder and Joseph Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research, 2009. DOI: 10.1287/moor.1080.0363.

Motivation

Many optimization problems in machine learning, signal processing and distributed computation have an objective that is a sum of a large number $m$ of component functions: one per data point, per sensor, or per processor. Evaluating the whole sum, or a subgradient of it, at every iteration is expensive when $m$ is large. Incremental methods process one component at a time, cycling through the components or sampling them, and update the iterate after each one. Incremental gradient and subgradient methods go back to the training of neural networks and to least squares; incremental proximal methods replace the subgradient step of a component by a proximal step, which is more stable and handles nonsmooth terms exactly.

Bertsekas (LIDS-P-2847, 2010, rev. 2011; Math. Program. 129 (2011)) proposed a unified family that mixes the two: each component is split as $F_i=f_i+h_i$, a proximal step is taken on $f_i$ and a subgradient step on $h_i$, followed by a projection onto the constraint set. This mission formalizes the convergence analysis of that family under the cyclic order of component selection.

Timeline. Incremental subgradient methods were analysed by Nedić and Bertsekas (SIAM J. Optim. 12 (2001)) for cyclic and randomized orders. Incremental proximal methods were studied by Bertsekas (Optimization for Machine Learning, 2011, ch. 4). The 2011 paper combines the two analyses; its cyclic-order results are Propositions 3–6.

Setting

Let $\mathbb R^n$ carry the Euclidean norm $\|\cdot\|$ and inner product $x'y$. The data are a nonempty closed convex set $X\subseteq\mathbb R^n$ and real-valued convex functions $f_i,h_i:\mathbb R^n\to\mathbb R$, $i=1,\dots,m$. The problem is

$$\text{minimize } F(x)=\sum_{i=1}^m F_i(x),\qquad F_i=f_i+h_i,\qquad\text{subject to } x\in X,$$

with optimal value $F^*=\inf_{x\in X}F(x)$, possibly $-\infty$, and optimal set $X^*=\{x^*\in X:F(x^*)=F^*\}$, possibly empty.

A subgradient $\tilde\nabla f(x)$ of a convex $f$ at $x$ is a vector $g$ with $f(y)\ge f(x)+g'(y-x)$ for all $y$; $P_X(u)$ is the point of $X$ nearest to $u$. At iteration $k$ one component $i_k$ is processed with stepsize $\alpha_k>0$. The three iterations are

$$\begin{aligned} &(19)\quad z_k=P_X\big(x_k-\alpha_k\tilde\nabla f_{i_k}(z_k)\big),&& x_{k+1}=P_X\big(z_k-\alpha_k\tilde\nabla h_{i_k}(z_k)\big),\\ &(20)\quad z_k=x_k-\alpha_k\tilde\nabla f_{i_k}(z_k),&& x_{k+1}=P_X\big(z_k-\alpha_k\tilde\nabla h_{i_k}(z_k)\big),\\ &(21)\quad z_k=x_k-\alpha_k\tilde\nabla h_{i_k}(x_k),&& x_{k+1}=P_X\big(z_k-\alpha_k\tilde\nabla f_{i_k}(x_{k+1})\big). \end{aligned}$$

The $f$-subgradient is taken at the new point, which makes the $f$-part a proximal step (Proposition 1). In the cyclic order $i_k=(k\bmod m)+1$; a block of $m$ consecutive iterations is a cycle, and $\alpha_k$ is constant within a cycle.

The analysis assumes that the subgradients the iteration uses are bounded by a constant $c$ and that, at each cycle start $k>0$, the function values at the intermediate points of the cycle differ from those at $x_k$ by at most $c$ times the distance (Assumption 1 for (19), (20); Assumption 2 for (21)). Both hold, for example, when all $f_i$, $h_i$ are polyhedral or Lipschitz.

Formalization targets

Goal: Proposition 6

If $\alpha_k\to0$ and $\sum_k\alpha_k=\infty$, then

$$\liminf_{k\to\infty}F(x_k)=F^*,$$

and if moreover $X^*\neq\emptyset$ and $\sum_k\alpha_k^2<\infty$, then $x_k\to x^*$ for some $x^*\in X^*$. Both parts are one item, as in the paper.

Milestones

1. Proposition 1: the proximal iteration over $X$ equals $P_X(x_k-\alpha_k\tilde\nabla f(x_{k+1}))$, and $\|x_{k+1}-y\|^2\le\|x_k-y\|^2-2\alpha_k(f(x_{k+1})-f(y))-\|x_k-x_{k+1}\|^2$ for $y\in X$.
2. Eq. (30) and Eq. (37): one-iteration estimates for (19)/(20) and for (21).
3. Proposition 3: over one cycle, $\|x_{k+m}-y\|^2\le\|x_k-y\|^2-2\alpha_k(F(x_k)-F(y))+\alpha_k^2\beta m^2c^2$, with $\beta=\frac1m+4$ for (19), (20) and $\beta=\frac5m+4$ for (21).
4. Footnote 5: nonnegative sequences with $Y_{k+1}\le Y_k-Z_k+W_k$ and $\sum W_k<\infty$ have $Y_k$ convergent.
5. Proof of Proposition 6: $\|x_{k+1}-x_k\|\le2\alpha_kc$.
6. Proposition 4 (constant stepsize $\alpha$): $\liminf F(x_k)=F^*$ if $F^*=-\infty$, and $\liminf F(x_k)\le F^*+\alpha\beta m^2c^2/2$ otherwise.

Significance

Proposition 6 is the exact-convergence guarantee for the cyclic incremental subgradient-proximal methods: with a diminishing, non-summable stepsize they reach the optimal value whatever the starting point, and with square-summable stepsizes the iterates converge to a single optimal solution. It covers the pure incremental subgradient method ($f_i=0$) and the pure incremental proximal method ($h_i=0$) as special cases, and it is the template for the randomized-order analysis of the companion mission. Proposition 4 quantifies what a constant stepsize achieves.

These results are proved in the paper. None of them, nor the underlying estimates, is formalized on the platform or, to our knowledge, in Mathlib. The mission produces machine-checked versions of the proximal-step lemma for extended-real-valued functions on a constrained set, of the cycle estimate (27) with its explicit constants, and of the deterministic supermartingale convergence lemma, all reusable for other incremental and proximal methods.

Difficulty

The obvious argument treats one cycle as one step of a subgradient method on $F$. It fails because within a cycle the subgradients are taken at the intermediate points $z_{k+j-1}$ or $x_{k+j-1}$, not at $x_k$, and the proximal steps use subgradients at the points they produce. The error between $F_j(x_k)$ and $F_j$ at those points must be controlled through the drift of the iterates during the cycle, and the bookkeeping differs between (19)/(20) and (21), which is why $\beta$ differs. For the second part of Proposition 6, convergence of the values in the $\liminf$ sense does not by itself give convergence of the iterates, and $X^*$ may contain more than one point.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Components are Fin m (0-based), so $i_k$ is k % m, and the paper's $j=1,\dots,m$ with $z_{k+j-1}$ becomes $j=0,\dots,m-1$ with z (k + j). $m\ge1$ is assumed (NeZero m).
• $P_X$ is a predicate (IsProj: a nearest point of $X$), not a choice function.
• Each iteration is a relation Step between $x_k$, $z_k$, $x_{k+1}$ and the two subgradients it uses, with the $f$-subgradient at the point the paper names. A run records these subgradients, so Assumptions 1–2 bound exactly them. The assumptions are not replaced by Lipschitz continuity, which is only a sufficient condition (p. 9).
• $F^*$ and $\liminf F(x_k)$ are taken in EReal; $F^*=-\infty$ is allowed and no boundedness is assumed.
• The standing assumptions of p. 4 (X nonempty closed convex, $f_i,h_i$ convex), positive stepsizes, constancy within a cycle and Assumptions 1–2 (stated "throughout this section", p. 8) are explicit hypotheses of every statement, including the goal, whose sentence does not repeat them.
• The starting point $x_0$ is arbitrary, as in the paper. Assumptions 1–2 make the cycle-start conditions only for $k>0$, and the bound $\|x_{k+1}-x_k\|\le2\alpha_kc$ needs $x_k\in X$, which holds from $k=1$ on. Proposition 3 and the step bound are therefore stated for $k>0$ and $k\ge1$; this does not affect Propositions 4 and 6.
• Proposition 1 is stated for extended-real-valued closed proper convex $f$, as in the paper, using the published class $\Gamma_0$ (MoreauProx.Characterization.GammaZero) and its subgradients, with relative interiors as Mathlib's intrinsicInterior.

The goal cannot be satisfied vacuously: a sorry-free check confirms that the hypotheses hold together (for $n=1$, $m=2$, $X=\mathbb R$, $\alpha_k=1/(\lfloor k/2\rfloor+1)$, $X^*\neq\emptyset$). Restricting to Lipschitz components, to bounded-below $F$, or to $x_0\in X$ would state a weaker theorem and is ruled out.

Proofs of any item are welcome, as are general lemmas (the projection theorem as a variational inequality, the subdifferential sum rule under the relative-interior condition) that the proofs need.

Selected references

• D. P. Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization, Report LIDS-P-2847, MIT, 2010 (rev. March 2011); Math. Program. 129(2) (2011) 163–195. https://doi.org/10.1007/s10107-011-0472-0
• A. Nedić, D. P. Bertsekas, Incremental Subgradient Methods for Nondifferentiable Optimization, SIAM J. Optim. 12(1) (2001) 109–138. https://doi.org/10.1137/S1052623499362111
• D. P. Bertsekas, Incremental Gradient, Subgradient, and Proximal Methods for Convex Optimization: A Survey, in Optimization for Machine Learning, MIT Press, 2011. https://arxiv.org/abs/1507.01030
• D. P. Bertsekas, A. Nedić, A. E. Ozdaglar, Convex Analysis and Optimization, Athena Scientific, 2003.