Convex Optimization

Motivation

First-order methods (gradient descent, Nesterov's accelerated method, the Heavy-ball method) are the workhorses of large-scale convex optimization, and their worst-case convergence rates on smooth strongly convex functions are classical objects of study. Lessard, Recht and Packard (arXiv:1408.3595v7, SIAM J. Optim. 26(1), 2016, doi:10.1137/15M1009597) recast a first-order method as a linear dynamical system in feedback with the gradient map, and replace the unknown gradient by integral quadratic constraints (IQCs): quadratic inequalities that every gradient of a function in a given class must satisfy along every input sequence. Any rate certified this way holds for the whole function class, and finding the certificate is a small semidefinite program.

The analysis is only as good as the IQCs it is fed. The constraints in Section 3.3 of the paper are what turn the general framework into statements about convex optimization. The weighted off-by-one IQC (Lemma 10) is the one the paper uses for its rate results for the Gradient method, Nesterov's method and the Heavy-ball method on strongly convex functions (Sections 4–5).

Timeline. IQCs were introduced for robust control in continuous time by Megretski and Rantzer (IEEE TAC 42(6), 1997, doi:10.1109/9.587335); the multipliers behind Lemma 9 go back to Zames and Falb (SIAM J. Control 6(1), 1968, doi:10.1137/0306007). Lessard, Recht and Packard (arXiv 2014, journal 2016) adapted the framework to discrete-time optimization algorithms, with exponentially weighted ("ρ-hard") constraints to certify linear rates.

Setting

Write $\langle\cdot,\cdot\rangle$ and $\|\cdot\|$ for the Euclidean inner product and norm on $\mathbb R^d$. For $0<m<L$, the class $S(m,L)$ consists of the functions $f:\mathbb R^d\to\mathbb R$ that are continuously differentiable, strongly convex with parameter $m$,

$$f(ax+by)\le af(x)+bf(y)-\tfrac m2\,ab\,\|x-y\|^2\qquad(a,b\ge0,\ a+b=1),$$

and have an $L$-Lipschitz gradient, $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$.

The gradient acts on sequences: for an input sequence $y=(y_0,y_1,\dots)$ in $\mathbb R^d$ the output is $u_k=\nabla f(y_k)$. A reference is a pair $(y_\star,u_\star)$ with $u_\star=\nabla f(y_\star)$; it need not be a minimizer. The shifted signals are

$$\tilde y_k:=y_k-y_\star,\qquad \tilde u_k:=u_k-u_\star .$$

Two scalar quantities recur: the sector term and the off-by-one term

$$s_t:=(\tilde u_t-m\tilde y_t)^{\mathsf T}(L\tilde y_t-\tilde u_t),\qquad p_t:=(\tilde u_t-m\tilde y_t)^{\mathsf T}\big(L(\tilde y_t-\tilde y_{t-1})-(\tilde u_t-\tilde u_{t-1})\big).$$

Given a rate $\rho\in(0,1]$, a constraint is $\rho$-hard when its partial sums, weighted by $\rho^{-2t}$, are nonnegative for every $k$.

Formalization targets

Goal: Lemma 10 (weighted off-by-one IQC, p. 16)

For $f\in S(m,L)$, every reference $u_\star=\nabla f(y_\star)$, every $0\le\bar\rho\le\rho\le1$ with $\rho>0$, every sequence $y$ and every $k\ge0$,

$$(\tilde u_0-m\tilde y_0)^{\mathsf T}(L\tilde y_0-\tilde u_0)+\sum_{t=1}^{k}\rho^{-2t}(\tilde u_t-m\tilde y_t)^{\mathsf T}\big(L(\tilde y_t-\bar\rho^2\tilde y_{t-1})-(\tilde u_t-\bar\rho^2\tilde u_{t-1})\big)\ \ge\ 0. \tag{3.20}$$

Milestones

1. (3.13c), Proposition 5: $f(y)\ge f(x)+\nabla f(x)^{\mathsf T}(y-x)+\frac1{2L}\|\nabla f(y)-\nabla f(x)\|^2$ for convex $f$ with $L$-Lipschitz gradient.
2. (3.13d), Proposition 5: the sector inequality $-2mL\|y-x\|^2+2(L+m)(y-x)^{\mathsf T}(\nabla f(y)-\nabla f(x))-2\|\nabla f(y)-\nabla f(x)\|^2\ge0$.
3. Lemma 6 (sector IQC), (3.14).
4. (3.16): $q_k:=(L-m)g(y_k)-\tfrac12\|\nabla g(y_k)\|^2\ge0$ with $g(x)=f(x)-f(y_\star)-\frac m2\|x-y_\star\|^2$.
5. (3.17): $s_k\ge q_k$.
6. (3.18): $p_t\ge q_t-q_{t-1}$.
7. Lemma 8 (off-by-one IQC), (3.15): $s_0+\sum_{t=1}^k p_t\ge0$.
8. Remark after Theorem 4, item 3: a $\rho_1$-hard constraint is $\rho$-hard for every $\rho\ge\rho_1$.
9. The general-term identity in the proof of Lemma 10: the $t$-th term of (3.20) equals $(1-\bar\rho^2)s_t+\bar\rho^2p_t\ge q_t-\bar\rho^2q_{t-1}$.

Further items

Lemma 9 (Zames–Falb IQC, (3.19)), which contains Lemma 8 as the multiplier $h=(1,0,0,\dots)$, and the rate claim of Section 4.4: gradient descent with step $\alpha>0$ on $f\in S(m,L)$ satisfies $\|\xi_k-\xi_\star\|\le\max\{|1-\alpha m|,|1-\alpha L|\}^k\|\xi_0-\xi_\star\|$.

The goal leaves $\bar\rho$ free in $[0,\rho]$: $\bar\rho=\rho=1$ gives Lemma 8 and $\bar\rho=0$ a weighted sector constraint, so the goal contains both earlier IQCs.

Significance

The result. Lemma 10 is the constraint that, combined with the paper's main theorem (Theorem 4), yields the certified linear rates for first-order methods on $S(m,L)$, including the numerically computed rates for Nesterov's method in Section 4.5 and the robustness analyses of Section 5. The sector IQC alone is too weak for accelerated methods; the off-by-one term carries the extra information about convexity (not just about the gradient's sector) that makes tight certificates possible. The parameter $\bar\rho$ is an additional degree of freedom in the semidefinite program (Remark 11).

Formalizing it. The lemmas are proved on the page, and no machine-checked version is known to exist. A formal proof supplies the reusable inequality layer for IQC-based algorithm analysis: co-coercivity for convex functions with Lipschitz gradient, the sector inequality, and the telescoping bounds (3.16)–(3.18). It also settles a gap in the printed proof: the proof of Lemma 8 uses $g(x)\ge g(y_\star)=0$ and $\nabla g(y_\star)=0$, which hold only when $\nabla f(y_\star)=0$, while Lemmas 8 and 10 are stated for every reference. The lemmas remain true for every reference, and the goal is stated in that generality.

Difficulty

The proofs are short but not routine to formalize. Co-coercivity (3.13c) for a convex function with Lipschitz gradient needs a descent lemma and a minimization argument over an auxiliary function; Mathlib has the ingredients but not the statement. The auxiliary function $g$ must be shown convex with $(L-m)$-Lipschitz gradient, which is not a consequence of the Lipschitz bound on $\nabla f$ by the triangle inequality alone. The printed proof of Lemma 8 needs $\nabla f(y_\star)=0$, so the general-reference statements need an argument the page does not give. Finally, the passage from $\bar\rho$-hardness to $\rho$-hardness reweights partial sums whose individual terms may be negative, and at $\bar\rho=0$ the weights $\bar\rho^{-2t}$ used on the page are undefined.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), so norms are 2-norms; gradients are Mathlib's gradient. $S(m,L)$ is the structure InSmL f m L with fields $0<m$, $m<L$, ContDiff ℝ 1 f, StrongConvexOn Set.univ m f, and the Lipschitz bound on gradient f.
• The output sequence is always $u_k=\nabla f(y_k)$ for the given $f$; the gradient is never a free map. A formalization with a free map $u$ satisfying only the sector inequality would make Lemma 6 a tautology, and is ruled out.
• Sequences are arbitrary maps $\mathbb N\to\mathbb R^d$ (the page writes $\ell_2^d$; every statement holds for all sequences). Sums $\sum_{t=1}^k$ are indexed by $t+1$ over $t<k$ to avoid natural-number subtraction.
• Weights $\rho^{-2t}$ are written $(\rho^{2t})^{-1}$, and $\rho>0$ is assumed (the page prints $0\le\rho$, where the weight is undefined).
• Block quadratic forms are expanded: $[v;w]^{\mathsf T}[[aI,bI],[bI,cI]][v;w]=a\|v\|^2+2b\langle v,w\rangle+c\|w\|^2$.
• Milestones (3.16), (3.17), (3.18), the general-term display and Lemma 9 assume $\nabla f(y_\star)=0$, as their proofs on the page do; (3.16) is false without it. The goal, Lemma 6 and Lemma 8 do not.
• (3.13c) is stated for convex $f$ with $L$-Lipschitz gradient (the case $m=0$ that the proof of Lemma 8 applies to $g$), which contains the page's version for $f\in S(m,L)$.
• The IQC factorizations $(\Psi,M)$ of Lemmas 6–10 are not formalized; the targets are the lemmas' "corresponding quadratic inequalities", which are what the paper's main theorem consumes.

Proofs of any milestone are welcome independently; (3.13c) and the Abel-summation remark are reusable beyond this mission.

Selected references

• L. Lessard, B. Recht, A. Packard, Analysis and Design of Optimization Algorithms via Integral Quadratic Constraints, SIAM J. Optim. 26(1):57–95, 2016; cited from arXiv:1408.3595v7. https://arxiv.org/abs/1408.3595
• A. Megretski, A. Rantzer, System analysis via integral quadratic constraints, IEEE Trans. Automat. Control 42(6):819–830, 1997. https://doi.org/10.1109/9.587335
• G. Zames, P. L. Falb, Stability conditions for systems with monotone and slope-restricted nonlinearities, SIAM J. Control 6(1):89–108, 1968. https://doi.org/10.1137/0306007
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Polynomial optimization problems invariant under permutation of the variables appear throughout global optimization, and their semidefinite (SDP) relaxations, the moment–sum-of-squares hierarchy of Lasserre (2001), grow quickly with the number of variables $n$. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486v3, Math. Oper. Res. 2013) show how symmetry reduces the size of these relaxations. Their last section treats a model family in which the reduction is extreme: minimizing one power sum subject to fixed values of the lower power sums.

