Optimization

Motivation

Tensor decompositions express a multiway array as a sum of simple terms. The canonical polyadic decomposition (CPD) writes an $N$-th order tensor $\mathcal T\in\mathbb C^{I_1\times\cdots\times I_N}$ as a sum of $R$ outer products of vectors; block term decompositions replace each rank-one term by a term of higher multilinear rank. These models are used in signal processing, blind source separation and telecommunications, and are computed numerically by minimizing a least-squares misfit.

Sorber, Van Barel and De Lathauwer (SIAM J. Optim. 23(2), 2013) introduce the (rank-$L_r\circ$ rank-1) block term decomposition (BTD), which contains both the CPD and the rank-$(L_r,L_r,1)$ BTD as special cases, and develop optimization algorithms for it: nonlinear conjugate gradient and quasi-Newton methods built on the complex gradient, and Gauss–Newton and Levenberg–Marquardt methods built on the Jacobian. For the second family the central object is the Gramian $J^{\mathrm H}J$ of the Jacobian $J$ of the residual. Theorem 4.5 of the paper gives its exact block structure, and that structure is what lets the methods run without ever forming $J$.

Setting

Fix $N = P + Q$ modes with dimensions $I_1,\dots,I_N$, a number of terms $R$, and block sizes $L_1,\dots,L_R$; put $R' = \sum_r L_r$. The BTD approximates $\mathcal T$ by

