All missions

Motivation

Many problems in machine learning and signal processing minimize a smooth loss plus a simple non-smooth regularizer: $\ell_1$-regularized least squares, group-sparse regression, and constrained problems written with an indicator function. The standard algorithm for this composite form is the proximal-gradient method, a gradient step on the smooth part followed by a proximal step on the regularizer. Its classical linear convergence guarantee needs the smooth part to be strongly convex, a hypothesis that fails for $\ell_1$-regularized least squares with fewer observations than variables and for most problems of interest without explicit $\ell_2$ regularization.

For smooth problems the Polyak–Łojasiewicz (PL) inequality $\tfrac12\|\nabla f(x)\|^2 \ge \mu(f(x) - f^*)$ gives a linear rate for gradient descent without convexity (Polyak 1963). Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) propose a generalization to the composite setting, the proximal-PL inequality, under which the proximal-gradient method converges linearly with a one-paragraph proof. They show that it contains the PL case, the strongly convex case, and convex objectives with quadratic growth, and that it is equivalent to the Kurdyka–Łojasiewicz inequality (Bolte, Nguyen, Peypouquet, Suter 2017) and to the proximal error bound used earlier by Luo, Tseng and Drusvyatskiy–Lewis.

Timeline:

• 1963: Polyak proves linear convergence of gradient descent under the PL inequality.
• 1993: Luo and Tseng prove linear convergence of feasible descent methods under an error bound.
• 2015–2016: Bolte et al. and Li–Pong obtain linear rates of proximal gradient under the KL inequality; Drusvyatskiy and Lewis relate error bounds and quadratic growth (arXiv:1602.06661).
• 2016: Karimi, Nutini and Schmidt introduce the proximal-PL inequality and Theorem 5.

Setting

Let $f, g : \mathbb R^d \to \mathbb R$ and consider problem (11),

$$\min_{x \in \mathbb R^d} F(x) = f(x) + g(x).$$

The function $f$ is differentiable with an $L$-Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L\|x - y\|$ with $L > 0$. The function $g$ is convex. $F$ has a minimizer $x^*$, and $F^* = F(x^*)$.

For a base point $x$ and a parameter $\alpha > 0$, the proximal model is

$$m_{x,\alpha}(y) = \langle \nabla f(x), y - x\rangle + \frac{\alpha}{2}\|y - x\|^2 + g(y) - g(x),$$

and the paper's measure of non-stationarity is

$$\mathcal D_g(x, \alpha) = -2\alpha \min_{y} m_{x,\alpha}(y). \tag{13}$$

$F$ satisfies the proximal-PL inequality with modulus $\mu > 0$ if

$$\tfrac12\,\mathcal D_g(x, L) \ge \mu\bigl(F(x) - F^*\bigr) \quad \text{for all } x. \tag{12}$$

When $g$ is constant, $\mathcal D_g(x, \alpha) = \|\nabla f(x)\|^2$ and (12) is the PL inequality.

The proximal-gradient method with step size $1/L$ starts at an arbitrary $x_0$ and sets

$$x_{k+1} \in \operatorname*{argmin}_y m_{x_k, L}(y). \tag{14}$$

The proximal residual function of Appendix E is $\mathcal R_g(\lambda, x, a) = \min_y [\|\lambda(y - x) + a\|^2 + 2\lambda(g(y) - g(x))]$.

Formalization targets

Goal: Theorem 5 (p. 8)

Under the hypotheses above,

$$F(x_k) - F^* \le \Bigl(1 - \frac{\mu}{L}\Bigr)^k \bigl[F(x_0) - F^*\bigr] \qquad \text{for every } k \ge 0.$$

Milestones (proof of Theorem 5)

1. The quadratic upper bound (2), p. 2: an $L$-Lipschitz gradient gives $f(y) \le f(x) + \langle\nabla f(x), y - x\rangle + \frac L2\|y - x\|^2$.
2. Descent by $\mathcal D_g$, p. 9: if $x^+$ minimizes $m_{x,L}$, then $F(x^+) \le F(x) - \frac{1}{2L}\mathcal D_g(x, L)$.
3. The one-step contraction (15), p. 9: $F(x^+) - F^* \le (1 - \mu/L)[F(x) - F^*]$.

Companion results

• Lemma 2 (p. 17): for convex $g$, $\mathcal R_g(\cdot, x, a)$ is non-increasing on $(0, \infty)$.
• Lemma 1 = Corollary 1 (p. 17): $\mathcal D_g(x, \mu_2) \ge \mathcal D_g(x, \mu_1)$ for $\mu_2 \ge \mu_1 > 0$.
• Appendix F, item 1 (p. 18): for constant $g$, $\mathcal D_g(x, \alpha) = \|\nabla f(x)\|^2$, and proximal-PL is PL.
• Appendix F, item 2 (p. 18): for $\mu$-strongly convex $f$, $F^* \ge F(x) - \frac{1}{2\mu}\mathcal D_g(x, \mu)$.
• Appendix F, item 4 (p. 19): for convex $f$ and $F$ with quadratic growth of modulus $\mu$, $\mathcal D_g(x, \mu/2) \ge \frac{\mu}{2}(F(x) - F^*)$.
• Two well-definedness statements: for convex $g$ and a positive parameter, the minima in (13) and (27) are attained.

Significance

Theorem 5 gives a global linear rate for the proximal-gradient method under a hypothesis that does not require strong convexity, or convexity of $f$. Through the classes of Section 4.1 it covers $\ell_1$-regularized least squares, the composite strongly convex case, and convex composite problems with quadratic growth. The quantity $\mathcal D_g$ also drives the analysis of proximal coordinate descent (Theorem 6, mission VI of this series), and Lemma 1 is what lets the sufficient conditions of Appendix F, which hold with $\mathcal D_g(x, \lambda)$ for $\lambda \le L$, be used in (12).

The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The work here is to formalize the known proofs, including the properties of $\mathcal D_g$ and $\mathcal R_g$ that the paper uses without stating: the minimum in (13) exists, and the value is finite.

Difficulty