For this family the paper gives two bounds. A lower bound (Theorem 6.6, the subject of a companion mission) comes from an SDP over an $n \times n$ Hankel matrix. The present mission concerns the complementary upper bound, Theorem 6.7, which comes from an SDP in a single real variable whose matrix has size $m$, the number of constraints plus one, independently of $n$. The idea behind it, that candidate optima have at most $m$ non-zero coordinates, is the same phenomenon studied in the degree principle for symmetric polynomials of Timofte (2003) and Riener (2012).

Setting

Fix $n, m, q \in \mathbb{N}$ and real numbers $\gamma_1, \dots, \gamma_{m-1}$. For $x \in \mathbb{R}^n$ write $s_j(x) = \sum_{i=1}^n x_i^j$ for the power sum of order $j$. Problem (6.4) is

$$\mathrm{P}_{nmq}: \quad \min \sum_{i=1}^n x_i^q \quad \text{s.t.} \quad \sum_{i=1}^n x_i^j = \gamma_j, \quad j = 1, \dots, m-1,$$

with standing assumptions $q \ge m$ and $m \le n + 1$, and optimal value $\min \mathrm{P}_{nmq}$ (an infimum, possibly $+\infty$ if the constraints are inconsistent, or $-\infty$).

For a sequence $s = (s_0, s_1, \dots)$ the Hankel matrix of order $k$ is $H_k(s) = (s_{i+j-2})_{1 \le i,j \le k}$. For a monic real polynomial

$$p = X^m + \sum_{j=0}^{m-1} p_j X^j$$

with complex roots $x_1, \dots, x_m$ (with multiplicity), the Newton sums are $s_k = \sum_{j=1}^m x_j^k$, so $s_0 = m$. Newton's identities express the $s_k$ through the coefficients and back; in particular $s_1, \dots, s_{m-1}$ determine $p_{m-1}, \dots, p_1$, so that, once $s_j = \gamma_j$ for $j < m$ is imposed, the only free coefficient is $p_0$, and every later Newton sum is a known polynomial $s_j = Q_j(p_0)$, $j \ge m$. For $q \le 2m - 2$ the paper defines

$$\mathrm{U}_{nmq} = \min_{p_0} \{\, Q_q(p_0) : H_m(s) \succeq 0 \,\}, \tag{6.7}$$

