Convex Optimization

Motivation

Nesterov's accelerated gradient method (Nesterov, 1983) minimizes a smooth convex function $f$ with the update

$$x_k=y_{k-1}-s\nabla f(y_{k-1}),\qquad y_k=x_k+\frac{k-1}{k+2}(x_k-x_{k-1}),$$

and, for step size $s\le 1/L$, attains $f(x_k)-f^\star\le 2\|x_0-x^\star\|^2/(s(k+1)^2)$. The rate $O(1/k^2)$ is optimal among first-order methods, yet the classical proof proceeds by an "estimate sequence" argument that offers little insight into why the momentum coefficient $(k-1)/(k+2)$ works.

Su, Boyd and Candès (arXiv:1503.01243, J. Mach. Learn. Res. 17, 2016) showed that, as $s\to0$, the iterates track the solution of the second-order ordinary differential equation

$$\ddot X+\frac3t\dot X+\nabla f(X)=0,\qquad X(0)=x_0,\ \dot X(0)=0,$$

under the time identification $t\approx k\sqrt s$. Their Theorem 3 is the continuous-time counterpart of Nesterov's rate. Its short proof by an energy (Lyapunov) function became the template for a large literature on continuous-time models of accelerated methods, including Wibisono, Wilson and Jordan's variational perspective (PNAS 2016) and Attouch, Chbani, Peypouquet and Redont's analysis of the damped system $\ddot x+\frac\alpha t\dot x+\nabla\Phi(x)=0$ (Math. Program. 2018).

This mission formalizes Theorem 3 and the three steps of its proof.

Setting

Let $n\ge0$ and let $\mathbb R^n$ carry the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For $f:\mathbb R^n\to\mathbb R$ differentiable, $\nabla f$ is its gradient.

• For $L>0$, the class $\mathcal F_L$ consists of the convex, continuously differentiable $f$ with $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$. The class $\mathcal F_\infty$ is $\bigcup_{L>0}\mathcal F_L$.
• A minimizer $x^\star$ is any point with $f(x^\star)\le f(y)$ for all $y$, and $f^\star=f(x^\star)$.
• A solution of the ODE (3) with initial point $x_0$ is a curve $X$ on $[0,\infty)$, twice continuously differentiable on $(0,\infty)$ and continuously differentiable on $[0,\infty)$, with $X(0)=x_0$, $\dot X(0)=0$, and $\ddot X(t)+\frac3t\dot X(t)+\nabla f(X(t))=0$ for every $t>0$. The damping coefficient $3/t$ is singular at $t=0$; the paper's Theorem 1 shows that a unique such solution exists for every $f\in\mathcal F_\infty$.
• The energy along a solution is

$$\mathcal E(t)=t^2\big(f(X(t))-f^\star\big)+2\Big\|X(t)+\frac t2\dot X(t)-x^\star\Big\|^2 .$$

In the Lean development these are IsFL, IsFinfty, IsSolution f 3 x₀ X V and energy f xstar X V t, in the namespace NesterovODE.Rate, where V is the velocity $\dot X$.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $f\in\mathcal F_\infty$, every minimizer $x^\star$, every $x_0$ and every solution $X$ of (3),

$$f(X(t))-f^\star\le\frac{2\|x_0-x^\star\|^2}{t^2}\qquad\text{for all }t>0.$$

Milestones (proof of Theorem 3, pp. 7–8)

1. Derivative of the energy. For $t>0$,

$$\dot{\mathcal E}=2t(f(X)-f^\star)+t^2\langle\nabla f(X),\dot X\rangle+4\Big\langle X+\frac t2\dot X-x^\star,\frac32\dot X+\frac t2\ddot X\Big\rangle .$$

2. The energy is nonincreasing. Using the ODE,

$$\dot{\mathcal E}=2t(f(X)-f^\star)+4\Big\langle X-x^\star,-\frac t2\nabla f(X)\Big\rangle=2t(f(X)-f^\star)-2t\langle X-x^\star,\nabla f(X)\rangle\le0 .$$

3. The bound chain. $\mathcal E$ is nonincreasing on $[0,\infty)$ and, for $t>0$,

$$f(X(t))-f^\star\le\frac{\mathcal E(t)}{t^2}\le\frac{\mathcal E(0)}{t^2}=\frac{2\|x_0-x^\star\|^2}{t^2}.$$