The proof of Theorem 5 is short; the difficulty sits in the objects. $\mathcal D_g$ is defined through a minimum over $\mathbb R^d$ of a function involving a non-smooth convex $g$, so every step that replaces the minimum by its value at a particular point needs the minimum to be finite and attained. The paper never states these facts, and they fail for an arbitrary $g$: for $g(y) = -\|y\|^2$ and $\alpha < 2$ the model is unbounded below and the minimum in (13) does not exist. The monotonicity of $\mathcal D_g$ in its second argument (Lemma 1) rests on the convexity inequality of $g$, and Appendix F item 4 relies on the projection onto the solution set, whose existence depends on that set being closed, convex and non-empty.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), $\nabla f$ is Mathlib's gradient f, and the Lipschitz hypothesis is written literally, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖, with 0 < L.
• The non-empty solution set is a point xstar with F xstar ≤ F y for all y; $F^*$ is f xstar + g xstar, never a free real.
• $g$ is real-valued and convex (ConvexOn ℝ Set.univ g). Indicator functions of convex sets, which the paper lists among its examples, take the value $+\infty$ and are outside this formalization; the formulas (13)–(15) subtract values of $g$, which is undefined at $+\infty$.
• The minimum in (13) and (27) is a real infimum. A real infimum of a set that is unbounded below has the junk value $0$ in Lean, so $\mathcal D_g(x, \alpha)$ is used only with $\alpha > 0$ and convex $g$, where the infimum is a minimum; this rules out the trivializing reading in which $\mathcal D_g$ vanishes and (12) becomes $F \le F^*$.
• A proximal-gradient run is any sequence whose every step is a minimizer of the model; the minimizer is unique for convex $g$, but uniqueness is not assumed.
• No relation between $\mu$ and $L$ is assumed, as in the paper.
• The PL predicate in Appendix F item 1 is the published ShiOptRates.PolyakLojasiewicz (the paper's (3) multiplied by 2), and (2) is the published ShiOptRates.QuadUpper.

Quadratic growth is stated with the distance to the solution set, $\operatorname{dist}(x, \mathcal X^*)$, which equals $\|x - x_p\|$ for the projection $x_p$ the paper uses. Appendix F item 3 (Hoffman's bound with an unspecified constant $\theta(A, B)$) and the equivalences of Appendix G are not included.

Contributions of every kind are welcome: proofs of the milestones, of the companion lemmas, and reusable facts about $\mathcal D_g$ (finiteness, attainment, continuity in $x$) that other proximal-method missions can import.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46, 1993. https://doi.org/10.1007/BF02096261
• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Mathematical Programming 165, 2017. https://doi.org/10.1007/s10107-016-1091-6
• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Mathematics of Operations Research 43(3), 2018. https://arxiv.org/abs/1602.06661
• G. Li, T. K. Pong, Calculus of the exponent of Kurdyka–Łojasiewicz inequality and its applications to linear convergence of first-order methods, Foundations of Computational Mathematics 18, 2018. https://arxiv.org/abs/1602.02915

Motivation

Accelerated gradient (AG) methods go back to Nesterov (1983), who showed that a first-order method with a momentum-like extrapolation reaches an $\epsilon$-optimal value of a smooth convex function in $O(1/\sqrt\epsilon)$ iterations, against $O(1/\epsilon)$ for gradient descent, and that this rate is optimal among first-order methods. Many objectives met in practice (training losses, nonconvex penalties, problems with unknown convexity) are smooth but not convex. For those, gradient descent is known to drive the gradient norm to zero, with $\min_{k\le N}\|\nabla\Psi(x_k)\|^2=O(1/N)$, while the classical AG method has no convergence guarantee at all.

Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) modified the AG method with a third step size and proved that one algorithm handles both cases: on a smooth nonconvex problem it has the gradient-descent rate for $\min_k\|\nabla\Psi\|^2$, and when the problem turns out to be convex it keeps Nesterov's optimal rate for the optimality gap. This mission formalizes that result, Theorem 1 of the paper, and its proof path in §2.1.

Setting

Let $\Psi:\mathbb R^n\to\mathbb R$ be differentiable with Lipschitz gradient: there is $L_\Psi>0$ with

$$\|\nabla\Psi(y)-\nabla\Psi(x)\|\le L_\Psi\|y-x\|\qquad\forall x,y\in\mathbb R^n, \tag{1.2}$$

and bounded from below, with $\Psi^*=\inf_x\Psi(x)$ (problem (1.1)). $\Psi$ need not be convex.

Algorithm 1 (AG). The inputs are a starting point $x_0$ and step sizes $\{\alpha_k\},\{\beta_k\},\{\lambda_k\}$, $k\ge1$, with $\alpha_1=1$, $\alpha_k\in(0,1)$ for $k\ge2$, $\beta_k>0$ and $\lambda_k>0$. Set $x^{ag}_0=x_0$ and, for $k=1,2,\dots$,

$$x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\qquad x_k=x_{k-1}-\lambda_k\nabla\Psi(x^{md}_k),\qquad x^{ag}_k=x^{md}_k-\beta_k\nabla\Psi(x^{md}_k).$$

One gradient is evaluated per iteration, at the middle point $x^{md}_k$; $x_k$ takes a long step $\lambda_k$ and the aggregated point $x^{ag}_k$ a short step $\beta_k$. With $\beta_k=\lambda_k$ the method reduces to gradient descent, with $\beta_k=\alpha_k\lambda_k$ to a variant of Nesterov's method.

The weights are $\Gamma_1=1$, $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ ($k\ge2$), and for a horizon $N$ and $1\le k\le N$

$$C_k=1-L_\Psi\lambda_k-\frac{L_\Psi(\lambda_k-\beta_k)^2}{2\alpha_k\Gamma_k\lambda_k}\Big(\sum_{\tau=k}^N\Gamma_\tau\Big).$$

Formalization targets

Goal: Theorem 1 (p. 5)

Fix $N\ge1$.

a) If $C_k>0$ for $k=1,\dots,N$, then

$$\min_{k=1,\dots,N}\|\nabla\Psi(x^{md}_k)\|^2\le\frac{\Psi(x_0)-\Psi^*}{\sum_{k=1}^N\lambda_kC_k}.$$

b) If $\Psi$ is convex with a minimizer $x^*$, and for $k=1,\dots,N$ one has $\alpha_k\lambda_k\le\beta_k<1/L_\Psi$ and $\alpha_1/(\lambda_1\Gamma_1)\ge\alpha_2/(\lambda_2\Gamma_2)\ge\dots$, then

$$\min_{k=1,\dots,N}\|\nabla\Psi(x^{md}_k)\|^2\le\frac{\|x_0-x^*\|^2}{\lambda_1\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)},\qquad \Psi(x^{ag}_N)-\Psi(x^*)\le\frac{\Gamma_N\|x_0-x^*\|^2}{2\lambda_1}.$$

The theorem leaves the step-size policy open: any sequences meeting the conditions are covered, and the rates of Corollary 1 ($O(1/N)$ in part a, $O(1/N^2)$ for the gap in part b) follow by substitution.

Milestones

The milestones follow the proof in §2.1: the quadratic bound (2.1); Lemma 1, which unrolls the recursion $\theta_k\le(1-\alpha_k)\theta_{k-1}+\eta_k$; the nonconvex chain (2.13), (2.15), the identity for $x^{ag}_k-x_k$, (2.16), (2.17), (2.18) and (2.19); and the convex chain (2.20)–(2.25).