where $s_0 = m$, $s_j = \gamma_j$ for $1 \le j \le m-1$, and $s_j = Q_j(p_0)$ for $m \le j \le 2m-2$. The constraint $H_m(s) \succeq 0$ is equivalent to the real-rootedness of $p$ (Hermite's criterion).

Formalization targets

Goal: Theorem 6.7

For $m \le n$ and $m \le q \le 2m-2$,

$$\min \mathrm{P}_{nmq} \le \mathrm{U}_{nmq},$$

and if $\mathrm{P}_{nmq}$ has an optimal solution $x^* \in \mathbb{R}^n$ with at most $m$ non-zero entries, then

$$\min \mathrm{P}_{nmq} = \mathrm{U}_{nmq}.$$

Both halves are part of the goal; the equality is what makes (6.7) an exact convex reformulation of (6.4) in the sparse case.

Milestones

In attack order:

1. Newton's identities for a monic polynomial of degree $m$, in the two forms printed on p. 27 ($k \ge m$ and $1 \le k < m$).
2. Given $s_1, \dots, s_{m-1}$ and $p_0$, there is exactly one monic polynomial of degree $m$ with those Newton sums and constant coefficient $p_0$.
3. $Q_j$ is affine in $p_0$ whenever $m \le j \le 2m-1$.
4. Hermite's criterion: all roots of $p$ are real if and only if $H_m(s) \succeq 0$.
5. From the proof of Theorem 6.7: if $p$ is feasible for (6.7) and real-rooted, its roots padded with zeros form a feasible point of $\mathrm{P}_{nmq}$ with objective $s_q$.

Significance

The result. Theorem 6.7 bounds a nonconvex polynomial optimization problem in $n$ variables from above by a semidefinite program in one variable with an $m \times m$ matrix. Combined with Theorem 6.6 it brackets $\min \mathrm{P}_{nmq}$ between two SDP values, and when an $m$-sparse optimum exists, it identifies the optimal value exactly by a problem whose size does not grow with $n$. The milestones are classical facts about univariate polynomials (Newton's identities, Hermite's criterion) that are used far beyond this paper, in real algebraic geometry, the theory of hyperbolic and real-rooted polynomials, and moment problems.

Formalizing it. The inequality has a short printed proof; the equality case has none, so the formalization supplies a complete argument for a stated but unproved claim. Hermite's real-root criterion is, as far as the platform's library search shows, not available in Mathlib, and a formal proof of it is a reusable contribution in its own right. Newton's identities exist in Mathlib for multivariate symmetric polynomials; their form for the coefficients and roots of a monic univariate polynomial, as printed here, is a separate statement. No part of Theorem 6.7 is known to have a machine-checked proof.

Difficulty

The obvious argument for the inequality, sending a feasible $p_0$ to the vector of roots of $p$, needs the roots to be real, and real-rootedness is encoded only through positive semidefiniteness of a Hankel matrix of Newton sums. The step "psd Hankel matrix implies real roots" is Hermite's criterion, a nontrivial classical theorem with no library support. The equality half needs the converse direction of the same criterion together with a construction that the text does not give. Finally, the printed proof starts from "an optimal solution $p_0$ of the SDP (6.7)", which need not exist; the formal statement is about infima and must be proved without assuming attainment.

Formalization scope

Points are Fin n → ℝ; $\gamma$ is a sequence ℕ → ℝ of which only $\gamma_1, \dots, \gamma_{m-1}$ are read. Both $\min \mathrm{P}_{nmq}$ and $\mathrm{U}_{nmq}$ are infima in EReal over their feasible sets, so an infeasible problem has value $+\infty$ and no optimizer is assumed. The Hankel matrix is indexed from $0$: entry $(i,j)$ is $s_{i+j}$, $0 \le i, j < k$, which is the paper's $(s_{i+j-2})_{1 \le i,j \le k}$. Newton sums of a real polynomial are the real part of $\sum_z z^k$ over its complex roots with multiplicity (Polynomial.aroots), which is real for real polynomials.

The feasible set of (6.7) is parametrized by the monic polynomial $p$ itself rather than by $p_0$: $p$ monic of degree $m$, $s_j(p) = \gamma_j$ for $1 \le j \le m-1$, and $H_m(s(p)) \succeq 0$. Milestone 2 shows that this is a bijective change of coordinates $p \leftrightarrow p_0$, and $s_j(p)$ for $j \ge m$ is the paper's $Q_j(p_0)$ by definition. The hypothesis $m \le q$ in the goal is the standing assumption $q \ge m$ of (6.4); with $q \le 2m-2$ it forces $m \ge 2$. In milestone 5, $q \ge 1$ is needed because the padding zeros contribute $0^q$.

Several formalizations would trivialize or falsify the targets and are ruled out: values are never real infima (which are $0$ on empty or unbounded sets); $\mathrm{U}_{nmq}$ is defined by (6.7) with $s_m, \dots, s_{2m-2}$ tied to $p_0$, not by the relaxation (6.6) in which those entries are free and which can have a strictly smaller value; and the equality half is stated in full, not weakened to an inequality.

The needed infrastructure is Vieta's formulas and Newton's identities over Polynomial, Hermite's quadratic form and its signature, and the passage between root multisets and coordinate vectors. All of it is reusable outside this mission; contributions of Hermite's criterion in particular are welcome.

Selected references

• C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013. arXiv:1103.0486v3 (the version formalized here): https://arxiv.org/abs/1103.0486, DOI: https://doi.org/10.1287/moor.1120.0558
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3):796–817, 2001. https://doi.org/10.1137/S1052623400366802
• V. Timofte, On the positivity of symmetric polynomial functions. Part I: General results, J. Math. Anal. Appl. 284(1):174–190, 2003. https://doi.org/10.1016/S0022-247X(03)00301-9
• C. Riener, On the degree and half-degree principle for symmetric polynomials, J. Pure Appl. Algebra 216(4):850–856, 2012. https://doi.org/10.1016/j.jpaa.2011.08.012
• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, 2nd ed., Springer, 2006 (Hermite's quadratic form). https://doi.org/10.1007/3-540-33099-2

Motivation

The Heavy-ball method of Polyak, $x_{k+1}=x_k-\alpha\nabla f(x_k)+\beta(x_k-x_{k-1})$, adds a momentum term to gradient descent. On strongly convex quadratics with curvature between $m$ and $L$, a classical eigenvalue analysis gives the step size and momentum that minimise the worst-case linear rate, $\alpha=4/(\sqrt L+\sqrt m)^2$ and $\beta=\bigl((\sqrt\kappa-1)/(\sqrt\kappa+1)\bigr)^2$ with $\kappa=L/m$, and the resulting rate $(\sqrt\kappa-1)/(\sqrt\kappa+1)$ matches the lower bound for first-order methods. Practitioners and theorists alike have long asked whether this tuning carries over from quadratics to all smooth strongly convex functions.

Lessard, Recht and Packard (SIAM J. Optim. 2016) built a framework, based on integral quadratic constraints (IQCs) from robust control, that certifies convergence rates of first-order methods by solving small semidefinite programs. Applied to the Heavy-ball method, the certificates degrade sharply once $L/m$ exceeds about 18. Section 4.6 of the paper shows that this is not a weakness of the certificates: the method itself fails. It exhibits a one-dimensional function $f$ with $m=1$, $L=25$ on which the Heavy-ball method with the quadratic-optimal tuning settles into a cycle of period 3 instead of converging to the minimiser. Appendix B proves this for the initial point $x_0=3.3$.

The example is a standard reference point for why momentum methods need an analysis beyond quadratics.

Setting

For $0<m<L$, the class $S(m,L)$ consists of the continuously differentiable functions $f:\mathbb R^d\to\mathbb R$ that are strongly convex with parameter $m$ and whose gradient is Lipschitz with constant $L$. Here $d=1$.

The counterexample is the function (unique up to an additive constant) with the piecewise-linear derivative (4.11):

$$\nabla f(x)=\begin{cases}25x & x<1,\\ x+24 & 1\le x<2,\\ 25x-24 & x\ge 2.\end{cases}$$

Its minimiser is $x=0$.

The Heavy-ball run with step size $\alpha$, momentum $\beta$ and starting point $x_0$ is the sequence $x_0,x_1,x_2,\dots$ with $x_{k+1}=x_k-\alpha\nabla f(x_k)+\beta(x_k-x_{k-1})$ and the initialization $x_{-1}=x_0$, so $x_1=x_0-\alpha\nabla f(x_0)$. With $L=25$, $m=1$ the tuning of Proposition 1 gives $\alpha=1/9$, $\beta=4/9$, and the run satisfies (B.1): $x_{k+1}=\tfrac{13}9x_k-\tfrac49x_{k-1}-\tfrac19\nabla f(x_k)$.

The limit cycle (B.3) is $p=792/1225$, $q=-2208/1225$, $r=2592/1225$; the sequence $x^\star_k$ cycles through $p,q,r$. The perturbation of a sequence is $\varepsilon_k=x_k-x^\star_k$; the matrix $P=\begin{bmatrix}-4/3&-4/9\\1&0\end{bmatrix}$ governs it near the cycle; and $\bar\varepsilon=r-2=142/1225$ is the distance from the cycle to the nearest transition point of $\nabla f$.

In Lean everything lives in the namespace IQCAlg.HeavyBall: gradF is (4.11), hbRun g α β x0 the Heavy-ball run, hbAlpha L m, hbBeta L m the tuning, cyc the cycle, eps x k the perturbation, Pm the matrix $P$, epsBar the margin $\bar\varepsilon$, and InSmL1 f m L the class $S(m,L)$ on $\mathbb R$.

Formalization targets

Goal: attraction to the 3-cycle from $x_0=3.3$

With $x$ the Heavy-ball run on (4.11) with Proposition 1's tuning for $L=25$, $m=1$, from $x_0=3.3$:

$$x_{3n}\to\frac{792}{1225},\qquad x_{3n+1}\to-\frac{2208}{1225},\qquad x_{3n+2}\to\frac{2592}{1225}\qquad(n\to\infty).$$

In particular the iterates do not converge to the minimiser $0$.

Milestones, in the order of the proof of Appendix B

1. (4.11) defines an $f\in S(1,25)$ (p. 23).
2. The tuning reduces to $\alpha=1/9$, $\beta=4/9$; $(p,q,r)$ is the unique solution of the linear system of p. 39, and the period-3 sequence $p,q,r,\dots$ satisfies (B.1) (pp. 39–40).
3. On the cycle's linear pieces, $(\varepsilon_{k+2},\varepsilon_{k+1})=P(\varepsilon_{k+1},\varepsilon_k)$ (p. 40).
4. $\rho(P)=2/3$ (p. 40).
5. $\|P^8\|^2<1/2$ in the induced 2-norm (p. 40).
6. (B.4): $\varepsilon_{k+8}^2<\tfrac12(\varepsilon_{k+1}^2+\varepsilon_k^2)$ while the iterates stay on the cycle's pieces (p. 40).
7. Eight consecutive $\varepsilon^2<\bar\varepsilon^2$ keep the whole tail below $\bar\varepsilon^2$ (p. 40).
8. From $x_0=3.3$, $|x_j-x^\star_j|<\bar\varepsilon$ for $j=4,\dots,11$ (p. 40).

Significance

The result itself. The goal shows that tuning a momentum method on quadratics does not transfer to the class $S(m,L)$ it is usually advertised for: a function with condition ratio 25 defeats the Heavy-ball method (the paper reports a cycle for $3.07\le x_0\le3.46$ numerically; only $x_0=3.3$ is proved). It explains the failure of IQC certificates for Heavy-ball at large $L/m$ and separates Heavy-ball from Nesterov's method, whose accelerated rate holds on all of $S(m,L)$.

Formalizing it. The paper's proof is complete but terse: the linear system, eleven exact rational iterates, a matrix-power norm bound and an induction keeping all later iterates on the right linear pieces are all left to "one can easily verify". A machine-checked version settles each of these and gives a reusable, fully explicit counterexample for momentum methods.

Difficulty

Every step is elementary, and the difficulty is in making the global argument airtight. The naive argument, that $\rho(P)=2/3<1$ forces perturbations to decay, does not suffice: a perturbation can grow transiently, push an iterate across a transition point $1$ or $2$ of $\nabla f$, and then the linear recursion no longer applies. The proof replaces the spectral radius by the induced norm of $P^8$, which requires a bound on the largest singular value of an explicit $2\times2$ matrix with entries over $3^{16}$, and combines it with an induction over blocks of eight indices whose invariant is that the iterates stay on the cycle's pieces. The remaining work is exact rational arithmetic on eleven iterates of a piecewise-defined recursion.

Formalization scope

All objects are on $\mathbb R$; no measure theory or probability is involved. The conventions:

• $S(m,L)$ is stated for $f:\mathbb R\to\mathbb R$ with Mathlib's StrongConvexOn, ContDiff ℝ 1 and an $L$-Lipschitz deriv f; this is the paper's class in dimension one.
• The run is indexed from $x_0$; the page's initialization $x_{-1}=x_0$ is built in as $x_1=x_0-\alpha\nabla f(x_0)$.
• The tuning is written as in Proposition 1 with Real.sqrt, not replaced by $1/9$ and $4/9$, so the goal is explicitly about the quadratic-optimal tuning; milestone 2 reduces it.
• The norm in milestone 5 is Mathlib's $\ell^2$ operator norm on matrices (Matrix.Norms.L2Operator), the page's induced 2-norm.
• The spectral radius in milestone 4 is taken over the complex spectrum.
• (B.4) carries the added hypothesis $(\varepsilon_{k+1},\varepsilon_k)\ne(0,0)$, without which its strict inequality reads $0<0$; its same-piece hypotheses are at indices $k+1,\dots,k+7$, the ones its outer inequality needs.

The goal has no hypotheses: it is a statement about one explicit sequence, so it cannot hold vacuously, and it pins the three limits exactly, which rules out a formalization that only asserts non-convergence or the existence of some cycle. The fixed starting point $33/10$ is exact; floating point never enters.

Contributions are welcome at every milestone. The matrix-norm bound and the exact-arithmetic computation of iterates are independent of each other and of the induction, and can be attacked in parallel. A general lemma converting an eight-step contraction into convergence of a perturbed linear recursion would be reusable beyond this mission.

Selected references

• L. Lessard, B. Recht, A. Packard, Analysis and Design of Optimization Algorithms via Integral Quadratic Constraints, SIAM J. Optim. 26(1):57–95, 2016; read as arXiv:1408.3595v7. https://arxiv.org/abs/1408.3595 — Section 4.6 and Appendix B.
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4(5):1–17, 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• A. Megretski, A. Rantzer, System analysis via integral quadratic constraints, IEEE Trans. Automat. Control 42(6):819–830, 1997. https://doi.org/10.1109/9.587335

Motivation

Many polynomial optimization problems are invariant under permuting the variables: the objective and the constraints are symmetric polynomials. Lasserre's moment–sum-of-squares hierarchy solves such problems by a sequence of semidefinite programs whose size grows quickly with the number of variables and the degree, and symmetry is the main tool for shrinking them. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 38(1), 2013, doi:10.1287/moor.1120.0558) develop symmetry reductions of the hierarchy and, in their Section 6, a second route: instead of reducing the moment matrices, describe the orbit space of the symmetry group directly by polynomial inequalities, following Procesi and Schwarz, and optimize over it.

For the symmetric group the orbit space is described by a single Hankel matrix of power sums. This mission formalizes the lower bound that results for a basic family of symmetric problems: minimize one power sum subject to prescribed values of the lower power sums.

Setting

Fix $n \in \mathbb N$ and a point $x = (x_1,\dots,x_n) \in \mathbb R^n$. The power sum of order $j$ is $s_j(x) = \sum_{i=1}^n x_i^{\,j}$; note $s_0(x) = n$.

The problem $\mathrm P_{nmq}$ (6.4). Given $m, q \in \mathbb N$ with $q \ge m$, $m \le n+1$, and prescribed reals $\gamma_1,\dots,\gamma_{m-1}$, minimize $s_q(x)$ over all $x \in \mathbb R^n$ with $s_j(x) = \gamma_j$ for $j = 1,\dots,m-1$. Its optimal value is written $\min \mathrm P_{nmq}$.

The Hankel matrix. For a real sequence $s = (s_0, s_1, \dots)$ and $k \in \mathbb N$, $H_k(s) = (s_{i+j-2})_{1\le i,j\le k}$.

The matrix $J$ (6.1). For a finite group acting on $\mathbb R^n$ with fundamental invariants $\pi_1,\dots,\pi_l$, the matrix $J = (\langle d\pi_i, d\pi_j\rangle)_{1\le i,j\le l}$ has $G$-invariant entries $\sum_k \partial_k\pi_i\,\partial_k\pi_j$. For the symmetric group with $\pi_j = s_j/j$, $J$ is the Hankel matrix $H_n(s)$ of power sums.

The SDP (6.5). For $m \le n+1$ and $m \le q \le 2n-2$,

$$\mathrm L_{nmq} = \min_s \{\, s_q \;:\; H_n(s) \succeq 0,\ s_0 = n,\ s_j = \gamma_j,\ j = 1,\dots,m-1 \,\}.$$

The variable is the sequence $s$; the constraint is a single linear matrix inequality of size $n$.

Formalization targets

Goal: Theorem 6.6

For $m \le n+1$ and $m \le q \le 2n-2$:

(a)

$$\min \mathrm P_{nmq} \ge \mathrm L_{nmq}.$$

(b) If $q = m = 2r$, put $\gamma_0 = n$, $H_r(\gamma) = (\gamma_{i+j-2})_{1\le i,j\le r}$ and $u_r(\gamma)^T = (\gamma_r,\dots,\gamma_{2r-1})$. If $H_r(\gamma) \succ 0$, then

$$\min \mathrm P_{nmq} \ge u_r(\gamma)^T H_r(\gamma)^{-1} u_r(\gamma).$$

The goal is the conjunction of (a) and (b).

Milestones

1. For $\pi_j = s_j / j$, $J = H_n(s)$ (p. 26).
2. The power-sum vector of a feasible point of (6.4) is feasible for (6.5) (proof of (a), p. 26).
3. $H_n(s) \succeq 0 \Rightarrow H_{r+1}(s) \succeq 0$ for $r < n$ (proof of (b), p. 26).
4. The Schur complement bound $u^T H_r(s)^{-1} u \le s_{2r}$ when $H_{r+1}(s) \succeq 0$ and $H_r(s) \succ 0$ (proof of (b), p. 26).

Significance

Part (a) bounds a nonconvex polynomial problem of degree $q$ in $n$ variables by a semidefinite program with one $n\times n$ matrix variable, whose size does not depend on $q$. Part (b) evaluates the bound in closed form in the even case $q = m$, where the SDP reduces to a single scalar constraint on the free moment $s_{2r}$. Together with the upper bound of Theorem 6.7 (a separate mission of this series), it brackets the optimal value of power-sum problems, which appear in moment problems, in the analysis of symmetric inequalities, and as test cases for symmetry-adapted relaxations.

The paper's proof is a few lines, citing the Procesi–Schwarz theorem and Schur's complement. A formal development makes each step explicit: the positive semidefiniteness of the Hankel matrix of power sums of a real point, the principal-submatrix argument, and the Schur complement for a Hankel block. It also fixes a misprint: the bound of (b) is printed as $u_r(\gamma)^T H_r(\gamma)\, u_r(\gamma)$ without the inverse, which is false (for $n = 2$, $m = q = 2$, $\gamma_1 = 1$ the minimum is $1/2$ but the printed bound is $2$). No machine-checked version of this result is known to exist.

Difficulty

The individual steps are classical, and the difficulty is in the bookkeeping. The paper reaches (a) through the Procesi–Schwarz description of the orbit space, a deep result stated for general finite groups; the formal route needs only the positive semidefiniteness of the Hankel matrix of power sums of every real point, which the page leaves implicit. The identity $J = H_n(s)$ requires computing partial derivatives of power sums with the right index shifts. In (b), $H_{r+1}(s)$ must be identified with a $2\times 2$ block matrix whose top-left block is $H_r(\gamma)$ with $\gamma_0 = n$, which needs the prescribed values $\gamma_1,\dots,\gamma_{2r-1}$ and a reindexing of $\{0,\dots,r\}$ as $\{0,\dots,r-1\}\sqcup\{r\}$. The extended-real values must be handled: the problem can be infeasible (value $+\infty$), and for odd $q$ unbounded below.

Formalization scope

Lean namespace SymPolyOpt.PowerSumLB. Conventions:

• A point is x : Fin n → ℝ; $s_j(x)$ is powerSum x j, so powerSum x 0 = n.
• $\gamma \in \mathbb R^{m-1}$ is a sequence γ : ℕ → ℝ of which only $\gamma_1,\dots,\gamma_{m-1}$ are read. The page's "$=\gamma_k$" in (6.4) is read as $\gamma_j$.
• $\min \mathrm P_{nmq}$ and $\mathrm L_{nmq}$ are infima in EReal: $+\infty$ for an infeasible problem, possibly $-\infty$. They are compared only by ≤.
• The SDP variable is a sequence s : ℕ → ℝ; its entries past $s_{2n-2}$ are unconstrained and irrelevant since $q \le 2n-2$.
• $H_k(s)$ is 0-indexed, $H_k(s)_{ij} = s_{i+j}$ for $0 \le i,j < k$, the same matrix as the page's.
• $J$ is formed with the product of partial derivatives as the pairing of (6.1), using Mathlib's MvPolynomial.psum and pderiv.
• $q \le 2n-2$ is natural-number subtraction; for $n \le 1$ it forces $q = 0$.

Disclosed changes relative to the page:

• Theorem 6.6(b) is stated with $H_r(\gamma)^{-1}$, as the paper's proof gives; the printed form without the inverse is false.
• $H_r(\gamma) \succ 0$ is added to (b) and to the Schur milestone, so that the inverse exists.

Trivializing formalizations are ruled out: real-valued infima (which return $0$ on empty or unbounded sets) are not used; $\mathrm L_{nmq}$ is an SDP over arbitrary sequences, not over power-sum vectors of points, so (a) is not definitional; the constraint $s_0 = n$ is kept; Lean's junk inverse of a singular matrix is excluded by the positive-definiteness hypothesis; and the printed false bound is not stated.

Needed infrastructure: Mathlib's Matrix.PosSemidef, Matrix.PosDef, PosSemidef.submatrix and the Schur-complement lemmas for block matrices (fromBlocks). A reusable lemma that Hankel matrices of power sums (and, more generally, of moments of a finitely supported measure) are positive semidefinite would serve other moment-problem missions. Contributions to any milestone are welcome.

Selected references

• C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013. arXiv:1103.0486v3, doi:10.1287/moor.1120.0558
• C. Procesi, G. Schwarz, Inequalities defining orbit spaces, Invent. Math. 81:539–554, 1985. doi:10.1007/BF01388587
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3):796–817, 2001. doi:10.1137/S1052623400366802