Significance

Theorem 3 is the statement that makes the ODE a faithful model of Nesterov's scheme at the level of rates: under $t\approx k\sqrt s$, the bound (7) reproduces the discrete bound (6) with the same constant 2. The paper also shows that the constant cannot be improved (p. 8). The energy $\mathcal E$ is the continuous analogue of the potential used in discrete proofs, and the same template, with other weights, gives the paper's later results on the generalized damping $r/t$ and on strongly convex objectives.

The result is proved in the paper. As far as the platform and Mathlib are concerned it is not formalized: Mathlib has the calculus (derivatives of inner products and norms along curves, the first-order characterization of convexity, monotonicity from a sign of the derivative) but no statement about this ODE. A machine-checked proof establishes the Lyapunov argument for the singular-at-zero system, including the endpoint $t=0$ where only one-sided regularity is available, and supplies reusable lemmas for the other missions of this series and for formalizations of inertial dynamics with vanishing damping.

Difficulty

The algebra is short; the care lies in the analytic bookkeeping that the paper leaves implicit.

• The energy is defined through $f\circ X$ and $\|X+\frac t2\dot X-x^\star\|^2$, so its derivative needs the chain rule for a $C^1$ function along a differentiable curve and the derivative of a squared norm of a curve.
• The ODE holds only for $t>0$ and the coefficient $3/t$ blows up at $0$. Monotonicity of $\mathcal E$ on the closed half-line therefore needs right-continuity of $\mathcal E$ at $0$, which follows from right-continuity of $X$ and $\dot X$ there, together with $t\dot X(t)\to0$; the derivative argument alone gives monotonicity only on $(0,\infty)$.
• The sign of $\dot{\mathcal E}$ needs the first-order inequality $f(x^\star)\ge f(X)+\langle\nabla f(X),x^\star-X\rangle$ for a differentiable convex function.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient f. $f\in\mathcal F_L$ is 0 < L ∧ ConvexOn ℝ Set.univ f ∧ ContDiff ℝ 1 f ∧ LipschitzWith L (gradient f) with L : NNReal.
• A solution is encoded as a pair of curves $(X,V)$: $X(0)=x_0$, $V(0)=0$, $X$ has right derivative $V(0)$ at $0$, $V$ is right-continuous at $0$, and for every $t>0$, $X$ has derivative $V(t)$ and $V$ has derivative $-\frac3tV(t)-\nabla f(X(t))$. For continuous $\nabla f$ this is exactly the paper's regularity class $C^2((0,\infty))\cap C^1([0,\infty))$ with the ODE and the initial conditions. Values of $X$ for $t<0$ are unconstrained and never used.
• The paper states Theorem 3 for "the unique global solution". The Lean statements quantify over every solution and every minimizer, which by Theorem 1 is the same statement and does not depend on Theorem 1 (formalized in a separate mission of this series).
• No hypothesis beyond the paper's is added. The Lipschitz constant is part of $\mathcal F_\infty$ and is kept although the proof of Theorem 3 does not use it quantitatively.
• The bound is stated for $t>0$ only. At $t=0$ the right-hand side $2\|x_0-x^\star\|^2/0$ is $0$ in Lean, and the inequality would be false.
• The derivative statements use HasDerivAt rather than deriv, so no derivative silently takes the default value $0$; the solution predicate is satisfiable (for $f(x)=\|x\|^2/2$, $x_0=0$, the zero curve is a solution), so the goal is not vacuous.

Contributions welcome: proofs of the three milestones and of the goal; general lemmas on the derivative of $t\mapsto f(X(t))$ and $t\mapsto\|X(t)+\frac t2V(t)-x^\star\|^2$; and the first-order convexity inequality in gradient form, which the strongly convex and generalized-damping missions of this series also need.

Selected references

• W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, J. Mach. Learn. Res. 17(153):1–43, 2016; cited from arXiv:1503.01243v2, 2015. https://arxiv.org/abs/1503.01243
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27(2):372–376, 1983.
• A. Wibisono, A. C. Wilson, M. I. Jordan, A variational perspective on accelerated methods in optimization, Proc. Natl. Acad. Sci. 113(47):E7351–E7358, 2016. https://doi.org/10.1073/pnas.1614734113
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. https://doi.org/10.1007/s10107-016-1065-5