Significance

The result. Theorem 1 is the first convergence guarantee for an accelerated gradient method on nonconvex smooth problems. It shows that acceleration costs nothing in the nonconvex case (the same $O(1/N)$ rate for the squared gradient norm as gradient descent) while keeping the optimal $O(1/N^2)$ gap when the function is convex, so a user need not know in advance which case holds. The same analysis is the template for the composite and stochastic results of the paper (Theorems 2–4) and for the later literature on accelerated methods for nonconvex optimization.

Formalizing it. The theorem is proved on paper; it is not known to have a machine-checked proof. The mission produces a Lean definition of the AG run with its three step sizes, a formal Lemma 1 (a reusable tool for any Nesterov-type analysis), and the two chains of estimates with all constants explicit. These pieces are reused by the composite and stochastic missions of the same paper.

Difficulty

The standard analysis of Nesterov's method is an estimate-sequence or potential argument that relies on convexity at every step: it bounds $\Psi(x^{md}_k)$ below by a linearization. Without convexity that lower bound fails, and the potential need not decrease. Part a) instead tracks the decrease of $\Psi$ along the $x_k$ sequence, where gradients are evaluated at a different point $x^{md}_k$; the error this creates is governed by the gap $x^{ag}_k-x_k$, which accumulates all past gradients with weights $\Gamma_k/\Gamma_\tau$. Controlling that accumulated term, and showing it is absorbed by the condition $C_k>0$ with $C_k$ depending on the horizon $N$, is the delicate step. Part b) needs the monotonicity (2.10) to turn a weighted telescoping sum into a single initial-distance term.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n). The gradient is an explicit map g, tied to $\Psi$ by the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ (differentiable with gradient $g$, and (1.2)); $L_\Psi>0$ as in (1.2). The quadratic bound (2.1) is the published, proved ConvexOptAlg.SmoothGD.lemma_3_4.
• The run is a definition (agRun, with xSeq, xagSeq, xmdSeq), computed by (2.2)–(2.4) from $x_0$; indices are 1-based as in the paper. $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$, so $\Gamma_1=1$. $C_k$ is C LΨ α β lam N k and depends on $N$.
• "Bounded from below" is BddBelow (Set.range Ψ) and $\Psi^*$ is ⨅ x, Ψ x. The minimum over $k=1,\dots,N$ is Finset.inf' over Finset.Icc 1 N with $N\ge1$. Convexity is ConvexOn ℝ Set.univ Ψ; $x^*$ is any global minimizer.
• Conditions (2.7), (2.9), (2.10) are imposed for $k=1,\dots,N$ only.
• Trivializing formalizations are excluded: the conclusion is about the AG run itself, not an arbitrary sequence; $g$ is the gradient of $\Psi$; $\Gamma_1=1$, not $0$ (with which every bound would divide by zero); and the minimum ranges over $k\le N$, not over all $k$.

Welcome contributions: proofs of Lemma 1 and of the algebraic milestones (the identity before (2.16), (2.16), (2.17), (2.22), (2.25)), which are independent of $\Psi$; then the descent chains; then Theorem 1.

Selected references

• S. Ghadimi, G. Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, 2013; Math. Program. 156 (2016) 59–99. https://arxiv.org/abs/1310.3787
• Y. E. Nesterov, A method for unconstrained convex minimization problem with the rate of convergence O(1/k²), Doklady AN SSSR 269 (1983) 543–547.
• Y. E. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8 (2015), arXiv:1405.4980. https://arxiv.org/abs/1405.4980

Motivation

Social networks exhibit triadic closure: two people with many friends in common tend to be friends themselves. Fox, Roughgarden, Seshadhri, Wei and Wein (arXiv:1804.07431, SIAM J. Comput. 2020, doi:10.1137/18m1210459) turn this empirical regularity into a distribution-free graph class and ask which algorithmic problems that are hard on worst-case graphs become tractable on it. Their test case is the enumeration of maximal cliques, a standard primitive of community detection. On a general $n$-vertex graph the number of maximal cliques can be $3^{n/3}$ (Moon and Moser, 1965), so no enumeration algorithm can be polynomial. The question is how far triadic closure alone pushes this count down.

Timeline:

• 1965: Moon and Moser prove that every $n$-vertex graph has at most $3^{n/3}$ maximal cliques, with equality for disjoint triangles.
• 2011: Eschen, Hoàng, Spinrad and Sritharan bound the number of maximal cliques of graphs without induced $K_{2,2}$ or diamond (the 2-closed graphs) by $O(n^{3/2})$; this is the $c=2$ case of the present bound.
• 2018: Fox et al. introduce $c$-closed graphs, prove the bound $3^{(c-1)/3}n^2$ (Theorem 2.1), and improve its dependence on $n$ to $4^{(c+4)(c-1)/2}n^{2-2^{1-c}}$ (Theorem 3.1, this mission). They also show a lower bound of order $2^{c/2}n^{3/2}$ up to a polynomial factor in $c$ (Theorem 4.1).

Setting

All graphs $G=(V,E)$ are finite, simple and undirected; $N(x)$ is the set of neighbours of a vertex $x$, and for $W\subseteq V$, $G[W]$ is the subgraph induced by $W$.

For a positive integer $c$, $G$ is $c$-closed if any two distinct vertices $u,v$ with $|N(u)\cap N(v)|\ge c$ are adjacent. A 1-closed graph is a disjoint union of cliques, and every graph on $n$ vertices is $(n-1)$-closed, so $c$ interpolates between the two. Being $c$-closed passes to induced subgraphs, with common neighbours counted inside the subgraph.

A clique is a set of pairwise adjacent vertices; it is maximal if no further vertex can be added. Write $\mathrm{mc}(G)$ for the number of maximal cliques of $G$, and

$$F(n,c)=\max\{\mathrm{mc}(G): G \text{ is a } c\text{-closed graph on } n \text{ vertices}\}.$$

The proof uses four further objects, computed in the current induced subgraph: the maximum degree $\Delta(G)$; for a non-empty set $S$ of vertices, $N(S)=\bigcap_{u\in S}N(u)$; the set $N_2(v)$ of vertices at distance exactly $2$ from $v$; and the function

$$F_0(m,c)=4^{(c+4)(c-1)/2}\,m^{\,2-2^{1-c}}.$$

Formalization targets

Goal: Theorem 3.1

For all positive integers $c,n$ and every $c$-closed graph $G$ on $n$ vertices,

$$\mathrm{mc}(G)\;\le\;4^{(c+4)(c-1)/2}\,n^{\,2-2^{1-c}}.$$