$$\sum_{r=1}^R\Big(\sum_{r'} a^{(1)}_{r'}\circ\cdots\circ a^{(P)}_{r'}\Big)\circ\big(c^{(1)}_r\circ\cdots\circ c^{(Q)}_r\big),$$

where the inner sum runs over the $L_r$ columns of block $r$. Here $A^{(p)} = [a^{(p)}_1\cdots a^{(p)}_{R'}]\in\mathbb C^{I_p\times R'}$ and $C^{(q)} = [c^{(q)}_1\cdots c^{(q)}_R]\in\mathbb C^{I_{P+q}\times R}$.

The paper reads this as a structured CPD in $R'$ rank-one terms. The first $P$ factor matrices are the $A^{(p)}$, and the last $Q$ are

$$A^{(P+q)} = C^{(q)}\cdot E,$$

where $E = \mathrm{diag}(1_{1\times L_1},\dots,1_{1\times L_R})\in\mathbb R^{R\times R'}$ copies column $r$ of $C^{(q)}$ into the $L_r$ columns of block $r$. The residual tensor is

$$\mathcal F_{\mathrm{BTD}} = \sum_{c=1}^{R'} a^{(1)}_c\circ\cdots\circ a^{(N)}_c - \mathcal T,$$

and the unknowns are $z = (\mathrm{vec}A^{(1)},\dots,\mathrm{vec}A^{(P)},\mathrm{vec}C^{(1)},\dots,\mathrm{vec}C^{(Q)})$. The Jacobian $J = \partial\,\mathrm{vec}(\mathcal F_{\mathrm{BTD}})/\partial z^{\mathrm T}$ is the complex (holomorphic) derivative: $\mathcal F_{\mathrm{BTD}}$ is a polynomial in $z$, not in $\bar z$.

Three auxiliary matrices enter the answer. The first is $W^\sigma = \ast_{m\notin\sigma}A^{(m)\mathrm H}A^{(m)}$, the Hadamard product of the Gramians of the factor matrices outside a mode set $\sigma$, with entries $w^\sigma_{r_1r_2}$. The second is $F^{(q)} = E\otimes\mathbb I_{I_{P+q}}$, which satisfies $\mathrm{vec}(C^{(q)}E)^{\mathrm T} = \mathrm{vec}(C^{(q)})^{\mathrm T}F^{(q)}$ (Proposition 4.1). The third is the block diagonal $\Sigma = \mathrm{diag}(\mathbb I_{I_1R'},\dots,\mathbb I_{I_PR'},F^{(1)},\dots,F^{(Q)})$.

Formalization targets

Goal: Theorem 4.5

For every tensor $\mathcal T$ and every $z$,

$$J^{\mathrm H}J = \Sigma\cdot\big[\Pi^{(n_1,n_2)}\big]_{n_1,n_2=1}^N\cdot\Sigma^{\mathrm T},$$ $$\Pi^{(n_1,n_2)} \triangleq \Big(\tfrac{\partial\,\mathrm{vec}\mathcal F}{\partial\,\mathrm{vec}(A^{(n_1)})^{\mathrm T}}\Big)^{\mathrm H}\Big(\tfrac{\partial\,\mathrm{vec}\mathcal F}{\partial\,\mathrm{vec}(A^{(n_2)})^{\mathrm T}}\Big) = \begin{cases}W^{\{n\}}\otimes\mathbb I_{I_n} & n=n_1=n_2,\\ \big[w^{\{n_1,n_2\}}_{r_1r_2}\,a^{(n_1)}_{r_2}a^{(n_2)\mathrm H}_{r_1}\big]_{r_1,r_2} & \text{otherwise.}\end{cases}$$

The goal has two parts, and both are required. The first is that the Gramian of the CPD Jacobian equals the explicit block matrix. The second is the factorization through $\Sigma$.

Milestones

1. The columns of the CPD Jacobian are rank-one tensors: $\partial\mathcal F/\partial a^{(n)}_{ir} = a^{(1)}_r\circ\cdots\circ e^{(n)}_i\circ\cdots\circ a^{(N)}_r$.
2. Diagonal blocks: inner products $w^{\{n\}}_{r_1r_2}\delta_{ij}$, hence the block $w^{\{n\}}_{r_1r_2}\mathbb I_{I_n}$.
3. Off-diagonal blocks: inner products $w^{\{n_1,n_2\}}_{r_1r_2}a^{(n_1)}_{ir_2}\overline{a^{(n_2)}_{jr_1}}$, hence the rank-one block $w^{\{n_1,n_2\}}_{r_1r_2}a^{(n_1)}_{r_2}a^{(n_2)\mathrm H}_{r_1}$.
4. Proposition 4.1: the vec identity for $C^{(q)}E$ and the chain rule (4.3b) for the Jacobian columns of $C^{(q)}$.
5. The blocks of $J^{\mathrm H}J$ that involve some $C^{(q)}$ are $\Pi F^{(q)\mathrm T}$, $F^{(q)}\Pi$ and $F^{(q_1)}\Pi F^{(q_2)\mathrm T}$, i.e. $J^{\mathrm H}J = \Sigma\,(J_{\mathrm{CPD}}^{\mathrm H}J_{\mathrm{CPD}})\,\Sigma^{\mathrm T}$.

Significance

With Theorem 4.5, $J^{\mathrm H}J$ is determined by the factor matrices and the small Gramians $A^{(n)\mathrm H}A^{(n)}$. For a hypercubical CPD this takes $O(NR^2)$ extra memory instead of the $O(N^2R^2I^2)$ of a dense Gramian. Theorem 4.6 of the paper then turns the same structure into a matrix–vector product in $O(NR^2I)$ operations, which is what inexact Gauss–Newton and Levenberg–Marquardt steps solved by preconditioned conjugate gradients require. The block-diagonal part $\Pi^{(n,n)} = W^{\{n\}}\otimes\mathbb I$ also gives the block Jacobi preconditioner of the paper's §4.2. For the CPD, expressions for the Gramian were already studied in chemometrics (the paper cites G. Tomasi's 2006 thesis for this); Theorem 4.5 states the block structure in closed form and extends it to the structured BTD through $\Sigma$.

The result is proved in the paper. As far as a search of Prove2Me and Mathlib shows, nothing about CPD or BTD Jacobians has been formalized. This mission produces a machine-checked proof of the block structure, starting from an explicit model of the decomposition and an honest complex derivative. That model (outer products, the structured CPD, $E$, $\Sigma$, the Hadamard-Gramian products) can be reused for the paper's cogradient theorem and for other tensor algorithms.

Difficulty

The identity is finite-dimensional, but no single step reduces it to a known lemma. First, $J$ is a genuine derivative of a multilinear polynomial map in $\sum_n I_nR'$ complex variables, so each entry has to be computed from the derivative of a sum of products. Second, $J^{\mathrm H}J$ is a sum over all $\prod_n I_n$ multi-indices. Turning it into the product of Gramians in $W^\sigma$ means exchanging a sum of products with a product of sums while one or two modes are held fixed, with the conjugates landing on crossed column indices ($a^{(n_1)}_{r_2}$, $\bar a^{(n_2)}_{r_1}$). Third, the structured factor matrices $A^{(P+q)} = C^{(q)}E$ are not unknowns. The derivative with respect to $C^{(q)}$ has to go through the chain rule and the vec–Kronecker identity, and $\Sigma$'s rows and columns are indexed by different sets.

Formalization scope

All objects are defined in TensorBTD.Gramian.Setting, with the following conventions.

• Modes and columns. The $N$ modes are Fin P ⊕ Fin Q (mode $p$ is Sum.inl (p-1) and mode $P+q$ is Sum.inr (q-1)), so all indices are 0-based. The $R'$ columns are Σ r : Fin R, Fin (L r) in lexicographic order, which is the order of (3.5).
• Tensors and residuals. A tensor is a function of the multi-index. The residual is defined entrywise as a sum of outer products. The paper's (3.8) is its mode-$n$ unfolding.
• Vectorization and Kronecker products. Vectorized indices are (column, row) pairs, Mathlib's column-major Matrix.vec. This is the paper's Definition 2.5 with its misprint $(i+(j-1)J)$ corrected to $(i+(j-1)I)$. Kronecker products are Mathlib's ⊗ₖ.
• Jacobian. The Jacobian is defined column by column as the complex derivative deriv of $t\mapsto G(x+te_\beta)$ at $0$. It is not defined by its closed form, and it is not a real derivative.
• The unstructured CPD. $\Pi^{(n_1,n_2)}$ differentiates with respect to $A^{(n)}$ for every $n$, including $n>P$, where $A^{(n)}$ is not an unknown. It is therefore taken as the Jacobian of the unstructured CPD residual in $R'$ terms, with all $N$ factor matrices free, evaluated at the factor matrices of $z$. This is how the paper's proof uses it.

There are no hypotheses. The paper's assumptions that $P, Q\ge 1$ and its qualifiers "nonzero" and "rank-$L_r$" are not used in Section 4, so they are dropped. This is a generalization: $Q = 0$ gives the plain CPD in $R'$ terms.

A goal that took the closed form of $\Pi$ as the definition, or that defined $J$ entrywise by the outer-product formula of milestone 1, would only state a sum identity. Both are ruled out: $J$ is a derivative, and the goal asserts that the Gramian of the CPD Jacobian equals the closed form. A misprint in the proof's closing paragraph, $F^{(q)}\Pi^{(p,P+q)}$ for the $(P+q,p)$ block, is corrected in Lean to $F^{(q)}\Pi^{(P+q,p)}$.

Useful Mathlib infrastructure includes Matrix.vec, Matrix.kroneckerMap, Matrix.blockDiagonal', Finset.prod_univ_sum and the derivative rules for finite products (HasDerivAt.finset_prod). General lemmas welcome as contributions: derivatives of multilinear maps along coordinate directions, the sum–product exchange over Fintype.piFinset, and the chain rule for a Jacobian composed with a linear map.

Selected references

• L. Sorber, M. Van Barel, L. De Lathauwer, Optimization-Based Algorithms for Tensor Decompositions: Canonical Polyadic Decomposition, Decomposition in Rank-$(L_r,L_r,1)$ Terms, and a New Generalization, SIAM J. Optim. 23(2), 695–720, 2013. https://doi.org/10.1137/120868323
• T. G. Kolda, B. W. Bader, Tensor Decompositions and Applications, SIAM Review 51(3), 455–500, 2009. https://doi.org/10.1137/07070111X
• L. De Lathauwer, Decompositions of a Higher-Order Tensor in Block Terms — Part II: Definitions and Uniqueness, SIAM J. Matrix Anal. Appl. 30(3), 1033–1066, 2008. https://doi.org/10.1137/070690729
• L. Sorber, M. Van Barel, L. De Lathauwer, Unconstrained Optimization of Real Functions in Complex Variables, SIAM J. Optim. 22(3), 879–898, 2012. https://doi.org/10.1137/110832124

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

Nesterov's accelerated gradient method minimizes a convex function $f$ with $L$-Lipschitz gradient at the rate $O(1/k^2)$, which is optimal among first-order methods. For a $\mu$-strongly convex $f$ the method with the generic momentum coefficient $(k-1)/(k+2)$ does not exploit the strong convexity: Su, Boyd and Candès show in §4.2 of arXiv:1503.01243 that its rate stays polynomial. Linear convergence $O((1-\sqrt{\mu/L})^k)$ is available with the momentum $(\sqrt L-\sqrt\mu)/(\sqrt L+\sqrt\mu)$, but this requires knowing $\mu$, which is rarely available in practice.

Restarting is the practical remedy. O'Donoghue and Candès (2013) proposed gradient restarting: reset the momentum whenever the objective increases. It is observed to recover linear convergence, but no rate was proved for it. Section 5 of Su, Boyd and Candès proposes a variant, speed restarting, which resets the momentum when the speed of the iterates stops increasing, and proves a linear rate for its continuous-time limit. This mission formalizes that result, Theorem 10 of the paper, and the lemmas it rests on.

Setting

Write $\mathbb R^n$ with the Euclidean norm. A function $f:\mathbb R^n\to\mathbb R$ is in $\mathcal F_L$ if it is convex and continuously differentiable with $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$. It is in $\mathcal S_\mu$ if it is continuously differentiable and $f(x)-\mu\|x\|^2/2$ is convex. The class $\mathcal S_{\mu,L}=\mathcal F_L\cap\mathcal S_\mu$ with $0<\mu\le L$ is the standing assumption of the whole mission. A minimizer is written $x^\star$ and $f^\star=f(x^\star)$; the ratio $L/\mu$ is the condition number.

The Nesterov ODE is

$$\ddot X(t)+\frac3t\dot X(t)+\nabla f(X(t))=0,\qquad X(0)=x_0,\ \dot X(0)=0, \tag{3}$$

the continuous-time limit of Nesterov's scheme with step size tending to zero. The paper's Theorem 1 shows it has a unique solution in $C^2((0,\infty))\cap C^1([0,\infty))$. In Lean a solution is a pair $(X,V)$ with $V=\dot X$ (IsSolution f 3 x₀ X V).

The speed restarting time of the solution from $x_0$ is

$$T=T(x_0;f)=\sup\Bigl\{t>0:\ \forall u\in(0,t),\ \frac{\mathrm d\|\dot X(u)\|^2}{\mathrm du}>0\Bigr\},$$

the first time at which the speed $\|\dot X\|$ decreases (restartTime; the set is restartSet).

The speed restarted ODE (29) replaces $3/t$ by $3/t_{\mathrm{sr}}$, where $t_{\mathrm{sr}}=t-\tau$ is the time since the latest restart $\tau$. Its solution $X^{\mathrm{sr}}$ starts at $x_0$, follows (3) from $x_0$ for time $T_1=T(x_0;f)$, then follows (3) from $X^{\mathrm{sr}}(T_1)$ for time $T_2=T(X^{\mathrm{sr}}(T_1);f)$, and so on. If a restart point is a minimizer the trajectory stays there. In Lean this is the predicate IsSpeedRestarted f x₀ Xsr.

Formalization targets

Goal: Theorem 10

There are positive constants $c_1,c_2$, depending only on $L/\mu$, such that for every $f\in\mathcal S_{\mu,L}$, every $x_0$ and every $t\ge0$,

$$f(X^{\mathrm{sr}}(t))-f^\star\le\frac{c_1L\|x_0-x^\star\|^2}2\,e^{-c_2t\sqrt L}.$$

The constants are left unspecified, so the goal survives improvements of them.

Milestones

For one unrestarted solution $X$ of (3), with $M(t)=\sup_{u\in(0,t]}\|\dot X(u)\|/u$:

• Lemma 11. For $t<\sqrt{12/L}$: $M(t)\le\|\nabla f(x_0)\|/(4(1-Lt^2/12))$.
• (30). For $0<t<\sqrt{12/L}$: $\bigl|\,\|\dot X(t)\|-\tfrac t4\|\nabla f(x_0)\|\,\bigr|\le L\|\nabla f(x_0)\|t^3/(48(1-Lt^2/12))$.
• Lemma 25. If $x_0\ne x^\star$: $T(x_0,f)\ge 4/(5\sqrt L)$.
• Descent display. $\dfrac{\mathrm df(X(t))}{\mathrm dt}=-\dfrac3t\|\dot X\|^2-\dfrac12\dfrac{\mathrm d\|\dot X\|^2}{\mathrm dt}\le0$ for $t\le T$.
• Lemma 12. For a universal $C>0$: $f(X(T))-f^\star\le(1-C\mu/L)(f(x_0)-f^\star)$.
• Lemma 13. For a universal $\tilde C$: $T\le 4\exp(\tilde CL/\mu)/(5\sqrt L)$.

Significance

Theorem 10 is a linear convergence guarantee for a momentum method that does not need $\mu$: the restart rule only watches the speed. The paper presents it as a new result; gradient restarting has no comparable theorem. It also gives a framework for analyzing restart rules: each restart decreases the gap by a factor depending on $L/\mu$ (Lemma 12), and restarts happen at a rate bounded below (Lemmas 13 and 25). Section 5.3 of the paper reports that the discrete analogue of the scheme (Algorithm 1) converges linearly in experiments.

The results are proved in the paper, but not formalized anywhere to our knowledge; the platform has no statement about restarting the Nesterov ODE. The formal work is the full proof, in particular the analysis of (3) near its singular point $t=0$. Sharper constants are of interest: the paper conjectures that $T=O(\sqrt L/\mu)$ for a large class of $f$, which would improve $c_2$, and the generalization to friction $r/t$ with $r>3$ mentioned after Theorem 10 is a natural further target.

Difficulty

The ODE (3) is singular at $t=0$, so the standard Picard–Lindelöf theory does not apply there, and the small-time estimates (Lemma 11, (30), Lemma 25) must control the solution uniformly up to $t=0$, where the friction coefficient $3/t$ is unbounded. Lemma 11 bounds a supremum by a quantity that involves the same supremum; this argument needs a separate proof that the supremum is finite.

The speed restarting time is defined as a supremum, and neither $T>0$ nor $T<\infty$ follows from the definition. The restarted trajectory is assembled from infinitely many segments, and the number of restarts before time $t$ needs a lower bound. The obvious route through the $O(1/t^2)$ rate of the unrestarted ODE gives only a polynomial rate, because it does not use strong convexity in a way that survives the restarts.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, $L$ is an NNReal, and $\mathcal S_\mu$ is the paper's literal definition. The classes $\mathcal F_L$, $\mathcal S_{\mu,L}$ and the solution predicate of (3) come from the series' shared definitions (NesterovODE.WellPosed.Setting, NesterovODE.StrongCvx.Setting); the speed restarting time and the restarted trajectory sit in this mission's Setting definition, namespace NesterovODE.Restart.

Conventions the formalization commits to:

• Solutions of (3) are pairs $(X,V)$, quantified over: every solution in the regularity class of Theorem 1 is covered. Values at negative times are unconstrained.
• $\tfrac12\mathrm d\|\dot X\|^2/\mathrm du$ is written as $\langle V(u),-\tfrac3uV(u)-\nabla f(X(u))\rangle$, its value along a solution.
• $M(t)$ is not defined; Lemma 11 is stated as a bound on every $\|\dot X(u)\|/u$, $u\in(0,t]$.
• Lean's sSup is $0$ on an empty or unbounded set. Lemma 25 is stated as membership of $4/(5\sqrt L)$ in the set defining $T$, and Lemma 13 as a bound on every element of that set, so neither can hold through this junk value.
• The constants of Lemmas 12 and 13 are chosen before the dimension, $f$, $\mu$, $L$, $x_0$ and the trajectory; those of Theorem 10 are functions of $L/\mu$ chosen in the same position. Choosing them after $f$ would trivialize the statements and is ruled out.
• Lemmas 11, 12, 13, 25, (30) and the descent display carry the standing assumption $f\in\mathcal S_{\mu,L}$; Lemmas 12, 13, 25 also carry $x_0\ne x^\star$, the paper's convention in §5. Theorem 10 holds for every $x_0$.
• The leftmost "$0\le$" of (30) is stated for $0<t\le\sqrt{6/L}$, the range on which it is true; the page writes it for all $t<\sqrt{12/L}$.
• The restarted trajectory stays at a minimizer once it reaches one. Restart times tending to infinity is not assumed: it follows from Lemmas 25 and 13.

A complete development needs the analysis of (3) at $t=0$ (also the subject of mission I of this series), monotonicity arguments from derivative signs, and properties of strongly convex functions with Lipschitz gradient. The last two are reusable beyond this mission. Proofs of any milestone, and statements with explicit constants, are welcome.

Selected references

• W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, arXiv:1503.01243v2, 2015; J. Mach. Learn. Res. 17(153):1–43, 2016. https://arxiv.org/abs/1503.01243
• B. O'Donoghue, E. J. Candès, Adaptive Restart for Accelerated Gradient Schemes, Foundations of Computational Mathematics 15:715–732, 2015. https://doi.org/10.1007/s10208-013-9150-3
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

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