Motivation

First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to $1/t$ after $t$ steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4

Setting

Let $X\subseteq\mathbb R^n$ and $Y\subseteq\mathbb R^m$ be closed convex sets. The primal–dual problem is $\min_{x\in X}\max_{y\in Y}L(x,y)$, where $L$ is differentiable, convex in $x$ and concave in $y$. A point $z=(x,y)$ is feasible when $z\in Z=X\times Y$. Its saddle-point set $Z^\star$ contains the feasible pairs satisfying $L(x,y')\le L(x,y)\le L(x',y)$ for every $x'\in X$ and $y'\in Y$. Distances and balls use a chosen seminorm $\|\cdot\|_p$; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3

For $r>0$, put $W_r(z)=\{\hat z\in Z:\|z-\hat z\|_p\le r\}$. The normalized duality gap is $\rho_r(z)=\sup_{\hat z\in W_r(z)}[L(x,\hat y)-L(\hat x,y)]/r$. At $r=0$ it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is $\alpha$-sharp on $S\subseteq Z$ when $\alpha\operatorname{dist}_p(z,Z^\star)\le\rho_r(z)$ for every $z\in S$ and every $0<r\le\operatorname{diam}_p(S)$. This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1

The base algorithm begins at $z^0\in Z$ and supplies averaged outputs $\bar z^t$ for positive inner times $t$. Property 3 requires constants $q,C>0$, uniform over every feasible start and output run, for which $\bar z^t\in Z$, $\rho_{\|\bar z^t-z^0\|_p}(\bar z^t)\le2C\|\bar z^t-z^0\|_p/t$, and $\|\bar z^t-z^0\|_p\le(q+2)\operatorname{dist}_p(z^0,Z^\star)$. An outer run starts at $z^{k,0}$, runs its inner algorithm for $\tau^k$ steps, and sets $z^{k+1,0}=\bar z^{k,\tau^k}$. Its first length $\tau^0\ge1$ is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below $\beta$ times the gap at the previous outer transition, with $0<\beta<1$. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)

Formalization targets

The goal is both parts of Theorem 2. Assume all outer starts lie in one set $S$ on which the problem is $\alpha$-sharp, with $\alpha>0$. Define the ceiling time $t^\star=\left\lceil2C(q+2)/(\alpha\beta)\right\rceil$. For every $k\ge1$ the target is

$$\tau^k\le t^\star, \qquad \operatorname{dist}_p(z^{k,0},Z^\star) \le\beta^k\frac{t^\star}{\tau^0}\operatorname{dist}_p(z^{0,0},Z^\star).$$

The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at $k=1$: the first interval is free and need not be at most $t^\star$. Applegate et al., arXiv:2105.12715v4, pp. 17–18

Significance

The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know $\alpha$ can have the same characteristic restart scale as one using a fixed frequency chosen from $\alpha$. The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5

Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4

Difficulty

The restart test uses a gap evaluated at the moving radius $\|\bar z^{k,t}-z^{k,0}\|_p$, whereas sharpness relates a gap at the radius of the previous outer transition to distance from $Z^\star$. This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18

Formalization scope

Lean represents $x$ and $y$ by finite-dimensional Euclidean spaces and $z$ by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. $Z^\star$ is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires $Z^\star\ne\varnothing$, a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to $Z^\star$ cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4

The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes $q,C$ before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor $t^\star/\tau^0$ is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18

Selected references

• D. Applegate, O. Hinder, H. Lu and M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Mathematical Programming, 2022; mission citation basis: arXiv:2105.12715v4.

Motivation

Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.

This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor $\beta$ per restart.

Setting

Let $X \subseteq \mathbb R^n$ and $Y \subseteq \mathbb R^m$ be closed convex sets and let $L(x, y)$ be differentiable, convex in $x$ and concave in $y$. Problem (1) is

$$\min_{x \in X} \max_{y \in Y} L(x, y),$$

with feasible region $Z = X \times Y$ and primal-dual points $z = (x, y)$. Its solution set $Z^\star$ is the set of saddle points $z^\star \in Z$: $L(x^\star, y') \le L(x^\star, y^\star) \le L(x', y^\star)$ for all $x' \in X$, $y' \in Y$. Throughout, $Z^\star \neq \emptyset$.