For fixed $c$ the exponent $2-2^{1-c}$ is $1,\ 3/2,\ 7/4,\dots$, strictly below $2$, which is what the improvement over Theorem 2.1 consists of. The constant is the one printed in the theorem.

Milestones

The milestones follow the proof on pp. 9–11:

1. $c$-closedness is hereditary (p. 3).
2. Lemma 3.2: $G[N(v)]$ is $(c-1)$-closed (p. 9).
3. The maximal cliques containing $v$ are in bijection with the maximal cliques of $G[N(v)]$ (Case 1, p. 9).
4. Inequality (2): the maximal cliques $\mathcal K$ that meet $N(v)$ but avoid $v$ satisfy $|\mathcal K|\le\sum_{S}\mathrm{mc}(G[N(S)\cap N_2(v)])$ (p. 9).
5. Inequality (3): $\sum_S|N(S)\cap N_2(v)|\le|N_2(v)|2^{c-1}\le\min\{\Delta^2,n\}2^{c-1}$ (p. 9).
6. Inequality (4) and its consequence in Case 2, where $\Delta>\sqrt n$: given the bound at level $c-1$, the number of maximal cliques meeting $N(v)\cup\{v\}$ is strictly less than $F_0(\Delta,c-1)\min\{\Delta,n/\Delta\}2^c$ (p. 10).
7. Claim 3.3: $(1-x)^k\le1-xk/2$ for $0<x\le1/2$, $1\le k\le2$ (p. 11).
8. The arithmetic of the inductive step: $F_0(n,c)$ dominates both branches of the recurrence (pp. 10–11).

Significance

Together with Theorem 2.1, Theorem 3.1 gives Theorem 1.4 of the paper: a $c$-closed graph on $n$ vertices has at most $\min\{3^{(c-1)/3}n^2,\ 4^{(c+4)(c-1)/2}n^{2-2^{1-c}}\}$ maximal cliques. For constant $c$ the count is polynomial with exponent below $2$, so all maximal cliques can be listed in polynomial time, and the problem is fixed-parameter tractable in $c$. Theorem 4.1 shows the exponent cannot drop below $3/2$ for $c\ge2$, so the bound is polynomially tight for $c=2$.

The result is proved in the paper; it has not been formalized. This mission produces a machine-checked proof of Theorem 3.1 together with the steps of the paper's argument. The printed argument has gaps that a formal proof must close: the base of the exponential factor changes from $4$ to $2$ in the middle of the proof, Claim 3.3 is applied with $x=\Delta/n$ that may exceed $1/2$, the induction meets the empty graph (one maximal clique, while $F_0(0,c)=0$), and the recursion deletes $\Delta+1$ vertices where the recurrence writes $n-\Delta$. A proof that also closes the stronger base-$2$ bound, which the arithmetic suggests, would be a welcome addition.

Difficulty

The count of maximal cliques through a vertex $v$ reduces to $G[N(v)]$, which is $(c-1)$-closed, so a naive induction on $c$ gives $\mathrm{mc}(G)\le n\,F(\Delta,c-1)$. When the maximum degree $\Delta$ is large this is no better than $n^2$. The high-degree case needs a separate count of the cliques that meet $N(v)$ without containing $v$, grouped by their trace on $N(v)$; bounding the sum over these traces requires the convexity of $F_0$ in its first argument and the constraint coming from $c$-closedness. The resulting recurrence then has to be solved with explicit real exponents of the form $2-2^{1-c}$, for all $c$ simultaneously, with the induction on $n$ and $c$ arranged so that the empty graph never enters the inductive hypothesis.

Formalization scope

• A graph on $n$ vertices is a SimpleGraph (Fin n). The general statements are over a finite vertex type with decidable equality.
• $c$-closedness counts common neighbours with Set.ncard and reads "at least $c$" as c ≤ ncard, not c < ncard. The relative notion IsCClosedOn c G W counts common neighbours inside $W$ and is equivalent to $c$-closedness of G.induce W.
• A maximal clique of $G[W]$ is a Finset $K\subseteq W$ that is maximal under inclusion among cliques contained in $W$; the empty graph has exactly one maximal clique. Neither all cliques nor maximal cliques of a different graph are counted.
• All powers in the bounds are real powers with the cast to $\mathbb R$ taken before subtraction; $n/\Delta$ is real division.
• The milestones are stated for an induced subgraph $G[W]$ with $N_2(v)$ computed inside $G[W]$, since the proof recurses on induced subgraphs; the paper states them for $W=V$.
• Added hypotheses, relative to the page: the inductive hypothesis of milestone 6 is an explicit premise restricted to non-empty vertex sets (it is false for the empty one); milestone 6 assumes $c\ge2$ and $\Delta\ge1$, and explicitly carries Case 2's $\Delta>\sqrt n$. Milestones 4 and 5 sum over non-empty $S$ only, as the paper defines $N(S)$ only for non-empty $S$; this strengthens them. Milestone 8 is stated with the base $4$ of $F_0$ although the page prints the display with base $2$.
• The paper's $F(n,c)$ is not defined; the goal quantifies over all graphs, which is equivalent.

Everything is built from Mathlib's SimpleGraph, commonNeighbors, IsClique, Maximal and Real.rpow. The definitions of $c$-closedness and of the maximal-clique count come from the reviewed shared module CClosedGraphs.Peeling.Setting. Contributions welcome: proofs of the milestones, a proof of the goal by a different route, and the base-$2$ strengthening.

Selected references

• J. Fox, T. Roughgarden, C. Seshadhri, F. Wei, N. Wein, Finding cliques in social networks: a new distribution-free model, arXiv:1804.07431v1, 2018; SIAM J. Comput., 2020. https://arxiv.org/abs/1804.07431, https://doi.org/10.1137/18m1210459
• J. W. Moon, L. Moser, On cliques in graphs, Israel J. Math. 3, 1965. https://doi.org/10.1007/BF02760024
• E. M. Eschen, C. T. Hoàng, J. P. Spinrad, R. Sritharan, On graphs without a $C_4$ or a diamond, Discrete Appl. Math. 159(7):581–587, 2011.

Motivation

Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.

The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.

Setting

The objective is a differentiable function $f:\mathbb R^n\to\mathbb R$ bounded below, with true optimal value $f^*=\inf_x f(x)$. Its gradient map $g=\nabla f$ is $L$-Lipschitz: $\|g(y)-g(x)\|\le L\|y-x\|$ for all $x,y$. The mission uses $L>0$. No convexity is assumed.

A stochastic first-order oracle returns a vector $G(x_k,\xi_k)$ when called at the current iterate $x_k$. Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most $\sigma^2$. The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes $\sigma>0$ because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.