Motivation

An online learner repeatedly chooses a point, observes a loss, and is judged by the difference between its accumulated loss and that of a fixed competitor. In practice, an available learner may operate on a broad feasible set $W$, while the application permits decisions only in a smaller set $V$. Replacing each output by a feasible point changes the learner's losses, so its existing regret guarantee no longer directly applies. Chapter 12 of Orabona's text develops reductions that use the learner as a black box: they change the feedback sent to it and recover a guarantee for the constrained predictions.

The chapter treats Euclidean and other norms, Bregman projections, sleeping experts, and the separation of magnitude from direction. This mission focuses on its first general construction, Theorem 12.5. It is useful when the internal update of the learner is unavailable or when a solver wants to reuse one unconstrained algorithm across several constraint sets. The theorem gives four explicit surrogate losses and an explicit bound on their subgradient norms. Orabona, Chapter 12 also explains how its distance based construction relates to regret matching on the simplex.

Setting

Work in a finite-dimensional real vector space $E$ with an arbitrary norm $\|\cdot\|$. Its continuous dual consists of real-valued linear functionals; $g(v)$ is the pairing and $\|g\|_*$ is the dual norm. Let $V\subseteq W\subseteq E$, with $V$ nonempty, closed, and convex. The distance to $V$ and the generalized projection are