Distances are measured in a semi-norm $\|\cdot\|$, which the paper allows in order to cover ADMM. Write $\operatorname{dist}(z, Z^\star) = \inf_{z^\star \in Z^\star}\|z - z^\star\|$, $\operatorname{diam}(S) = \sup_{s, s' \in S}\|s - s'\|$, and $W_r(z) = \{\hat z \in Z : \|z - \hat z\| \le r\}$. The primal-dual gap (3) at $z$ is $\sup_{\hat z \in Z}\{L(x, \hat y) - L(\hat x, y)\}$, and the normalized duality gap (4a)–(4b) is

$$\rho_r(z) = \frac{1}{r}\sup_{\hat z \in W_r(z)}\{L(x, \hat y) - L(\hat x, y)\} \quad (r > 0), \qquad \rho_0(z) = \limsup_{r \to 0^+}\rho_r(z).$$

By Definition 1, problem (1) is $\alpha$-sharp on $S \subseteq Z$ if $\alpha\operatorname{dist}(z, Z^\star) \le \rho_r(z)$ for all $z \in S$ and all $r \in (0, \operatorname{diam}(S)]$.

The base method is abstract. From a start $z^0$ it outputs averaged points $\bar z^t$, $t \ge 1$. It has Property 3 with constants $q, C > 0$ if, for every start $z^0 \in Z$ and every $t \ge 1$, $\bar z^t \in Z$ and

i. $\rho_{\|\bar z^t - z^0\|}(\bar z^t) \le 2C\|\bar z^t - z^0\|/t$,

ii. $\|\bar z^t - z^0\| \le (q + 2)\operatorname{dist}(z^0, Z^\star)$.

Algorithm 1 with fixed-frequency restarts (29) runs the base method from $z^{n,0}$ for

$$t^\star = \left\lceil \frac{2C(q+2)}{\alpha\beta}\right\rceil$$

steps, sets $z^{n+1,0} = \bar z^{n,t^\star}$, and repeats, with $\beta \in (0, 1)$.

Formalization targets

Goal: Theorem 1 (p. 17)

If the base method has Property 3 and (1) is $\alpha$-sharp on $W_R(z^{0,0})$ with $R = \frac{q+2}{1-\beta}\operatorname{dist}(z^{0,0}, Z^\star)$, then for every $n \ge 0$

$$\operatorname{dist}(z^{n,0}, Z^\star) \le \beta^n \operatorname{dist}(z^{0,0}, Z^\star). \tag{31}$$

Milestones

1. Proposition 5 (p. 11): for $z \in Z$, $\rho_r(z)$ is non-increasing in $r \in [0, \infty)$.
2. Proposition 6 (p. 11): for $z \in Z$ and $r \ge 0$, the primal-dual gap at $z$ is zero if and only if $\rho_r(z) = 0$.
3. Proposition 8 (p. 17): under Property 3, $\|\bar z^t - z^0\| = 0$ implies $\bar z^t \in Z^\star$.
4. First display of the proof of Theorem 1 (p. 17): if (31) holds for all $n \le N$, then $\|z^{N+1,0} - z^{0,0}\| \le R$, so $z^{N+1,0} \in W_R(z^{0,0})$.
5. Display (32) (p. 17): if $z^{N,0}, z^{N+1,0} \in W_R(z^{0,0})$, then

$$\operatorname{dist}(z^{N+1,0}, Z^\star) \le \beta\operatorname{dist}(z^{N,0}, Z^\star).$$

Companion statements

Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates $z^t$ and targets $\hat z^t$ has Property 1 with $C$ if $L(\hat x^{t+1}, y) - L(x, \hat y^{t+1}) \le \frac C2\|z - z^t\|^2 - \frac C2\|z - z^{t+1}\|^2$ for every $z \in Z$ (12). It has Property 2 with $q$ if $\|\hat z^t - z^t\| \le q\operatorname{dist}(z^t, Z^\star)$ or $\|\hat z^t - z^{t-1}\| \le q\operatorname{dist}(z^t, Z^\star)$.

• Proposition 2: Property 1 gives non-expansiveness $\|z^{t+1} - z^\star\| \le \|z^t - z^\star\|$ and the ergodic rate $L(\bar x^t, y) - L(x, \bar y^t) \le C\|z - z^0\|^2/(2t)$.
• Proposition 4: Properties 1 and 2 give Property 3 for the averages $\bar z^t = \frac1t\sum_{i=1}^t \hat z^i$, with the same $q$ and $C$.

Fact 1 (p. 11), that $r\rho_r(z)$ is non-decreasing in $r$, is included as well.

Significance

Theorem 1 converts any primal-dual method with an $O(1/t)$ ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is $O\big(\frac{C}{\alpha}\log\frac1\epsilon\big)$ iterations to reach $\operatorname{dist}(z, Z^\star) \le \epsilon$ (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with $\alpha$ the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.

The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.

Difficulty

Each proof is short, but the statements are delicate in ways the paper passes over.

• The paper's argmax over $W_r(z)$ need not exist under a semi-norm, and $\rho_r(z)$ may be $+\infty$. Proposition 5 therefore has to be proved with suprema, through the convex-combination scaling $z + \frac{r_1}{r_2}(\hat z - z)$, not with a maximizer.
• Sharpness is only available at radii in $(0, \operatorname{diam}(W_R(z^{0,0}))]$ and only at points of $W_R(z^{0,0})$. So the induction in Theorem 1 must carry two facts together: the contraction (31), and the fact that every restart point stays in $W_R(z^{0,0})$.
• The step size $r = \|z^{N+1,0} - z^{N,0}\|$ may be zero, which is why Proposition 8, and through it Propositions 5 and 6 at $r = 0$, is needed.

A direct contraction argument that applies sharpness at an arbitrary radius, or on all of $Z$, does not prove the theorem as stated.

Formalization scope

• $\mathbb R^n$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). $n = 0$ and $m = 0$ are allowed.
• The semi-norm is an arbitrary Seminorm ℝ on their product, never the product's built-in norm.
• The primal-dual gap, $\rho_r$ and $\operatorname{diam}$ are suprema in EReal, so unbounded sets give $+\infty$ and not a junk $0$. $\operatorname{dist}(\cdot, Z^\star)$ is a real infimum over the nonempty set $Z^\star$.
• The base method is a map from starts to sets of admissible output sequences, because a primal-dual step can be an argmin and need not be single-valued. Property 3 quantifies over every start in $Z$ and every run, with $q$ and $C$ fixed first.
• The restart length is the natural number $\lceil 2C(q+2)/(\alpha\beta)\rceil$, and every inner loop has exactly this length.

Standing assumptions and added hypotheses:

• $X$ and $Y$ are closed and convex, and $L$ is convex-concave and differentiable on the whole space.
• $Z^\star \neq \emptyset$ replaces the page's "non-empty feasible region and bounded optimal value".
• $\alpha > 0$ is assumed.
• Property 1 is required for every $t \ge 0$, although the paper's $\mathbb N$ starts at one: the proof of Proposition 2 telescopes from $z^0$.
• The iterates of a generic algorithm stay in $Z$, which the page leaves implicit.

Departures from the page:

• Proposition 8 asserts only $\bar z^t \in Z^\star$. The page's "$\bar z^{n,t} = z^{n,0}$" does not follow under a semi-norm.
• Milestones that do not use a standing assumption drop it.

The goal is not trivialized by its hypotheses. A companion check file exhibits $L(x, y) = xy$ on $\mathbb R \times \mathbb R$, with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and $\operatorname{dist}(z^{0,0}, Z^\star) = 1$. Sharpness is assumed only where Definition 1 and the theorem assume it: replacing $W_R(z^{0,0})$ by $Z$, or the radius range by all $r > 0$, would weaken the theorem.

A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of $\rho_r$, sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.

Selected references

• D. Applegate, O. Hinder, H. Lu, M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Math. Program. (2022); arXiv:2105.12715v4. https://arxiv.org/abs/2105.12715 · https://doi.org/10.1007/s10107-022-01901-9
• D. Applegate, M. Díaz, O. Hinder, H. Lu, M. Lubin, B. O'Donoghue, W. Schudy, Practical Large-Scale Linear Programming using Primal-Dual Hybrid Gradient, NeurIPS 2021. https://arxiv.org/abs/2106.04756
• A. Chambolle, T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, J. Math. Imaging Vision 40 (2011). https://doi.org/10.1007/s10851-010-0251-1
• A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15 (2004). https://doi.org/10.1137/S1052623403425629

Motivation

Best subset selection with a ridge term, the $\ell_0\ell_2$-regularized least squares problem

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2,$$

is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box $|\beta_i| \le M z_i$ (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces $\beta_i^2$ by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.

Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, $\mathrm{PR}(\infty)$, studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.

Setting

Fix a design matrix $X \in \mathbb R^{n\times p}$, a response $y \in \mathbb R^n$, parameters $\lambda_0, \lambda_2 > 0$ and a bound $M > 0$. Write $[p] = \{1,\dots,p\}$ and $\|\beta\|_\infty \le M$ for $|\beta_i| \le M$ for every $i \in [p]$.

The Big-M formulation (2) is

$$\min_{\beta, z}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\sum_{i\in[p]} z_i + \lambda_2\|\beta\|_2^2 \quad\text{s.t.}\quad -Mz_i \le \beta_i \le Mz_i,\ z_i\in\{0,1\}.$$

Its interval relaxation replaces $z_i \in \{0,1\}$ by $z_i \in [0,1]$; its optimal value is $V_{B(M)}$. Eliminating $z$ gives the equivalent form (37),

$$V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta),\qquad H(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\Big(\frac{\lambda_0}{M}|\beta_i| + \lambda_2\beta_i^2\Big).$$

The reverse Huber penalty is $\mathcal B(t) = |t|$ for $|t| \le 1$ and $\mathcal B(t) = (t^2+1)/2$ for $|t| \ge 1$, and $\psi_1(b;\lambda_0,\lambda_2) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$. The interval relaxation of $\mathrm{PR}(\infty)$ has the value (6),

$$V_{PR(\infty)} = \min_{\beta\in\mathbb R^p} G(\beta),\qquad G(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2).$$

Let $\mathcal S(\lambda_2)$ be the set of minimizers of $G$, and, as in (9),

$$\mathcal L(M) = \{\lambda_2 > 0 \;:\; \exists\beta\in\mathcal S(\lambda_2) \text{ with } \|\beta\|_\infty \le M\}.$$

The comparison runs through the scalar function $t(b) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0}) - \frac{\lambda_0}{M}|b| - \lambda_2 b^2 = \psi_1(b) - \big(\tfrac{\lambda_0}{M}|b| + \lambda_2 b^2\big)$ and through $v^*(M) = \min_{\|\beta\|_\infty\le M} G(\beta)$.