A randomized stochastic gradient run starts at $x_1$ and uses $x_{k+1}=x_k-\gamma_k G(x_k,\xi_k)$. It chooses an output index $R\in\{1,\ldots,N\}$ with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs $x_R$. For a parameter $\widetilde D>0$, the constant stepsize in equation (2.13) is $\gamma_k=\min\{1/L,\widetilde D/(\sigma\sqrt N)\}$. The paper writes $D_f=\sqrt{2(f(x_1)-f^*)/L}$ and

$$\mathcal B_N=\frac{LD_f^2}{N}+\left(\widetilde D+\frac{D_f^2}{\widetilde D}\right)\frac{\sigma}{\sqrt N}.$$

The two-phase method makes $S$ independent RSG runs, yielding $\bar x_1,\ldots,\bar x_S$. For each candidate it averages $T$ fresh oracle outputs into an estimated gradient $\widehat g_s$. It selects a candidate $\bar x^*$ whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.

Formalization targets

The first target is the one-run mean bound of Corollary 2.2, $L^{-1}\mathbb E\|g(x_R)\|^2\le\mathcal B_N$, followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.

For arbitrary positive $S,N,T$, Theorem 2.4(a) states the stronger quantitative tail bound

$$\Pr\left\{\|g(\bar x^*)\|^2\ge2\left(4L\mathcal B_N+\frac{3\lambda\sigma^2}{T}\right)\right\}\le\frac{S+1}{\lambda}+2^{-S}\qquad(\lambda>0).$$

The goal, Theorem 2.4(b), specializes those parameters to an accuracy $\varepsilon>0$ and failure probability $0<\Lambda<1$. It sets

$$S=\left\lceil\log_2\frac2\Lambda\right\rceil,\qquad N=\left\lceil\max\left\{\frac{32L^2D_f^2}{\varepsilon},\left(\frac{32L(\widetilde D+D_f^2/\widetilde D)\sigma}{\varepsilon}\right)^2\right\}\right\rceil,\qquad T=\left\lceil\frac{24(S+1)\sigma^2}{\Lambda\varepsilon}\right\rceil.$$

An $(\varepsilon,\Lambda)$-solution is a point satisfying $\Pr\{\|g(\bar x^*)\|^2\le\varepsilon\}\ge1-\Lambda$. With those parameter values, the method computes such a point using at most $S(N+T)$ stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.

Significance

The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.

The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.

Difficulty

Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's $1,\ldots,S$. The objective's true infimum is carried by IsGLB (Set.range f) fstar, so $D_f$ cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.

All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final $2^{-S}\le\Lambda/2$ comparison. Positive $\sigma$ and $\widetilde D$ avoid zero steps and an empty post-optimization average.

The formal goal states the probability guarantee. The $S(N+T)$ oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.

Selected references

• Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. arXiv:1309.5549v1.

Motivation

In a prophet inequality, a gambler sees prizes one at a time and must decide when to stop, while a prophet knows every realization and takes the largest. A stopping guarantee compares the gambler’s expected prize with the prophet’s. The order of arrival changes the problem: here the prizes are independent but can have different distributions, and every permutation of their arrival is equally likely. Before seeing any prize, the gambler chooses a threshold for each distribution and accepts the first prize above its threshold. Such a rule has no need to update thresholds after observing rejections. Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld prove that this restricted rule still earns at least a $1-1/e$ fraction of the prophet’s expected maximum (Theorem 1, pp. 1455, 1459).

The random-arrival stopping model also supplies guarantees for posted-price mechanisms. A posted price gives a buyer a take-it-or-leave-it offer; the first buyer who accepts ends the sale. The paper explains the connection between its stopping rules and expected revenue under random buyer arrival (§1.1 and §5). This mission formalizes the stopping theorem itself, which is the mathematical guarantee used before that economic translation.

Setting

Let $n\ge1$, and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables with known, possibly different distributions. Their realizations arrive in a uniformly random order. A nonadaptive threshold rule chooses constants $\tau_i\in[0,\infty]$ before any realization is observed. It accepts the first arriving index $i$ with $X_i>\tau_i$ and receives $X_i$. If no prize crosses its threshold, its reward is zero. An infinite threshold deliberately excludes an index. The strict comparison matches Theorem 1, even though an earlier description in §1.2 uses a weak comparison (pp. 1454–1455).

For fixed realized prizes, write $Y_i=\mathbf1_{\{X_i>\tau_i\}}$. Conditional on the set of indices with $Y_i=1$, each accepted index is equally likely to arrive first. The conditional expected reward is therefore

$$R_\tau(X)=\frac{\sum_{i=1}^{n}X_iY_i}{\sum_{i=1}^{n}Y_i},\qquad 0/0:=0.$$

The prophet benchmark is $X^*=\max_i X_i$. The theorem compares $\mathbb E R_\tau(X)$ with $\mathbb E X^*$, including distributions for which either expectation may be infinite. The variables need no common distribution and no atomlessness assumption.

The paper’s main supporting result is the Bernoulli Selection Lemma. It starts with independent Bernoulli indicators $Y_i$ of success probabilities $q_i$, fixed real prizes $b_i$, and a chosen subset $S$. Its payoff is the average $\sum_{i\in S}b_iY_i/\sum_{i\in S}Y_i$, again zero when the denominator vanishes. The lemma compares the best subset with a finite linear optimization problem over $0\le z_i\le q_i$ and $\sum_i z_i\le1$ (Lemma 1, p. 1455).

Formalization targets

Nonadaptive threshold guarantee

The goal is the exact constant of Theorem 1:

$$\exists\tau\in[0,\infty]^n:\quad \mathbb E R_\tau(X)\ \ge\ (1-e^{-1})\,\mathbb E X^*.$$

The quantifiers range over every finite nonempty family of independent nonnegative variables. The thresholds are deterministic and indexed by the distributions, and the assertion covers atoms as well as continuous laws. This is the paper’s headline nonadaptive result (Theorem 1, p. 1459).

Bernoulli selection and comparison steps

The milestone list includes the paper’s multilinear formulation (4), its substitution (5), Proposition A.1, Lemmas 2 and 3, and the Bernoulli Selection Lemma. The latter states, in particular, that the maximum expected selected average dominates $(1-e^{-1})$ times the optimum over feasible $z$. Two further milestones express the decomposition of the expected maximum and the upper-tail comparison used for continuous distributions (§2–3 and Appendix A). These targets fix the finite selection problem and the probabilistic quantities that the goal must connect.

Significance

The guarantee identifies what fixed, distribution-specific thresholds can achieve under random arrival: the expected accepted prize reaches a constant fraction of the prophet’s benchmark for every collection of independent nonnegative distributions. The paper also gives examples showing why a rule that keeps every positive prize is inadequate and studies where the $1-e^{-1}$ factor is tight (§2.1 and §3.1). These are claims about the performance of a restricted class of stopping rules, not about an optimal adaptive strategy.

