Operations Research

Motivation

Quasi-Newton methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.

The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most $n$ steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.

Timeline.

• 1952: Hestenes and Stiefel's conjugate gradient method minimizes a strictly convex quadratic in at most $n$ steps (J. Res. NBS 49); Davidon cites it as [2].
• 1959: Davidon's ANL-5990, including the Appendix method treated here.
• 1963: Fletcher and Powell simplify the body's method into the DFP update and prove its quadratic termination with exact line searches (Comput. J. 6).
• 1967: Broyden's survey of quasi-Newton methods discusses the symmetric rank-one update (Math. Comp. 21); textbooks later analyse it under the name SR1.
• 1980: Nocedal's limited-storage BFGS, whose termination on quadratics with exact line searches is a separate Prove2Me mission (Math. Comp. 35).

Setting

Vectors are elements of $\mathbb R^n$ and matrices are real $n\times n$. Fix a symmetric positive definite matrix $G$ and a point $\xi$, and let

$$f(x)=\tfrac12\,(x-\xi)^{\mathsf T}G\,(x-\xi)+c ,$$

a quadratic with constant Hessian $G$ and minimum point $\xi$. Its gradient is $\nabla(x)=G(x-\xi)$, display (6) of the Appendix.

The method keeps a point $x_k$ and a symmetric trial matrix $H_k$, which plays the role of $G^{-1}$. Write $\nabla_k=\nabla(x_k)$. One iteration is

$$x_{k+1}=x_k-H_k\nabla_k \quad\text{(2)},\qquad H_{k+1}=H_k+a_k\,(H_k\nabla_{k+1})(H_k\nabla_{k+1})^{\mathsf T}\quad\text{(3)},$$

a full step with no line search followed by a symmetric rank-one update. With the two scalars

$$N_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_{k+1},\qquad M_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_k ,$$

footnote 2 of the Appendix fixes the coefficient on a quadratic to $a_k=(M_k-N_k)^{-1}$, which makes the paper's quality measure $\Delta$ of (4) vanish. Write $S_k=x_{k+1}-x_k$ for the step and $D_k=\nabla_{k+1}-\nabla_k$ for the change of gradient. The paper writes $x$, $H$, $\nabla$ for the current quantities and $x^{+}$, $H^{+}$, $\nabla^{+}$ for the updated ones, and uses the letter $N$ both for the number of variables and for the scalar $N_k$; here the number of variables is $n$.

Formalization targets

Goal: termination in $n$ steps

If $H_0$ is symmetric and $M_k\ne N_k$ for every $k<n$, then

$$H_n=G^{-1}\qquad\text{and}\qquad x_{n+1}=\xi .$$

This is the sentence after (8) on p. 17: "After no more than $N$ steps (for which $\Delta=0$), $H$ will equal $G^{-1}$ and the following step will be to the exact minimum."

Milestones

1. Display (6): the gradient of $f$ is $G(x-\xi)$.
2. Display (8): with $a=(M-N)^{-1}$ and $M\ne N$, $H^{+}GS=H^{+}D=S$.
3. Display (7): if $HGu=u$ then $H^{+}Gu=u$, for any coefficient $a$.
4. The sentence "so that $S$ becomes another such eigenvector", read along the run: if $M_i\ne N_i$ for $i<k$, then $H_kGS_j=S_j$ for every $j<k$.

Further statements of the Appendix

• Condition 1 (p. 16): if $H$ is positive definite and $R^{-1}\le\det H^{+}/\det H\le R$ with $R>1$, then $H^{+}$ is positive definite.
• The constraint remark (p. 17): for any function and any coefficients, if $H_0$ is symmetric and $H_0b=0$, then every step is perpendicular to $b$ and $b\cdot x_k$ is conserved.
• Table (5) (p. 16): for general (non-quadratic) $f$, the coefficient $a$ that minimizes $\Delta$ subject to condition 1, and the minimum value, on each of five ranges of $M$.

Significance

The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from $n$ gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric $H_k$ converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.

The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first $n$ coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.

Difficulty

Each update changes $H$ by a rank-one term, and nothing in a single step forces $H_n$ to be $G^{-1}$: the coefficient $a_k$ depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — $n$ steps, $n$ conditions — does not by itself give $n$ independent conditions on $H_n$; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators $M_k-N_k$ are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of $H_0$, or a line search.

Formalization scope

Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; $u^{\mathsf T}Hv$ is u ⬝ᵥ (H *ᵥ v) and $(Hg)(Hg)^{\mathsf T}$ is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with $a_k=(M_k-N_k)^{-1}$; DavidonVM.Termination.Delta provides the update and the quantity $\Delta$ of (4).

Committed conventions, each a reading of something the paper leaves implicit:

• The function is an explicit quadratic with constant symmetric positive definite $G$ ("in the neighborhood of a minimum"); the run's gradient field is $G(x-\xi)$, and milestone 1 ties it to the quadratic. The goal uses positive definiteness; milestones use only symmetry where that suffices; the secant milestone needs nothing on $G$.
• Only $H_0$ is assumed symmetric (the paper, p. 4: "It is to be symmetric"); positive definiteness of $H_0$ is not assumed.
• "Steps for which $\Delta=0$" is read through footnote 2 as $M_k\ne N_k$. Lean's real inverse gives $0^{-1}=0$, so without this hypothesis the update would silently leave $H$ unchanged.
• The stopping rule "provided that $N$ is greater than some preassigned $\varepsilon$" is not modelled; the run continues for every $k$, and the goal looks at steps $0,\dots,n$ only.
• $G^{-1}$ is Mathlib's matrix inverse, the true inverse since $G$ is positive definite.

A statement of the goal with the extra hypothesis "$S_0,\dots,S_{n-1}$ are linearly independent", or with $H_k G S_j=S_j$ assumed, would be a weaker theorem than the paper's and is ruled out. The case $n=0$ is trivial; the hypotheses are jointly satisfiable for $n=1$ (checked locally).

Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.

Selected references

• W. C. Davidon, Variable Metric Method for Minimization, SIAM J. Optim. 1(1) (1991) 1–17 (Argonne report ANL-5990, 1959). https://doi.org/10.1137/0801001
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• R. Fletcher and M. J. D. Powell, A rapidly convergent descent method for minimization, Comput. J. 6 (1963) 163–168. https://doi.org/10.1093/comjnl/6.2.163
• C. G. Broyden, Quasi-Newton methods and their application to function minimisation, Math. Comp. 21 (1967) 368–381. https://doi.org/10.1090/S0025-5718-1967-0224273-2
• J. Nocedal, Updating quasi-Newton matrices with limited storage, Math. Comp. 35 (1980) 773–782. https://doi.org/10.1090/S0025-5718-1980-0572855-7

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.