Formalization targets

Goal: Proposition 2 (p. 7)

$$V_{B(M)} \ge V_{PR(\infty)}\quad\text{if } M \le \tfrac12\sqrt{\lambda_0/\lambda_2},\qquad (10)$$ $$V_{B(M)} \le V_{PR(\infty)}\quad\text{if } M \ge \sqrt{\lambda_0/\lambda_2} \text{ and } \lambda_2 \in \mathcal L(M).\qquad (11)$$

Milestones, in the order of the paper's proof

1. (37): $V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta)$, attained.
2. (10) on its own.
3. Lemma 1: for $M \ge \sqrt{\lambda_0/\lambda_2}$ and $b \in [-M, M]$, $t(b) \ge 0$.
4. (41): for $M \ge \sqrt{\lambda_0/\lambda_2}$, $v^*(M) \ge V_{B(M)}$.

The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for $M \le \frac12\sqrt{\lambda_0/\lambda_2}$ and $|b| \le M$, $t(b) = (2\sqrt{\lambda_0\lambda_2} - \lambda_0/M)|b| - \lambda_2 b^2 \le 0$.

Significance

Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of $\mathrm{PR}(\infty)$ lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small $\lambda_2$ favours the Big-M relaxation and a large $\lambda_2$ favours $\mathrm{PR}(\infty)$ (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation $\mathrm{PR}(M)$ beats both when $\sqrt{\lambda_0/\lambda_2} > M$, this motivates the paper's choice of $\mathrm{PR}(M)$ as the formulation on which its BnB solver is built.

The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.

Difficulty

The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, $|b| = \sqrt{\lambda_0/\lambda_2}$, and at the sign of $2\sqrt{\lambda_0\lambda_2} - \lambda_0/M$. The passage from coordinatewise inequalities to optimal values is where care is needed. $V_{B(M)}$ is defined over pairs $(\beta, z)$, and its identification with a minimum of $H$ over a compact box requires eliminating $z$ and showing attainment. For (11) a pointwise comparison of $G$ and $H$ on the box only bounds $V_{B(M)}$ by the box-restricted value $v^*(M)$, not by $V_{PR(\infty)}$, which is an infimum over all of $\mathbb R^p$; the hypothesis $\lambda_2 \in \mathcal L(M)$ is what closes this gap, and dropping it gives a statement the paper does not prove.

Formalization scope

All declarations live in the namespace L0BnB.BigMvsPR. Vectors are Fin p → ℝ, $X$ is a Matrix (Fin n) (Fin p) ℝ, and $X\beta$ is X *ᵥ β. Every norm is an explicit sum: $\|v\|_2^2 = \sum_i v_i^2$, and $\|\beta\|_\infty \le M$ is $\forall i,\ |\beta_i| \le M$. The reverse Huber penalty is an if on $|t| \le 1$.

Optimal values are real infima (sInf): $V_{B(M)}$ over the feasible pairs $(\beta, z)$ of the interval relaxation, $V_{PR(\infty)}$ over all of $\mathbb R^p$, $v^*(M)$ over the box. For $\lambda_0, \lambda_2 > 0$ each set of values is nonempty ($\beta = z = 0$) and bounded below by $0$, so no infimum takes Lean's junk value. $V_{PR(\infty)}$ is defined as the displayed minimum (6); its identification with the interval relaxation of $\mathrm{PR}(\infty)$ is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. $\mathcal S(\lambda_2)$ is the set of minimizers of $G$, as the paper uses it in the proof of (11).

All theorems assume $\lambda_0, \lambda_2, M > 0$. The paper remarks that Proposition 2 applies for any $M \ge 0$; $M = 0$ is excluded because $H$ and $t$ divide by $M$. The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of $H$ and $G$ is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.

The paper states no $O(\cdot)$ bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of $H$), and of the goal.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming, 2022. https://arxiv.org/abs/2004.06152
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv preprint, 2015. https://arxiv.org/abs/1510.06083
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, The Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388
• A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
• O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
• A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007 (the reverse Huber penalty).