The paper proves Theorem 1; a machine-checked proof of this mission’s goal remains to be supplied. The finite Bernoulli model, its subset optimum, and the nonnegative expectation conventions would be reusable for other random-order stopping and allocation results. This mission makes the paper’s claimed constants, event comparisons, and boundary cases explicit in the theorem statements so a later proof has a fixed target.

Difficulty

Taking the first value above a single low threshold can accept a modest prize before a rare large one arrives. Raising every threshold can instead reject too many prizes. The paper’s example with a constant prize and a rare large prize shows that accepting all available values does not meet the claimed factor (p. 1460). The difficulty is obtaining one set of fixed thresholds that balances those risks across different distributions, while the benchmark selects the largest realization after seeing them all. The Bernoulli selection inequality carries the sharp constant; connecting it to general distributions must also account for ties and atoms.

Formalization scope

Lean represents the index set by Fin n with $n\ge1$, so its index zero is the paper’s index one. The existing published definition SamuelCahnProphet.Median.Setting.maxX supplies the sample maximum; this mission defines the strict accepted set and its real-valued reward ratio. Thresholds live in $[0,\infty]$ because the paper explicitly uses $\infty$ to exclude a variable. Expectations are nonnegative extended integrals of ENNReal.ofReal, preserving infinite values and avoiding a default zero for nonintegrable real integrals. The source’s nonnegativity assumption is represented almost surely, which is enough for these expectations and does not restrict the distributions further.

The Bernoulli law is a finite product formula. Its probabilities lie in $[0,1]$, while prizes are arbitrary real numbers as in the printed lemma. The feasibility condition includes $z_i\ge0$: these variables are probabilities, and allowing negative values would change the optimization problem. The finite subset optimum is an attained maximum. Proposition A.1 is stated for $M\ne\varnothing$; an empty $M$ contradicts the budget conclusion for $a>0$. It also includes the printed $a=0$ case. Lemma 2 includes $y=1$ as printed: the removable division by zero in (6) is assigned its continuous value $2/e$. The comparison milestones for continuous distributions assume atomlessness explicitly; the goal does not.

The accepted set depends only on fixed thresholds and the realized values. It cannot depend on the sampled arrival order or on prior observations. A constant choice such as accepting every positive prize does not prove the target guarantee. Contributions that establish the finite Bernoulli selection result, its analytic bounds, the random-order reward identity, or the passage from continuous to arbitrary distributions all serve the stated goal. The random-order identity and the discontinuous case are further work beyond the current milestone list.

Selected references

• José Correa, Patricio Foncea, Ruben Hoeksma, Tim Oosterwijk, and Tjark Vredeveld, Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals, Mathematics of Operations Research 46(4), 1452–1478, 2021. DOI: 10.1287/moor.2020.1105.

Motivation

Mobile devices run applications whose computational demand often exceeds what a battery-powered processor can serve with acceptable delay. Computation offloading sends part of the work elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. When many users share one cloudlet, each user's response time depends on how much the others offload, and selfish users interact strategically. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016) model this interaction as a generalized Nash equilibrium problem (GNEP): every user minimises its own expected cost, and all users share a coupling constraint that caps the cloudlet's utilisation.

The paper computes equilibria through a variational inequality (VI) reformulation and, for distributed computation, through an extended game with a price player. The convergence of the methods it relies on (proximal-point and best-response schemes for monotone VIs, see Facchinei and Pang, 2003) requires the VI map to be monotone. This mission formalizes the paper's Theorem 1, which gives an explicit, checkable condition on the model's parameters under which that map is monotone.

Setting

There are $N$ users $u=1,\dots,N$. Each user splits its task stream over three tiers $I=\{m,\mathit{clet},\mathit{cloud}\}$ (own device, cloudlet, cloud) and chooses fractions $x_u=(x_{u,m},x_{u,clet},x_{u,cloud})$; a strategy profile is $x\in\mathbb R^{3N}$. The data are positive rates combined into $\alpha_u,\beta_u,\gamma_u,\delta_u$ (the traffic intensities a user generates on its device, the wireless link, the cloud path and the cloudlet), power parameters $P_{u,m},P_{u,t},P_{u,\max}$, the number $n$ of cloudlet servers, the offloadable fraction $\chi\in(0,1]$ and the utilisation cap $U_{\max}$.

The cloudlet load is $\frac1n\sum_v\delta_vx_{v,clet}$ and $D(x)=1-\frac1n\sum_t\delta_tx_{t,clet}$. User $u$'s private feasible set $\tilde K_u$ consists of the $x_u\ge0$ with $\sum_{i}x_{u,i}=1$, $x_{u,clet}+x_{u,cloud}\le\chi$ and the power budget $\alpha_uP_{u,m}x_{u,m}+\beta_uP_{u,t}(x_{u,clet}+x_{u,cloud})\le P_{u,\max}$. The shared constraint is $\Omega=\{x:\frac1n\sum_u\delta_ux_{u,clet}\le U_{\max}\}$, and the joint feasible set is $K=(\prod_u\tilde K_u)\cap\Omega$. User $u$ minimises

$$\lambda_uR_u(x)=\frac{\alpha_ux_{u,m}}{1-\alpha_ux_{u,m}}+\beta_ux_{u,clet}+\gamma_ux_{u,cloud}+\frac{\delta_ux_{u,clet}}{D(x)}.$$

Assumption A requires $U_{\max}$ and all $\alpha_u,\delta_u$ to lie in $(0,1)$.

The VI map $F:\mathbb R^{3N}\to\mathbb R^{3N}$ stacks each user's gradient in its own variables:

$$F(x)_u=\Big(\frac{\alpha_u}{(1-\alpha_ux_{u,m})^2},\ \beta_u+\delta_u\frac{1-\frac1n\sum_{v\ne u}\delta_vx_{v,clet}}{D(x)^2},\ \gamma_u\Big).$$

$F$ is monotone on $K$ if $(F(y)-F(x))^\top(y-x)\ge0$ for all $x,y\in K$. Finally $\delta_{\max}=\max_u\delta_u$.

Formalization targets

Goal: Theorem 1

Under Assumption A, if

$$\delta_{\max}\le\frac{n}{N\chi}(1-U_{\max}),\tag{18}$$

then $F$ is monotone on $K$. The condition involves only the data of the game, so the goal is the paper's statement with no constant changed.

Milestones

The milestones follow the paper's argument in order.