$$d_V(z)=\min_{y\in V}\|z-y\|, \qquad \Pi_V(z)=\{x\in V:\|z-x\|=d_V(z)\}.$$

The minimum exists under these assumptions. A projection need not be unique for an arbitrary norm; the construction accepts any $x_t\in\Pi_V(z_t)$. In round $t$, an underlying learner outputs $z_t\in W$, the reduction predicts $x_t\in V$, and the environment reveals a real-valued loss $\ell_t$. Choose a subgradient $g_t$ of $\ell_t$ at $x_t$ that satisfies the subgradient inequality for competitors in $V$. Choose any full-space subgradient $q_t\in\partial d_V(z_t)$. For a fixed $u\in V$, the constrained regret is

$$\operatorname{Regret}_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

The surrogate losses are functions passed back to the learner. Their four formulas are the distance-penalized linear loss, its linear form using $q_t$, a distance penalty activated only when $g_t(x_t-z_t)>0$, and that activated penalty's linear form. Each is defined on the ambient space, then used on $W$. The projection rule and the selected subgradients are the only information the reduction needs from a run.

Formalization targets

Constrained regret from surrogate regret

For each of the four choices $k$ in Theorem 12.5 and every $u\in V$, the goal is

$$\operatorname{Regret}_T(u) \le \sum_{t=1}^{T}\bigl(\widetilde\ell_t^{(k)}(z_t) -\widetilde\ell_t^{(k)}(u)\bigr).$$

The theorem is pathwise: it applies to any sequence of predictions $z_t$ that the underlying learner could produce. No particular learner or regret rate is built into the target. Equation (12.2) isolates the linearized regret term that each surrogate must cover. The four clauses of Lemma 12.2 establish convexity, the exact Lipschitz constant, the zero subgradient on $V$, and the subdifferential characterization outside $V$.

Surrogate subgradient size

The companion clause of Theorem 12.5 says that every full-space subgradient $\widetilde g_t$ of a surrogate at a point of $W$ satisfies

$$\|\widetilde g_t\|_*\le 2\|g_t\|_*.$$

The factor $2$ is part of the printed result. It applies to all four choices, including the branches at which the activation term vanishes.

Significance

The result transfers a regret guarantee from an algorithm working on $W$ to feasible decisions in $V$ through a loss transformation. The norm bound makes this transfer quantitative for algorithms whose guarantees depend on subgradient magnitudes: the new losses have controlled scale. Lemma 12.2 is reusable apart from online learning, because it describes distance and subgradients for a closed convex set in any finite-dimensional normed geometry.

Orabona presents these as established mathematical results in Theorem 12.5 and Lemma 12.2. The work here is to give them auditable Lean statements and, subsequently, machine-checked proofs. The chapter's Bregman projection, sleeping-experts, and magnitude/direction reductions are separate results; this proposal leaves them for later missions or additions. A proof of the present goal would make the first black-box reduction reusable without depending on a specific unconstrained learner's implementation.

Difficulty

Simply projecting $z_t$ into $V$ leaves an extra term in the linearized regret: the old learner was evaluated at $z_t$ while the actual loss was incurred at $x_t$. An arbitrary correction to the feedback can cover that term while destroying convexity or greatly enlarging gradients. The four formulas balance both requirements, and the two activated formulas must also handle the boundary case $x_t=z_t$, where a normalized direction would otherwise divide by zero. Generalized projections create another issue: an argument cannot silently assume one canonical nearest point when the norm is not Euclidean.

Formalization scope

Lean uses a finite-dimensional real normed space and represents dual vectors as continuous linear functionals. Their operator norm is the book's dual norm. The distance is Metric.infDist; nonemptiness keeps its value meaningful, and closedness plus finite dimensionality supplies an attained minimum. Projection is a relation, so all valid choices are covered. Sequences start at index $1$; index $0$ is unused, and the horizon is explicitly at least one. The original losses are real-valued on the ambient space, with the subgradient inequality required only for comparators in $V$. The distance and surrogate subgradients use the full-space inequality. This matters when $W$ has empty interior: a relative subgradient on $W$ can have an arbitrary normal component and would make the printed norm bound false.