Motivation

Best subset selection with ridge shrinkage asks for a coefficient vector $\beta\in\mathbb R^p$ that fits a response $y\in\mathbb R^n$ through a design matrix $X\in\mathbb R^{n\times p}$ while using few nonzero coefficients:

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2 .$$

This $\ell_0\ell_2$-regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound $M$ instead of the bound-free formulation.

The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.

Setting

Fix $X$, $y$, regularization parameters $\lambda_0,\lambda_2>0$ and a bound $M>0$ on $\|\beta\|_\infty$; write $[p]=\{1,\dots,p\}$.

The Big-M formulation $B(M)$ introduces indicators $z_i$ and minimizes $\tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_i z_i+\lambda_2\|\beta\|_2^2$ subject to $-Mz_i\le\beta_i\le Mz_i$, $z_i\in\{0,1\}$. Its interval relaxation lets $z_i\in[0,1]$; its optimal value is $V_{B(M)}$.

The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $(t^2+1)/2$ for $|t|\ge1$. Put

$$\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The paper's Theorem 1 shows that the interval relaxation of the perspective formulation $\mathrm{PR}(M)$ is equivalent to

$$\min_{\|\beta\|_\infty\le M} F(\beta),\qquad F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M), \tag{5}$$

and $V_{PR(M)}$ denotes the optimal value of (5). Without a bound, the relaxation value of $\mathrm{PR}(\infty)$ is