1. A map whose Jacobian is positive semidefinite on a convex set is monotone there (p. 12, citing Facchinei–Pang).
2. The Jacobian $JF(x)$ has the sparse structure (16), with nonzero entries $A_u$, $B_u$, $B_{uv}$ given by (17).
3. On $K$, $JF(x)$ is positive semidefinite as soon as the symmetric part $B^s=\frac12(B^\top+B)$ of its clet block is.
4. The identity (20): $B^s=\frac1{nD^2}\big(\delta\delta^\top\circ(I+E+\frac1{nD}(x^\delta_{clet}e^\top+e(x^\delta_{clet})^\top))\big)$, with $\circ$ the Hadamard product, $E$ the all-ones matrix and $x^\delta_{clet}=(\delta_ux_{u,clet})_u$.
5. The Schur product theorem (a published platform theorem).
6. The characteristic polynomial (21) of $ve^\top+ev^\top$, namely $\eta^{N-2}(\eta^2-2(e^\top v)\eta+(e^\top v)^2-N\|v\|^2)$.
7. The sufficient condition (22): $\frac1{nD}(\sqrt N\|x^\delta_{clet}\|-e^\top x^\delta_{clet})\le1$ implies $B^s\succeq0$.
8. The bound (23) on $K$: $\frac1{nD}(\sqrt N\|x^\delta_{clet}\|-e^\top x^\delta_{clet})\le\frac1{nD}\delta_{\max}\chi\sqrt N(\sqrt N-1)\le\frac{\delta_{\max}}{1-U_{\max}}\frac{N\chi}{n}$.

Significance

Theorem 1 is the hypothesis under which the rest of the paper operates. The extended game of §5.2 inherits the monotonicity properties of $F$ (p. 14), and the distributed solution methods of §6 are designed for that monotone setting. Condition (18) translates monotonicity into a statement about the system: the largest per-user cloudlet traffic intensity must stay below a threshold that grows with the number $n$ of servers and shrinks with $N$, $\chi$ and $U_{\max}$. Remark 1 (p. 14) stresses that (18) is only sufficient.

The result is proved in the paper; this mission produces a machine-checked proof. On the way it yields statements reusable outside this model: the Jacobian criterion for monotonicity of a differentiable map on a convex set, and the spectrum of the symmetric rank-two matrix $ve^\top+ev^\top$. None of these statements is on the platform; the Schur product theorem, which the proof also uses, is referenced as a published platform theorem.

Difficulty

The Jacobian $JF(x)$ is not symmetric: $B_{uv}$ carries the row user's own term $\frac2n\delta_ux_{u,clet}$, so $B_{uv}\ne B_{vu}$ in general, and the eigenvalues of $JF(x)$ say nothing directly about its quadratic form. The quadratic form must be controlled uniformly over the whole feasible set $K$, whose shape (simplices cut by the cap $\chi$, the power budgets and the shared constraint) enters the final bound, and the condition must come out in the paper's exact constants. In Lean, the main costs are the coordinatewise Fréchet derivative of $F$ on $\mathbb R^{3N}$, the characteristic polynomial of a rank-two matrix of arbitrary size, and the passage from a characteristic polynomial to positive semidefiniteness.

Formalization scope

Users are Fin N (0-based); tiers are a three-element type Tier; a profile is Fin N → Tier → ℝ. The inner product on $\mathbb R^{3N}$ is written out as $\sum_u\sum_i a_{u,i}b_{u,i}$, and the norm on $\mathbb R^N$ in (21)–(23) is the Euclidean norm written as $\sqrt{\sum_uv_u^2}$, because Mathlib's norm on function types is the sup norm. $F$ is defined by the closed form of p. 11, not as a derivative, so milestone 2 has content. $\delta_{\max}$ is the real supremum of the $\delta_u$, which is the maximum for $N\ge1$.

Standing hypotheses carried by every statement: Assumption A, $n\ge1$ and $0<\chi\le1$. Disclosed choices relative to the page:

• (21) is stated for an arbitrary $v\in\mathbb R^N$ and assumes $N\ge2$, so that $\eta^{N-2}$ is a polynomial;
• (22) is stated at any profile with $D>0$;
• (20) is stated at any profile with $D\ne0$;
• the derivative (16)–(17) is stated on the open region $\alpha_ux_{u,m}<1$, $\frac1n\sum_t\delta_tx_{t,clet}<1$, which contains $K$;
• in milestone 1, differentiability is required at each point of the convex set (in a full neighbourhood).

The formulas for $F$, $A_u$, $B_u$ and $B_{uv}$ divide by $1-\alpha_ux_{u,m}$ and $D$, and Lean sets $a/0=0$. Every statement is therefore restricted to $K$ or to a region where these denominators are nonzero; monotonicity on the larger set $\prod_u\tilde K_u$, where $D$ can vanish, is a different and false-by-junk claim and is not posed. $K$ is nonempty for admissible data (e.g. all users computing locally), so the goal is not vacuous.

Contributions welcome: proofs of any milestone, especially the generic ones (1 and 6), which belong in a general library.

Selected references