The underlying algorithm is abstracted by its sequence $z_t\in W$; its surrogate regret is exactly the sum on the right of the goal. $W$ is allowed to be strictly larger than $V$, so the statement retains the constraint-reduction content. The normalized direction in the third and fourth surrogates appears only in the branch with $g_t(x_t-z_t)>0$, which implies $x_t\ne z_t$. Contributions toward the distance-function lemmas, the surrogate inequalities, and the gradient bound all support the goal. The same geometric definitions can also support later reductions based on other projections.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 12, pp. 192–205. arXiv

Motivation

An online classifier must predict a label before learning the correct answer. Its errors matter directly: a low numerical loss is useful only if it controls the number of wrong predictions. Chapter 8 of Orabona's textbook examines this connection for linear classification, where a vector of weights produces a score by taking an inner product with the incoming example. The Perceptron is a particularly spare example: it changes its weights only after a mistake, and it needs no learning rate or chosen comparator. This makes its guarantee a useful point of contact between classification mistakes and the convex losses used elsewhere in online optimization.

Theorem 8.2 compares the Perceptron's mistake count with a whole family of comparator losses, indexed by a real exponent $q\ge1$. The theorem is a known result in the book, not an unsolved conjecture. The mission concerns a faithful Lean statement and, subsequently, its machine-checked proof. The distinction matters because other Perceptron bounds on the platform address batch separability, multiclass prediction, or a hinge loss only on update rounds; those results do not state this theorem with its constants and quantifiers.

Setting

Fix a dimension $d$ and a sequence of feature vectors $z_t\in\mathbb R^d$ with binary labels $y_t\in\{-1,1\}$, for rounds $t=1,\ldots,T$. The Perceptron begins at $x_1=0$. At round $t$ it predicts $\widetilde y_t=\operatorname{sign}(\langle z_t,x_t\rangle)$, where $\operatorname{sign}(0)=0$. It records a mistake when $y_t\widetilde y_t\le0$ and, on exactly those rounds, adds $y_tz_t$ to its weights. Write $\tau_t=\mathbf 1\{y_t\widetilde y_t\le0\}$ and $M=\sum_{t=1}^T\tau_t$. A zero score is a mistake even though it is not a strict sign disagreement.

For a score $m\in\mathbb R$, a label $y\in\{-1,1\}$, and a real power $q\ge1$, the hinge-power loss is $\ell_q(m,y)=\max(1-ym,0)^q$. A fixed competitor $u\in\mathbb R^d$ has cumulative loss $L_q(u)=\sum_{t=1}^T\ell_q(\langle z_t,u\rangle,y_t)$. The loss is zero when $u$ gives every example the correct sign with margin at least one. The book assumes the input vectors obey $\|z_t\|_2\le R$; $R$ is a nonnegative radius. The sequence is arbitrary, so the result includes examples chosen with knowledge of earlier predictions.

Formalization targets

Perceptron mistake guarantee

The goal is Theorem 8.2, p. 144 of Orabona. For every $u\in\mathbb R^d$ and every real $q\ge1$,

$$M-L_q(u)\le\frac{q^2R^2\|u\|_2^2}{2} +qR\|u\|_2\sqrt{\frac{q^2R^2\|u\|_2^2}{4}+L_q(u)}.$$

All constants and the full family of powers are part of the target. For a competitor with $L_q(u)=0$, choosing $q=1$ yields the finite mistake bound $M\le R^2\|u\|_2^2$, as the book explains on p. 144. For a nonseparable sequence, the same statement measures mistakes relative to the competitor's nonzero loss.

Milestone statements

The milestone list follows the book's named ingredients: Lemma 4.29 converts an implicit square-root inequality into an explicit one; the constant-step clause of Theorem 2.13 gives the linear-loss gradient bound; and displays (8.4) and (8.5) relate the Perceptron updates to the comparator and to the hinge loss. Theorem 2.13 is stated in the linear, whole-space case used on p. 145. The printed (8.4) has an invalid extra term on its left; the milestone retains the printed text for provenance, while the Lean statement gives the valid comparator inequality used by (8.5). The correction is described in the item and moderation notes.

Significance

The guarantee answers a practical question about a simple online rule: how many classification errors can it make when a fixed linear predictor has small convex loss? The answer has explicit dependence on the feature radius, comparator norm, loss exponent, and comparator loss. It contains the separable margin case and also applies when no comparator classifies every example with margin one. The quantifier over all $u$ permits a later analyst to choose a competitor after seeing the sequence without changing the algorithm or the theorem.

A complete formalization would provide a reusable account of a deterministic online classifier, its exact zero-score convention, and the passage from update counts to a family of hinge losses. The local Lean declarations currently compile as statements with proof placeholders; compilation does not establish the mathematical inequalities. A proof of the goal and milestones remains to be supplied and checked. In particular, the correction to (8.4) should be made explicit in any downstream development so that later results never depend on the false printed left side.

Difficulty

The mistake count is discontinuous in the prediction score, while the competitor is measured by a smooth family of convex surrogates. A direct comparison of their per-round losses does not give the theorem's constants. The update rule also depends on its own current score, so its condition must be tied to the weight sequence generated by earlier rounds. Treating the update indicators as free variables, or counting only rounds with a strictly negative score, changes the statement.

The book's proof passes through an implicit inequality involving $\sqrt M$. That relation alone is weaker than the displayed goal until its constants and nonnegative domains are handled precisely. Real powers require special attention at a zero hinge value. The printed (8.4) introduces an additional difficulty: with $u=0$ and two one-dimensional examples $z_1=1$, $z_2=-1$ carrying positive labels, its left side is positive while its right side is zero. The valid comparator inequality has to be distinguished from that printed display.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$, its Euclidean inner product and norm, and sequences indexed by natural numbers with active rounds $1,\ldots,T$. Index zero carries no data requirement. A total recursive definition fixes $x_1=0$ and every later Perceptron update. Mathlib's Real.sign supplies $\operatorname{sign}(0)=0$; an indicator records both a wrong sign and a zero score. The comparator loss uses a maximum with zero before taking a real power. No probability space is needed because Algorithm 8.2 is deterministic.

The Lean theorems explicitly require binary labels on the active rounds, $q\ge1$ for the goal, $R\ge0$, and $\|z_t\|_2\le R$. They allow $T=0$, $d=0$, and $R=0$; the formulas remain meaningful in these cases. The set $X$ in the book's theorem is omitted because the assertion uses only the given feature sequence and its norm bound. The constant-step milestone requires $\eta>0$ because its formula divides by $\eta$. The definitions include a mistake count, hinge-power loss, cumulative comparator loss, and the fixed algorithm; the theorem layer can reuse Mathlib's inner-product and real-analysis results. Contributions toward these statements, the algebraic milestone, or the full theorem proof are in scope. A run that can skip a zero-score update or whose iterates are chosen independently of the recursion is outside this mission.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 8, pp. 141–146; Lemma 4.29, p. 45; Theorem 2.13, p. 13. arXiv PDF.

Why moving comparators matter

In online learning, a learner chooses a point before seeing each round's loss. Ordinary regret compares the learner with one fixed point chosen after all rounds. That comparison can be too coarse when a useful action changes over time. A portfolio allocation, a prediction rule, or an operating point may need to move after the environment shifts. Dynamic regret compares the learner with a specified sequence of feasible points, one for each round. The sequence is allowed to move, but its movement appears explicitly in the bound. Chapter 14 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization develops this comparison, then studies strongly adaptive and tracking regret. This mission isolates its first capstone, Theorem 14.2.

The result extends the book's earlier analysis of online mirror descent to changing comparators. As the chapter explains, a moving comparator can achieve a smaller cumulative loss than any single fixed point, so a dynamic bound answers a stricter performance question. The bound also makes its own limit clear: frequent or large comparator changes cost more. The chapter relates this framework to earlier work on drift in online learning; the formal target here is the precise statement in the pinned arXiv version, with its explicit constants and final Bregman term. Source, Chapter 14, pp. 227–229.

Setting and notation