$$V_{PR(\infty)}=\min_{\beta\in\mathbb R^p}G(\beta),\qquad G(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2). \tag{6}$$

Finally $h(\lambda_0,\lambda_2,M)=\lambda_0/M+\lambda_2M-2\sqrt{\lambda_0\lambda_2}$, and $\beta^*$ denotes an optimal solution of (5).

Formalization targets

Goal: Proposition 1

For $\sqrt{\lambda_0/\lambda_2}>M$,

$$V_{PR(M)}\ \ge\ V_{B(M)}+\lambda_2\big(M\|\beta^*\|_1-\|\beta^*\|_2^2\big), \tag{7}$$ $$V_{PR(M)}\ \ge\ V_{PR(\infty)}+h(\lambda_0,\lambda_2,M)\,\|\beta^*\|_1. \tag{8}$$

Milestones

1. (37): $V_{B(M)}=\min_{\|\beta\|_\infty\le M}H(\beta)$ with $H(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_i\big(\tfrac{\lambda_0}{M}|\beta_i|+\lambda_2\beta_i^2\big)$; the Big-M relaxation expressed in $\beta$ alone. It holds for every $M>0$.
2. (7) alone.
3. The linear case of $\psi_1$: if $|b|\le M<\sqrt{\lambda_0/\lambda_2}$ then $\psi_1(b;\lambda_0,\lambda_2)=2|b|\sqrt{\lambda_0\lambda_2}$.
4. (8) alone (the paper's (38)).

The goal is the conjunction of milestones 2 and 4.

Significance

In the regime $\sqrt{\lambda_0/\lambda_2}>M$ both added terms are nonnegative: $M\|\beta^*\|_1\ge\|\beta^*\|_2^2$ because $\|\beta^*\|_\infty\le M$, and $h>0$ because $\lambda_0/M+\lambda_2M>2\sqrt{\lambda_0\lambda_2}$ whenever $M\ne\sqrt{\lambda_0/\lambda_2}$. So the perspective relaxation is at least as strong as both the Big-M relaxation and $\mathrm{PR}(\infty)$, strictly so as soon as one coordinate of $\beta^*$ lies strictly inside $(0,M)$ in absolute value (for (7)) or $\beta^*\ne0$ (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on $\mathrm{PR}(M)$ with a valid, tight $M$; the regime $\sqrt{\lambda_0/\lambda_2}\le M$, where (5) is (6) with the additional box constraint $\|\beta\|_\infty\le M$, is complementary.

Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.

Difficulty

The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument "$V_{PR(M)}-V_{B(M)}\ge F(\beta^*)-H(\beta^*)$" requires that the Big-M relaxation, which is posed over pairs $(\beta,z)$, have value at most $H(\beta^*)$; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs $V_{PR(\infty)}\le G(\beta^*)$, i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime $\sqrt{\lambda_0/\lambda_2}>M$, in which $\psi=\psi_2$. Dropping the regime hypothesis makes (8) false in general: for $\sqrt{\lambda_0/\lambda_2}\le M$ one has $\psi=\psi_1$ and $h\ge0$, and the right side can exceed $V_{PR(M)}=V_{PR(\infty)}$.

Formalization scope

All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; $[p]$ is Fin p. Norms are explicit sums: $\|v\|_2^2$ is ∑ i, v i ^ 2, $\|\beta\|_1$ is ∑ i, |β i|, and $\|\beta\|_\infty\le M$ is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).

Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty ($\beta=0$, $z=0$) and bounded below by $0$ under the positivity hypotheses, so sInf is the true infimum and never a junk value. $V_{B(M)}$ is defined over pairs $(\beta,z)$ with $z_i\in[0,1]$, not through $H$; (37) is a theorem. $V_{PR(\infty)}$ is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of $\mathrm{PR}(\infty)$ in $(\beta,z,s)$ variables, and that identification is not part of the mission. $V_{PR(M)}$ is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the $(\beta,z,s)$ relaxation) belongs to a sibling mission.

The optimal solution $\beta^*$ is a binder with the hypotheses $\|\beta^*\|_\infty\le M$ and $F(\beta^*)\le F(\beta)$ for every $\beta$ in the box. A formalization in which $\beta^*$ is an arbitrary feasible point, or in which $V_{B(M)}$ or $V_{PR(\infty)}$ is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no $O(\cdot)$ in this result, so no constant is instantiated.

Needed infrastructure is light: continuity of $H$ and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming (2022). https://arxiv.org/abs/2004.06152
• H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 1517–1537, 2020. https://doi.org/10.1287/opre.2019.1919
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv e-prints, 2015 (the paper's reference [21], source of (6) for $\mathrm{PR}(\infty)$). https://arxiv.org/abs/1510.06083