• V. Cardellini, V. De Nitto Personé, V. Di Valerio, F. Facchinei, V. Grassi, F. Lo Presti, V. Piccialli, A game-theoretic approach to computation offloading in mobile cloud computing, Mathematical Programming, 2016. https://doi.org/10.1007/s10107-015-0881-6 (accepted manuscript: IRIS Sapienza, handle 11573/779661).
• F. Facchinei, J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, vols. I–II, Springer, 2003 (the paper's [17]). https://doi.org/10.1007/b97543
• F. Facchinei, C. Kanzow, Generalized Nash equilibrium problems, Annals of Operations Research 175 (2010), 177–211 (the paper's [16]). https://doi.org/10.1007/s10479-009-0653-x
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1990 (the paper's [24]; Schur product theorem, Theorem 7.5.3). https://doi.org/10.1017/CBO9780511810817
• D. S. Bernstein, Matrix Mathematics: Theory, Facts, and Formulas with Application to Linear Systems Theory, Princeton University Press, 2005 (the paper's [6]; Fact 4.9.16). https://press.princeton.edu/books/hardcover/9780691118024

Motivation

Twin-width was introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021) as a graph parameter under which first-order model checking is fixed-parameter tractable when a contraction sequence is given. Its interest lies in the classes it covers at once: planar and, more generally, $K_t$-minor-free graphs, bounded-degree grids, unit ball graphs of bounded clique number, and the classes of bounded rank-width or clique-width. These are the classical dense-graph width measures, for which FO (indeed MSO$_1$) model checking was already known to be tractable through Courcelle–Makowsky–Rotics.

This mission formalizes the link to the dense width measures, stated in the paper through boolean-width (Bui-Xuan, Telle and Vatshelle, Theor. Comput. Sci. 412(39), 2011). It is known that $\operatorname{boolw}(G)\le\operatorname{modw}(G)\le\operatorname{cw}(G)\le 2^{\operatorname{rw}(G)+1}-1$ (Vatshelle's PhD thesis, Chapter 4), so a bound on twin-width in terms of boolean-width shows that bounded twin-width captures bounded rank-width, clique-width, module-width and boolean-width simultaneously.

Setting

Let $G$ be a finite simple graph on a vertex set $V$.

Two vertex sets $X,Y\subseteq V$ are homogeneous if either all pairs $(x,y)\in X\times Y$ are edges or none is. For a partition $\mathcal P$ of $V$, a part $X$ has red degree equal to the number of other parts $Y\ne X$ that are not homogeneous to $X$; $\mathcal P$ is a $d$-partition if every part has red degree at most $d$. The graph $G$ has twin-width at most $d$, written $\operatorname{tww}(G)\le d$, if there are partitions $\mathcal P_0,\dots,\mathcal P_N$ of $V$ with $\mathcal P_0$ the partition into singletons, $\mathcal P_N$ having at most one part, each $\mathcal P_{i+1}$ obtained from $\mathcal P_i$ by merging two parts, and every $\mathcal P_i$ a $d$-partition. This is the paper's partition form (p. 3:32) of its definition through trigraphs and red edges (pp. 3:11–3:12).

A decomposition tree of $G$ is a rooted binary tree $T$, every internal node having exactly two children, whose leaves are in one-to-one correspondence with $V$. Each edge $e$ of $T$ lies above exactly one rooted subtree and induces a cut $P_e=(A_e,B_e)$ of $V$: $A_e$ is the set of leaf labels of that subtree and $B_e=V\setminus A_e$. For disjoint $A,B$ write

$$\nu_G(A,B)=\bigl|\{N(S)\cap B: S\subseteq A\}\bigr|,$$

the number of different neighbourhoods in $B$ of subsets of $A$, the empty subset included. The boolean-width of the cut is $\log_2\nu_G(A,B)$, the boolean-width of $T$ is its maximum over the edges of $T$, and $\operatorname{boolw}(G)$ is the minimum over all decomposition trees. In Lean, nbhdCount G A B is $\nu_G(A,B)$, and BoolWidthLE G N states that some decomposition tree has $\nu_G(A_e,B_e)\le N$ on every edge, so $\operatorname{boolw}(G)\le k$ is BoolWidthLE G (2^k).

Formalization targets

Goal: Theorem 4.2 (p. 3:14)

Every graph with boolean-width $k$ has twin-width at most $2^{k+1}-1$. With $N=2^{k}$, the integer neighbourhood count,

$$\operatorname{BoolWidthLE}(G,N)\ \Longrightarrow\ \operatorname{tww}(G)\le 2N-1 .$$

Milestones (proof of Theorem 4.2, p. 3:14)

1. A graph with at most $N$ vertices has $\operatorname{tww}(G)\le N$.
2. A rooted binary tree with more than $2N$ leaves ($N\ge1$) has a rooted subtree below some edge with between $N+1$ and $2N$ leaves.
3. If $\nu_G(A,B)\le N$ and $|A|\ge N+1$, two distinct vertices of $A$ have the same neighbourhood in $B$.
4. If $(A,B)$ partitions $V$, $|A|\le 2N$, and $u\ne v\in A$ have the same neighbourhood in $B$, then contracting $u$ and $v$ yields a $(2N-1)$-partition.

Significance

The theorem places the classes of bounded boolean-width, and therefore of bounded clique-width and rank-width, inside the classes of bounded twin-width, with a single-exponential bound. Combined with the paper's model-checking algorithm, it recovers tractability of FO model checking on these classes once a contraction sequence is computed, and it situates twin-width as a common generalization of the dense width measures and of sparse classes such as $K_t$-minor-free graphs.

No machine-checked version of twin-width or boolean-width is known to exist; neither notion is in Mathlib. The mission produces Lean definitions of twin-width in partition form, of decomposition trees and of the neighbourhood count behind boolean-width, together with the four combinatorial steps the paper's proof states explicitly. The definitions are shared, in identical form, with the other missions of this series on the same paper.

Difficulty

The first three milestones are elementary: a counting bound on contraction sequences, a walk down a binary tree, and a pigeonhole argument. The fourth is a direct count of non-homogeneous parts.

The difficulty is the iteration. After the first contraction the leaves of the updated tree are contracted vertices, so "the same neighbourhood in $B_e$" must be read as homogeneity to all of $B_e$ for a set of vertices, and the boolean-width bound of the cuts must be re-established for sets rather than single vertices. The paper asserts the invariant that the contractions never create a red component of more than $2^{k+1}$ vertices without proving it. A complete proof of the goal therefore has to supply an invariant, carried through all $|V|-1$ contractions, that keeps every part's red degree below $2N-1$. The naive repetition of the first step does not by itself control red edges between previously contracted parts.

Formalization scope

Twin-width is the predicate TwinWidthLE G d, never a numerical infimum, so a junk value of an empty or unbounded infimum cannot make the goal trivial. A contraction sequence must merge exactly two parts at each step and start from singletons; it cannot jump to one part. Homogeneity counts all pairs between two parts, in both of its alternatives. Boolean-width is bounded on every edge of the decomposition tree, not only at the root, and the count runs over neighbourhoods of all subsets of $A_e$, not only of single vertices. The bound $2N-1$ depends only on $N$, not on the graph.

Boolean-width is kept as the integer count $N=2^{\operatorname{boolw}(G)}$; since $\operatorname{boolw}(G)=k$ means that the least admissible count is $2^k$, the Lean goal for this $N$ is exactly the printed theorem. Subtractions $2N-1$ are in $\mathbb N$ and exact where used. Graphs live on a Fintype vertex type with decidable equality and decidable adjacency. A graph on the empty vertex set has no decomposition tree; the goal is silent about it, and it has twin-width $0$. No hypothesis is added to any statement relative to the page except $N\ge 1$ in milestone 2, which the page has implicitly ($2^k\ge1$) and without which the conclusion is impossible.

The definitions needed are the setting module TwinWidthI.BoolWidth.Setting: merge steps, homogeneity, $d$-partitions, twin-width, decomposition trees (DTree), the count $\nu_G$ and BoolWidthLE. Proofs of the milestones, a proof of the goal, and lemmas towards the iteration invariant are welcome.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé and R. Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655
• B.-M. Bui-Xuan, J. A. Telle and M. Vatshelle, Boolean-width of graphs, Theoretical Computer Science 412(39), 5187–5204, 2011. https://doi.org/10.1016/j.tcs.2011.05.022
• M. Vatshelle, New Width Parameters of Graphs, PhD thesis, University of Bergen, 2012 (reference [39] of Bonnet et al.; source of the chain boolw ≤ modw ≤ cw ≤ 2^{rw+1} − 1).