Let $E$ be a finite-dimensional real normed space, $V\subseteq X\subseteq E$, and $V$ a nonempty closed convex feasible set. On round $t=1,\ldots,T$, the learner plays $x_t\in V$, receives a real-valued loss $\ell_t$, and selects a subgradient $g_t$ at $x_t$. A comparison sequence $u_1,\ldots,u_T$ consists of arbitrary points in $V$. The dynamic regret is

$$\operatorname{DRegret}_T(u_1,\ldots,u_T) =\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u_t)\bigr).$$

The path length of the comparison sequence is the total distance between successive points:

$$P(u_1,\ldots,u_T)=\sum_{t=2}^{T}\lVert u_t-u_{t-1}\rVert.$$

It is zero for a constant sequence. The path starts at round two, so neither $u_0$ nor an artificial first movement enters the claim. The norm on $E$ is arbitrary. Its dual norm on continuous linear functionals is written $\lVert\cdot\rVert_*$.

Online mirror descent uses a differentiable regularizer $\psi$ and its Bregman divergence

$$B_\psi(a;b)=\psi(a)-\psi(b)-\langle\nabla\psi(b),a-b\rangle.$$

At each round, the next point minimizes $\langle g_t,z\rangle+B_\psi(z;x_t)/\eta$ over $z\in V$, with one constant step size $\eta>0$. The regularizer is closed and $\lambda$-strongly convex, with $\lambda>0$, on the stated domain. Its derivative must be evaluated at interior points of $X$. For a horizon $T\ge1$, the theorem measures the range of the gradients seen along the run by the finite maximum

$$Q=\max_{1\le t\le T}\lVert\nabla\psi(x_t)-\nabla\psi(x_1)\rVert_*.$$

The maximum includes $x_1$, at which the difference is zero, and stops at $x_T$. These conventions are the ones in Definition 14.1 and Theorem 14.2.

Formalization targets

One-step mirror descent estimate

The first milestone is the inequality part of Lemma 6.10. For each feasible comparator, one OMD update controls the loss difference by a decrease in Bregman divergence plus a quadratic dual-norm term. The milestone records the book's whole inequality chain, including the intermediate term that exposes the change in the iterate. It is the local estimate used at every round of Theorem 14.2. Lemma 6.10, p. 67.

Summed comparison with an extra endpoint

The second milestone is the display in the proof of Theorem 14.2 immediately before the final choice $u_{T+1}=u_T$. It keeps that additional comparator free and shows the gradient-difference sum explicitly. This intermediate statement is useful for inspecting the sign and time index of each comparator shift. Proof of Theorem 14.2, pp. 228–229.

Goal: dynamic regret of online mirror descent

The goal is the full bound of Theorem 14.2:

$$\operatorname{DRegret}_T(u_1,\ldots,u_T) \le \frac{B_\psi(u_T;x_1)+Q P(u_1,\ldots,u_T)}{\eta} +\frac{\eta}{2\lambda}\sum_{t=1}^{T}\lVert g_t\rVert_*^2 -\frac{B_\psi(u_T;x_{T+1})}{\eta}.$$

It applies to every feasible comparator sequence, including a constant one. The negative terminal divergence is part of the target. Retaining it makes the statement match the source and preserves information for later use. Theorem 14.2, p. 228.

What the result gives

The theorem quantifies how much a comparator may move before its performance becomes hard to match. The cost of movement is linear in the path length and scaled by the regularizer-gradient range $Q$. With a bounded dual norm for the observed subgradients and a suitable constant step size, the chapter derives a square-root dependence on the horizon for slowly moving sequences. A static comparator has path length zero and recovers the familiar mirror-descent setting. The bound also applies to arbitrary norms and regularizers, so it is not limited to Euclidean projection. Discussion after Theorem 14.2, p. 229.

The mathematical result is proved in the book. The remaining task is to give its exact assumptions, update rule, intermediate inequality, and final inequality machine-checked proofs. The already published Bregman definition supplies a reusable representation of $B_\psi$; the new run, path-length, and gradient-maximum definitions supply the chapter's missing interface. Those definitions can support later formalizations of tracking regret and other moving-comparator results. No proof of the present chapter result is claimed by these draft statements.

Difficulty

For a fixed comparator, the Bregman terms from successive rounds line up directly. With $u_t$ changing, they do not: each transition changes the first argument of $B_\psi$. The resulting correction depends on differences of regularizer gradients, and its time index must agree with the path-length sum. A simple replacement of the static comparator by $u_t$ in a static regret theorem therefore leaves an unaccounted term. The terminal point $x_{T+1}$ is also essential to the full telescoping statement. The mission asks for the book's exact constant and terminal term rather than only an asymptotic rate.

Formalization scope

The Lean model uses a finite-dimensional real normed space. Losses and the regularizer are real-valued on their evaluated domains; the feasible-set and domain predicates represent the book's extended-real convention outside those domains. Closedness of the regularizer is represented by a closed epigraph over $X$. Subgradients are continuous linear functionals, so their operator norm is the dual norm. The run predicate represents every admissible subgradient and argmin choice for Algorithm 6.1; it also carries the required membership of $x_1,\ldots,x_{T+1}$ in $V\cap\operatorname{int}X$. The run is a predicate on sequences, not a selected canonical sequence.

The book's round labels start at one. Index zero is unused. The horizon is at least one, and $\eta,\lambda$ are positive. These conditions keep the finite maximum nonempty and every denominator meaningful. The subgradient condition is relative to $V$, which is sufficient for the theorem's comparisons and slightly weaker than the book's full-space subgradient convention. This choice is disclosed in the item statements. The comparator sequence is universally quantified through its feasibility condition; it is never restricted to a constant sequence or assumed to satisfy the conclusion. The definitions and theorem statements invite proofs of the one-step inequality, the summed estimate, and the final bound, as well as reusable results about Bregman divergence on arbitrary normed spaces.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv

Motivation

Phase recovery (also called phase retrieval) asks to reconstruct a complex signal from the magnitudes of linear measurements of it, the phases being lost. It arises wherever detectors record intensities only: X-ray crystallography, diffraction imaging, astronomy and optics, where a sensor measures $|\langle a_i, x\rangle|^2$ and not $\langle a_i, x\rangle$. The classical algorithms are alternating projections of Gerchberg–Saxton type (Gerchberg and Saxton, 1972; Fienup, 1982), which are fast but non-convex and can stall at stationary points that are not solutions.

Two convex relaxations change this picture. PhaseLift (Chai, Moscoso and Papanicolaou, 2011; Candès, Strohmer and Voroninski, 2013) lifts the signal $x$ to the rank-one matrix $xx^*$ and relaxes the rank constraint to a trace minimization; for random Gaussian measurements it provably recovers $x$ with high probability (Candès and Li, 2014). Waldspurger, d'Aspremont and Mallat (arXiv:1206.0102v3, Math. Programming 2015) instead separate amplitude and phase and obtain PhaseCut, a semidefinite program with the structure of the Goemans–Williamson MaxCut relaxation, for which MaxCut algorithms (block coordinate descent, rounding) apply. The question this mission formalizes is how the two relaxations compare in the noiseless case.

Timeline. An earlier version of the paper showed that PhaseLift tightness implies PhaseCut tightness; Voroninski (2012, working paper, cited in arXiv:1206.0102v3, §4.3) reversed the argument under additional assumptions. Version 3 of the paper (2013) introduces the refined program PhaseCutMod and proves that, for injective $A$, PhaseCutMod is tight whenever PhaseLift is (Corollary 4.3).

Setting

Fix a measurement matrix $A\in\mathbb C^{n\times p}$ with rows $a_1^*,\dots,a_n^*$, and a vector of amplitudes $b\in\mathbb R^n$. The phase recovery problem (1) is

$$\text{find } x\in\mathbb C^p \text{ such that } |Ax| = b,$$

i.e. $|a_i^*x| = b_i$ for every $i$. Write $\mathbf H_m$ for the $m\times m$ Hermitian matrices and $X\succeq 0$ for positive semidefiniteness. When $A$ is injective, $A^*A$ is invertible and the pseudoinverse is $A^\dagger = (A^*A)^{-1}A^*$; $AA^\dagger$ is the orthogonal projector onto the range of $A$. With $\operatorname{diag}(b)$ the diagonal matrix of the $b_i$, set

$$M = \operatorname{diag}(b)(\mathbf I - AA^\dagger)\operatorname{diag}(b),\qquad B = \operatorname{diag}(b)A^{\dagger *}A^\dagger\operatorname{diag}(b).$$

The three programs are

$$\text{(PhaseLift)}\quad \min_{X\in\mathbf H_p} \operatorname{Tr}(X)\ \ \text{s.t.}\ \operatorname{Tr}(a_ia_i^*X) = b_i^2,\ i=1,\dots,n,\ X\succeq 0;$$ $$\text{(PhaseCut)}\quad \min_{U\in\mathbf H_n} \operatorname{Tr}(UM)\ \ \text{s.t.}\ \operatorname{diag}(U) = 1,\ U\succeq 0;$$ $$\text{(PhaseCutMod)}\quad \min_{U\in\mathbf H_n} \operatorname{Tr}(BU)\ \ \text{s.t.}\ \operatorname{Tr}(MU) = 0,\ \operatorname{diag}(U) = 1,\ U\succeq 0.$$

PhaseCutMod selects, among the optimal points of PhaseCut (which in the noiseless case are exactly its points with $\operatorname{Tr}(MU)=0$), one of minimal $\operatorname{Tr}(BU)$. A relaxation is tight when it has a unique optimal solution and that solution has rank one. The two lifted programs are linked by the map

$$\Phi(X) = \operatorname{diag}(b)^{-1}AXA^*\operatorname{diag}(b)^{-1}.$$

In Lean these objects are PhaseCut.Tight.pinv, Mmat, Bmat, Phi, IsSolvable, phaseLiftFeasible/phaseLiftOptimal, phaseCutFeasible/phaseCutOptimal, phaseCutModFeasible/phaseCutModOptimal and IsTight.

Formalization targets

Goal: Corollary 4.3 (p. 13)

If $A$ is injective, $b_i\neq 0$ for all $i$, and (1) has an exact solution, then

$$\text{PhaseLift is tight}\ \Longrightarrow\ \text{PhaseCutMod is tight}.$$

The statement fixes no constants and no probabilistic model: it is a deterministic comparison of two programs, valid for every $A$ and $b$ meeting the three hypotheses.

Milestones

1. $M\succeq 0$ (§2.2, p. 4).
2. For $U, M\succeq 0$, $\operatorname{Tr}(UM)=0$ implies $UM=0$ (proof of Proposition 4.2, p. 12).
3. $\operatorname{Tr}(MU)=0,\ U\succeq 0$ (15) holds iff $U=\Phi(X)$ for some $X\succeq 0$ (16) (proof of Proposition 4.2, p. 12).
4. Proposition 4.2 (p. 12): $\Phi$ is a bijection from the feasible set of PhaseLift onto the feasible set of PhaseCutMod.
5. $\operatorname{Tr}(X) = \operatorname{Tr}(B\Phi(X))$ (proof of Corollary 4.3, p. 13).
6. $\operatorname{Rank}(X) = \operatorname{Rank}(\Phi(X))$ (proof of Corollary 4.3, p. 13).
7. Companion: when (1) is solvable, every optimal solution of PhaseCut is feasible for PhaseCutMod (§4.3, p. 12).

Significance

The result. Corollary 4.3 says that the MaxCut-type relaxation, once refined to PhaseCutMod, is never worse than PhaseLift at exact recovery: every recovery guarantee proved for PhaseLift (for instance the Gaussian-measurement results of Candès–Strohmer–Voroninski and Candès–Li) transfers to PhaseCutMod. Since PhaseCutMod can be approached by solving PhaseCut with $M$ replaced by $M+\gamma B$ for small $\gamma>0$, the algorithms designed for PhaseCut (greedy and block-coordinate SDP solvers) inherit those guarantees. The bijection of Proposition 4.2 also gives a precise dictionary between the lifted signal space $\mathbf H_p$ and the phase space $\mathbf H_n$.

Formalizing it. The result is proved in the paper; to the best of current knowledge none of it has a machine-checked proof. The mission produces a formal statement of the three programs over complex Hermitian matrices, of the pseudoinverse identities for injective matrices, and of the trace and rank transport under the congruence $\Phi$, which are reusable for other lifting arguments in phase retrieval and low-rank SDP.

Difficulty

The corollary itself is short once Proposition 4.2 and the two transport identities are available; the substance lies in Proposition 4.2. The natural first attempt is to check that $\Phi$ maps feasible points to feasible points, which is direct. Surjectivity is the step that requires an argument: a PhaseCutMod-feasible $U$ satisfies only the scalar constraint $\operatorname{Tr}(MU)=0$, and one must first upgrade it to the matrix equation $MU=0$ (using positive semidefiniteness of both factors) and then to a range condition on $\operatorname{diag}(b)U\operatorname{diag}(b)$ before a preimage can be written down. In Lean, an additional cost is the absence of a pseudoinverse and of trace-zero-product lemmas for complex Hermitian matrices in the form needed, and the bookkeeping between complex traces and real objectives.

Formalization scope

Matrices are Matrix (Fin n) (Fin p) ℂ and Matrix (Fin m) (Fin m) ℂ; $X\succeq 0$ is Mathlib's Matrix.PosSemidef (Hermitian included); rank is Matrix.rank. Conventions committed to:

• Injectivity is Function.Injective A.mulVec. $A^\dagger$ is encoded as (Aᴴ * A)⁻¹ * Aᴴ, Mathlib's inverse returning $0$ on singular matrices; it is the pseudoinverse only for injective $A$, so every statement mentioning $M$, $B$ or $\Phi$ assumes injectivity. This adds injectivity, not present on the page, to the claim $M\succeq 0$ (p. 4) and to the companion claim on p. 12.
• $\operatorname{diag}(b)^{-1}$ has entries $b_i^{-1}$ and is used only under $b_i\neq 0$.
• $\operatorname{Tr}(a_ia_i^*X) = a_i^*Xa_i$ is the diagonal entry $(AXA^*)_{ii}$.
• Objectives are real parts of complex traces (the traces are real on the feasible sets); the PhaseCutMod constraint $\operatorname{Tr}(MU)=0$ is an equation in $\mathbb C$.
• Optimal sets are sets of minimizers over the feasible set; tight means the optimal set equals $\{X\}$ for some $X$ of rank one. Weakening this to "some optimal solution has rank one" would be a different, weaker statement and is excluded, as is applying tightness to the feasible set instead of the optimal set.
• Proposition 4.2's "bijection" is Set.BijOn Φ (PhaseLift feasible) (PhaseCutMod feasible).
• The hypotheses of Proposition 4.2 and Corollary 4.3 are the page's, including the solvability of (1).

Infrastructure that a complete development needs, and that is reusable beyond this mission: the pseudoinverse identities $A^\dagger A = \mathbf I$ and $AA^\dagger A = A$ for injective complex $A$, the fact that $\mathbf I - AA^\dagger$ is a Hermitian idempotent, the lemma $\operatorname{Tr}(UM)=0\Rightarrow UM=0$ for complex positive semidefinite matrices, and rank invariance under congruence by injective matrices. Proofs of any milestone are welcome, as are general Mathlib-style lemmas on these points.

Selected references

• I. Waldspurger, A. d'Aspremont, S. Mallat, Phase recovery, MaxCut and complex semidefinite programming, Mathematical Programming 149 (2015); preprint arXiv:1206.0102v3 (2013). https://arxiv.org/abs/1206.0102
• E. J. Candès, T. Strohmer, V. Voroninski, PhaseLift: Exact and stable signal recovery from magnitude measurements via convex programming, Comm. Pure Appl. Math. 66 (2013). https://arxiv.org/abs/1109.4499
• E. J. Candès, X. Li, Solving quadratic equations via PhaseLift when there are about as many equations as unknowns, Found. Comput. Math. 14 (2014). https://arxiv.org/abs/1208.6247
• A. Chai, M. Moscoso, G. Papanicolaou, Array imaging using intensity-only measurements, Inverse Problems 27 (2011). https://doi.org/10.1088/0266-5611/27/1/015005
• V. Voroninski, A comparison between the PhaseLift and PhaseCut algorithms, working paper, 2012 (as cited in arXiv:1206.0102v3, p. 28). https://arxiv.org/abs/1206.0102
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995). https://doi.org/10.1145/227683.227684
• J. R. Fienup, Phase retrieval algorithms: a comparison, Applied Optics 21 (1982). https://doi.org/10.1364/AO.21.002758