Convex Optimization

Motivation

Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the simplest matrix consistent with a set of linear observations, where "simplest" means "of least rank". Given a linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ and a vector $b\in\mathbb R^p$, the affine rank minimization problem is

$$\min_X\ \operatorname{rank}(X)\quad\text{s.t.}\quad \mathcal A(X)=b .$$

This problem is NP-hard in general: it contains the problem of finding the sparsest solution of a linear system as the special case of diagonal matrices. A standard heuristic, popularized in control by Fazel, Hindi and Boyd, replaces the rank by the nuclear norm $\|X\|_*$, the sum of the singular values, which is the convex envelope of the rank on the unit ball of the operator norm. The resulting problem is a semidefinite program and can be solved efficiently.

Recht, Fazel and Parrilo (arXiv:0706.4138, SIAM Review 2010) gave the first general conditions under which this heuristic provably returns the minimum-rank solution. Their argument transfers the compressed sensing theory of Candès and Tao (Decoding by linear programming, 2005) and Candès, Romberg and Tao from sparse vectors and the $\ell_1$ norm to low-rank matrices and the nuclear norm. This mission formalizes the paper's deterministic recovery theorem (Section 3).

Setting

Matrices are real $m\times n$ matrices. For matrices $X,Y$ of the same size, $\langle X,Y\rangle=\operatorname{Tr}(X^{\top}Y)=\sum_{i,j}X_{ij}Y_{ij}$ is the trace inner product. With $\sigma_1(X)\ge\sigma_2(X)\ge\dots\ge0$ the singular values of $X$, the three norms used are the operator norm $\|X\|=\sigma_1(X)$, the Frobenius norm $\|X\|_F=\sqrt{\langle X,X\rangle}=(\sum_i\sigma_i(X)^2)^{1/2}$, and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$.

A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by $p$ measurement matrices $A_1,\dots,A_p$ through $\mathcal A(X)_i=\langle A_i,X\rangle$; $\|\mathcal A(X)\|$ is the Euclidean norm of the vector $\mathcal A(X)\in\mathbb R^p$.

For an integer $r$, the $r$-restricted isometry constant $\delta_r(\mathcal A)$ (Definition 3.1) is the smallest $\delta\ge0$ with

$$(1-\delta)\,\|X\|_F\le\|\mathcal A(X)\|\le(1+\delta)\,\|X\|_F\qquad\text{for every } X \text{ with } \operatorname{rank}X\le r .$$

Fix a matrix $X_0$ of rank at most $r$, put $b=\mathcal A(X_0)$, and consider the nuclear norm minimization problem

$$X^*:=\arg\min_X\ \|X\|_*\quad\text{s.t.}\quad\mathcal A(X)=b. \tag{3.1}$$

Formalization targets

Goal: Theorem 3.3

If $r\ge1$ and $\delta_{5r}(\mathcal A)<\tfrac1{10}$, then $X^*=X_0$; precisely,

$$\forall X\in\mathbb R^{m\times n}:\quad \mathcal A(X)=\mathcal A(X_0)\ \text{ and }\ \|X\|_*\le\|X_0\|_*\ \Longrightarrow\ X=X_0 .$$

The statement holds for every linear map, every $m,n,p$ and every $X_0$ of rank at most $r$. The constant $1/10$ is the paper's; the paper notes (p. 14) that its derivation is chosen for simplicity and is not optimal.

Milestones, in the paper's order

1. Theorem 3.2 (p. 12): if $\delta_{2r}<1$, then $X_0$ is the only matrix of rank at most $r$ with $\mathcal A(X)=b$.
2. (2.1) (p. 6): $\|X\|\le\|X\|_F\le\|X\|_*\le\sqrt r\,\|X\|_F\le r\,\|X\|$ whenever $\operatorname{rank}X\le r$.
3. Lemma 2.3 (p. 9): if $AB^{\top}=0$ and $A^{\top}B=0$, then $\|A+B\|_*=\|A\|_*+\|B\|_*$.
4. Lemma 3.4 (pp. 12–13): every $B$ splits as $B=B_1+B_2$ with $\operatorname{rank}B_1\le2\operatorname{rank}A$, $AB_2^{\top}=0$, $A^{\top}B_2=0$ and $\langle B_1,B_2\rangle=0$.
5. (3.3)–(3.4) (p. 13): for the error $R=R_0+R_c$ of a minimizer, $\|R_c\|_*\le\|R_0\|_*$.
6. (3.5)–(3.6) (p. 13): a matrix splits into pairwise orthogonal pieces of rank at most $3r$ whose Frobenius norms, from the second piece on, sum to at most $\|M\|_*/\sqrt{3r}$.
7. Monotonicity (p. 12): $\delta_r\le\delta_{r'}$ for $r\le r'$.
8. (3.7) (p. 14): $\|\mathcal A(R)\|\ge\big((1-\delta_{5r})-\tfrac9{11}(1+\delta_{3r})\big)\|R_0\|_F$, with a positive factor whenever $9\delta_{3r}+11\delta_{5r}<2$.

Significance

Theorem 3.3 is a deterministic certificate: it separates the question "does nuclear norm minimization recover low-rank matrices?" into a property of the measurement map alone, with an absolute constant independent of $m$, $n$, $r$ and $p$. Section 4 of the same paper then shows that random maps with i.i.d. Gaussian or Bernoulli entries satisfy $\delta_{5r}<1/10$ with high probability once $p$ is of order $r(m+n)\log(mn)$, so a matrix with $mn$ entries is determined by far fewer measurements than entries and is found by a semidefinite program.

The theorem is proved in the paper, and the sparse-vector analogue has been formalized on this platform (HighDimProb.SparseRecovery.rip_implies_exact_recovery, from Vershynin's textbook; CandesTao.Decoding.decoding_by_lp). The matrix version is not formalized. A machine-checked proof needs the basic theory of singular values for rectangular real matrices (the norm comparisons (2.1), additivity of the nuclear norm, the triangle inequality for the nuclear norm, and block decompositions via the singular value decomposition), most of which Mathlib lacks in this form. That infrastructure is reusable for every nuclear-norm result on the platform.

Difficulty

For sparse vectors the analogous proof splits the error vector by its support, and every step is coordinatewise. For matrices there is no common basis: the error $R$ and the target $X_0$ have different singular vectors, and the restricted isometry inequality controls only matrices of low rank. The first obstacle is therefore to split $R$ into a piece of rank at most $2\operatorname{rank}X_0$ and a piece whose row and column spaces are orthogonal to those of $X_0$, so that the nuclear norm is additive. The second is that the triangle inequality, additivity and the norm chain (2.1) for the nuclear norm are themselves nontrivial statements about singular values. Applying the restricted isometry inequality directly to $R$ fails, because $R$ need not have low rank.

Formalization scope

• Matrices are Matrix (Fin m) (Fin n) ℝ; rank is Matrix.rank; transpose is Xᵀ. The norms and the inner product are opNorm, frobeniusNorm, nuclearNorm and traceInner of the published module HighDimStat_MatrixRank_Core, which defines the nuclear norm as the sum of the square roots of the eigenvalues of $X^{\top}X$.
• The map $\mathcal A$ is given by Xs : Fin p → Matrix (Fin m) (Fin n) ℝ and evaluated by observationOp; measNorm Xs X is $\|\mathcal A(X)\|$.
• ripConst Xs r is the infimum of the admissible $\delta\ge0$; the set is nonempty and closed, so the infimum is attained. It is defined for every $r$, not only $1\le r\le m$, since the goal uses $\delta_{5r}$. The paper's normalization $m\le n$ is not assumed.
• The goal assumes $\operatorname{rank}X_0\le r$ rather than $=r$ (equivalent by monotonicity of $\delta$). Its conclusion quantifies over all feasible $X$ with $\|X\|_*\le\|X_0\|_*$, so it does not depend on a choice of arg min. A formalization that fixes some minimizer unrelated to $b$, or only asserts the existence of a minimizer equal to $X_0$, would be trivial and is excluded.
• Milestone (3.5)–(3.6) is stated existentially, listing the properties of the singular value blocks that the proof uses, because Mathlib has no ordered rectangular singular value decomposition. Milestone (3.7) makes explicit the orthogonality $\langle R_0,R_1\rangle=0$ that the paper uses silently.

Welcome contributions: a rectangular SVD with ordered singular values, the triangle inequality and duality for nuclearNorm, and the attainment and monotonicity lemmas for ripConst.

Selected references

• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Review 52(3), 471–501, 2010. https://doi.org/10.1137/070697835 ; preprint arXiv:0706.4138v1. https://arxiv.org/abs/0706.4138
• E. J. Candès, T. Tao, Decoding by Linear Programming, IEEE Trans. Inform. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
• E. J. Candès, J. Romberg, T. Tao, Stable Signal Recovery from Incomplete and Inaccurate Measurements, Comm. Pure Appl. Math. 59(8), 2006. https://doi.org/10.1002/cpa.20124
• M. Fazel, Matrix Rank Minimization with Applications, PhD thesis, Stanford University, 2002.
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §10.5. https://doi.org/10.1017/9781108231596

Motivation

Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time, the problem written $R\,|\,|\sum w_jC_j$ in the three-field notation, is one of the basic NP-hard models of machine scheduling. Each job may take a different time on each machine, as when heterogeneous processors, plants or crews serve the same pool of tasks, and the objective rewards finishing important jobs early. For a single machine the problem is solved exactly by Smith's ratio rule (Smith, 1956). With several unrelated machines the problem is strongly NP-hard and the question is how close to the optimum a polynomial-time algorithm can come.

Timeline of the guarantees for $R\,|\,|\sum w_jC_j$:

• Lenstra, Shmoys and Tardos (1990) gave an LP-based 2-approximation for the makespan on unrelated machines; their assignment variables $a_{ij}$ are the ones used here.
• Hall, Schulz, Shmoys and Wein (1997) gave constant-factor approximations for $\sum w_jC_j$ on unrelated machines via time-indexed and interval-indexed LP relaxations.
• Schulz and Skutella (conference version 1999, journal 2002) obtained $3/2+\varepsilon$ by randomized rounding of a time-indexed LP.
• Skutella (J. ACM 2001), the paper of this mission, gave a convex quadratic relaxation in assignment variables alone and a $3/2$-approximation by randomized rounding, with a short analysis.
• Bansal, Srinivasan and Svensson (2016) improved $3/2$ to $3/2-\varepsilon$ for a small constant $\varepsilon>0$; later work lowered the constant further.

Setting

There are $n$ jobs $j\in J$ and $m$ machines $i$. Job $j$ has a weight $w_j\ge 0$ and a processing time $p_{ij}>0$ on machine $i$. A schedule assigns each job to one machine and orders the jobs on every machine; the completion time $C_j$ of a job is the time at which it finishes when each machine works without idle time.

For a fixed assignment, Smith's ratio rule orders each machine optimally. Fix for each machine $i$ the total order $j\prec_i k$ iff $w_j/p_{ij}>w_k/p_{ik}$, ties broken by index. Under an assignment $\sigma$ the completion time of $j$ is

$$C_j(\sigma)=p_{\sigma(j)j}+\sum_{k\prec_{\sigma(j)}j,\ \sigma(k)=\sigma(j)}p_{\sigma(j)k},$$

and the problem is to minimize $\mathrm{val}(\sigma)=\sum_jw_jC_j(\sigma)$ over all assignments.

With $a_{ij}\in\{0,1\}$ indicating that $j$ runs on $i$, the problem is the integer quadratic program (IQP) with objective

$$Z_{QP}(a)=c^Ta+\tfrac12a^TDa,\qquad c_{ij}=w_jp_{ij},$$

where $D$ is symmetric with entry $w_jp_{ik}$ at $((i,j),(i,k))$ for $k\prec_ij$ and zero across machines and on the diagonal. Relaxing $a_{ij}\in\{0,1\}$ to $a\ge 0$ with $\sum_ia_{ij}=1$ gives (QP). Raising the diagonal gives the convex program (CQP), with objective $Z_{CQP}(a)=\tfrac12c^Ta+\tfrac12a^T(D+\operatorname{diag}(c))a$. Adding the lower bound $c^Ta$ gives (CQP′):

$$\min Z\quad\text{s.t.}\quad \textstyle\sum_ia_{ij}=1,\ \ a\ge 0,\ \ Z\ge Z_{CQP}(a),\ \ Z\ge c^Ta .$$

Randomized rounding of a fractional $\bar a$ sends job $j$ to machine $i$ with probability $\bar a_{ij}$, the choices being pairwise independent across jobs, and then orders every machine by $\prec_i$.

Formalization targets

Goal: (CQP′) is a relaxation, and rounding loses at most 3/2

For every instance with $p>0$, $w\ge 0$:

$$\forall\sigma:\ (a^\sigma,\ \mathrm{val}(\sigma))\ \text{is feasible for (CQP′)},$$ $$\forall(\bar a,Z)\ \text{feasible for (CQP′)}:\quad \mathbb E\Bigl[\sum_jw_jC_j\Bigr]\le\tfrac32 Z .$$

The first part makes $Z^*_{CQP'}$ a lower bound on the optimum. The second is Lemma 2.8. Together they are Corollary 2.9 and the value guarantee of the $3/2$-approximation.

Milestones

In attack order:

• Lemma 2.2: $\mathbb E[C_j]=\sum_i(\Pr[j\mapsto i]p_{ij}+\sum_{k\prec_ij}\Pr[j,k\mapsto i]p_{ik})$ for any random assignment.
• Theorem 2.1: rounding a feasible $\bar a$ has expected value exactly $Z_{QP}(\bar a)$.
• Corollary 2.3: (IQP) and (QP) have the same optimum.
• The positive semidefiniteness of $D+\operatorname{diag}(c)$ and Lemma 2.4: $a\mapsto(1-\gamma)c^Ta+\tfrac12a^T(D+2\gamma\operatorname{diag}(c))a$ is convex for all instances iff $\gamma\ge\tfrac12$.
• The identity $Z_{QP}=Z_{CQP}+\tfrac12(c^Ta-a^T\operatorname{diag}(c)a)$ and Theorem 2.6 a), the factor $2$ for (CQP).
• Lemma 2.8, the integrality step of Theorem 2.10, and Corollary 2.11, the bound $(1+c^T\bar a/(2Z))Z$.

Significance

The result gives a $3/2$-approximation for $R\,|\,|\sum w_jC_j$ from a relaxation with only $mn$ variables, without time indexing, so its size does not depend on the processing times. The same convexification, adapted to time slots, yields the factor 2 with release dates (§3 of the paper). The equality of Theorem 2.1 makes the analysis exact: the loss of rounding is exactly the gap between $Z_{QP}$ and the convex objective. The relaxation also bounds the power of preemption (§4), and for identical machines it connects scheduling to Max-$k$-Cut (§6).

All these results are proved in the paper; none is known to be formalized. A formal development adds:

• a checked model of Smith-sequenced assignment schedules;
• the expectation calculus for pairwise independent rounding;
• the positive-semidefiniteness argument of Lemma 2.4;
• a precise statement of what the $3/2$ guarantee says when complexity is set aside.

Difficulty

Two steps resist the obvious approach.

Positive semidefiniteness. $D$ alone is indefinite: two jobs with unit data give the block $\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$. Positive semidefiniteness of $D+\operatorname{diag}(c)$ holds only because the jobs on each machine are ordered by Smith's ratio. A generic matrix argument that ignores this ordering fails, and the "only if" half of Lemma 2.4 needs a specific family of instances.

Exact expectations under pairwise independence. Theorem 2.1 is an equality that uses only the one- and two-job marginals. A proof that silently assumes full independence of the choices proves a different statement. A proof that drops the product condition on pairs is false: with correlated choices the expected value differs from $Z_{QP}$.

Formalization scope

Jobs and machines are Fin n and Fin m; vectors in $\mathbb R^{mn}$ are functions on Fin m × Fin n and $D$ is a Matrix over that type. The order $\prec_i$ is cross-multiplied ($w_jp_{ik}>w_kp_{ij}$, or equality and $j<k$), which equals the page's ratio definition because $p>0$.

Standing assumptions of p. 2 are hypotheses of every theorem: $p_{ij}>0$ and $w_j\ge0$. Hypotheses added relative to the page:

• Corollary 2.11 assumes $Z>0$, which its fraction presupposes;
• the integrality step of Theorem 2.10 assumes integral $p$ and $w$, as the page's proof does.

Optimum. The scheduling optimum $Z^*$ is the minimum of $\mathrm{val}$ over assignments, by Smith's rule (p. 7, cited by the paper, not reproved). "Within a factor $\alpha$ of the optimum" is stated as a bound against the value of every assignment, so no optimum is presupposed.

Rounding. Randomized rounding is any nonnegative weight $\mu$ of total mass 1 on assignments, with $\Pr_\mu[j\mapsto i]=\bar a_{ij}$ and $\Pr_\mu[j\mapsto i,\,k\mapsto h]=\bar a_{ij}\bar a_{hk}$ for $j\ne k$. The product weight satisfies this.

Not formalized. Polynomial running time, solvability of (CQP′) within additive error $\varepsilon$ (ellipsoid method), and derandomization by conditional probabilities. Theorem 2.10 is formalized as the existence of an outcome in the support of the rounding with the $3/2$ guarantee.

Trivializing formalization ruled out. A bound $\mathbb E\le\tfrac32Z$ for an arbitrary number $Z$ says nothing about schedules. The goal therefore also states that every schedule is feasible for (CQP′) at its own value, so $Z$ is a genuine lower bound on the optimum.

Contributions welcome. A complete development needs:

• linearity of expectation over a finite weight on assignments;
• the computation of Lemma 2.2;
• a positive-semidefiniteness criterion via principal minors or a direct sum-of-squares decomposition of $a^T(D+\operatorname{diag}(c))a$;
• convexity of quadratic forms with PSD matrices.

The rounding calculus and the PSD lemma are reusable for §§3–4 of the same paper. Alternative proofs of Lemma 2.4 are welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22(3), 1997. https://doi.org/10.1287/moor.22.3.513
• A. S. Schulz, M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM Journal on Discrete Mathematics 15(4), 2002. https://doi.org/10.1137/S0895480199357078
• N. Bansal, A. Srinivasan, O. Svensson, Lift-and-round to improve weighted completion time on unrelated machines, STOC 2016. https://doi.org/10.1145/2897518.2897572

Motivation

Semidefinite programs optimize a linear objective while requiring an affine matrix to be positive semidefinite. They include familiar linear and quadratic optimization models and arise in engineering and combinatorial optimization. Vandenberghe and Boyd's survey develops their duality theory and describes interior point methods that work with primal and dual matrices simultaneously. The question in this mission is quantitative: if a method lowers a particular potential by a fixed amount at each step, how quickly does its primal-dual objective gap shrink? Vandenberghe and Boyd, pp. 49, 76–77.

The paper uses the potential to combine two kinds of progress. One term records the size of the duality gap; another records how far the current matrices are from a central pair. Decreasing the gap alone does not ensure the matrices remain well positioned for the next step, so the potential accounts for both quantities. Theorem 5.1 turns a per-step decrease in this scalar into an explicit bound on the gap after $k$ steps. The theorem concerns any sequence meeting that decrease condition; it does not prescribe a particular search direction or step-selection algorithm. Vandenberghe and Boyd, pp. 76–77.

Setting

Fix a vector $c\in\mathbb R^m$ and symmetric real $n\times n$ matrices $F_0,F_1,\ldots,F_m$. For $x\in\mathbb R^m$, define the affine matrix

$$F(x)=F_0+\sum_{i=1}^{m}x_iF_i.$$

The primal problem minimizes $c^Tx$ subject to $F(x)\succeq0$. A dual-feasible matrix $Z$ satisfies $Z\succeq0$ and $\operatorname{Tr}(F_iZ)=c_i$ for every $i=1,\ldots,m$. Here $\succeq0$ means positive semidefinite; $\succ0$ means positive definite. The pair $(x,Z)$ is strictly feasible if both $F(x)\succ0$ and $Z\succ0$, with the dual equations still satisfied. Section 4 also assumes that $F_1,\ldots,F_m$ are linearly independent. Vandenberghe and Boyd, pp. 49, 63, 70.

For a feasible pair, the duality gap is the difference between the primal objective $c^Tx$ and the dual objective $-\operatorname{Tr}(F_0Z)$. Equation (32) identifies it as

$$\eta=c^Tx+\operatorname{Tr}(F_0Z)=\operatorname{Tr}(F(x)Z).$$

For a strictly feasible pair, define the deviation from centrality and the potential by

$$\psi(x,Z)=-\log\det(F(x)Z)+n\log\eta-n\log n,$$ $$\varphi(x,Z)=\nu\sqrt n\,\log\eta+\psi(x,Z),\qquad \nu\ge1.$$

The logarithm is natural. The matrix size $n$ determines the $\sqrt n$ factor; it is distinct from the number $m$ of decision variables. These are the explicit formulas on p. 76, where the paper also expresses $\psi$ through a central pair. Vandenberghe and Boyd, pp. 64, 75–76.

Formalization targets

The first milestones establish the gap identity, the expanded determinant formula for $\varphi$, and nonnegativity of $\psi$ with its stated equality condition. The final milestone bounds the gap by the potential:

$$\eta\le\exp\!\left(\frac{\varphi(x,Z)}{\nu\sqrt n}\right).$$

For the goal, let $(x^{(j)},Z^{(j)})$, $j=0,\ldots,k$, be strictly feasible pairs and suppose a fixed $\delta>0$ gives the decrease stated in equation (56) at every step $j<k$:

$$\varphi(x^{(j+1)},Z^{(j+1)})\le\varphi(x^{(j)},Z^{(j)})-\delta.$$

The goal theorem, Theorem 5.1, says that for $0<\varepsilon<1$ and

$$k\ge\frac{\nu\sqrt n\log(1/\varepsilon)+\psi(x^{(0)},Z^{(0)})}{\delta},$$

one has the boundary-correct gap estimate

$$\operatorname{Tr}(F(x^{(k)})Z^{(k)})\le\varepsilon\operatorname{Tr}(F(x^{(0)})Z^{(0)}).$$

The paper prints a strict inequality in the last display. Its stated non-strict threshold permits equality, as explained under Formalization scope. Vandenberghe and Boyd, p. 77, (56) and Theorem 5.1.

Significance

The theorem converts a local numerical guarantee into a global bound on an optimization certificate. Because the gap is the difference between primal and dual objectives, shrinking it gives a quantitative measure of progress toward optimality for every strictly feasible iterate. The expression records the dependence on matrix size, desired relative gap, starting deviation, and guaranteed potential decrease. It leaves the mechanism that achieves the decrease open, so different potential reduction methods can use the same conclusion. Vandenberghe and Boyd, pp. 64, 76–77.

The target here is a machine-checked statement and proof of this known 1996 result, together with its four supporting facts. The draft declarations compile as statements; their proofs remain open. A complete development would make the determinant, trace, positive-definiteness, and sequence reasoning reusable for other matrix optimization arguments. It would also record the boundary correction precisely rather than carrying forward a strict sign that fails at equality.

Difficulty

The substantive matrix claim is $\psi(x,Z)\ge0$. The product $F(x)Z$ need not be symmetric, even though both factors are positive definite, so directly applying a result about symmetric matrix eigenvalues to the product is not automatic. The nonnegativity and its equality case must respect the positivity and determinant conventions used by the explicit formula. The later exponential bound and iteration statement depend on those facts and on keeping each logarithm in its positive domain. Vandenberghe and Boyd, p. 76.

Formalization scope

Lean uses Fin m for the $m$ variable matrices, indexed from zero, with $F_0$ as a separate argument; Fin n indexes matrix rows and columns. Matrix.IsHermitian represents real symmetry. Matrix.PosSemidef and Matrix.PosDef represent the paper's matrix inequalities $\succeq0$ and $\succ0$, including symmetry. The matrix size satisfies $n\ge1$. Traces, determinants, natural logarithms, and $\sqrt n$ are the corresponding Mathlib operations. All statements involving $\psi$ or $\varphi$ require strict feasibility, so the real logarithm's default value on nonpositive inputs cannot decide a theorem. The paper's linearly independent $F_1,\ldots,F_m$ are an explicit hypothesis on the Section 4 and 5 statements. Vandenberghe and Boyd, pp. 49, 70, 76–77.

The definition of $\psi$ uses the explicit second formula on p. 76. The central pair in the preceding formula is not represented; its existence is introduced on p. 75 without a proof there. The p. 76 prose describes $\psi\ge0$ for feasible pairs, but its finite real logarithmic formula and the potential reduction iterates use strictly feasible pairs. The milestone states that domain explicitly. In Theorem 5.1 strict feasibility is assumed for the iterates $j=0,\ldots,k$ and equation (56) for the steps $j<k$ only, so the statement covers a method that stops after $k$ steps. The fixed $\delta$ is positive, and $\nu\ge1$ and $0<\varepsilon<1$ are explicit.

The paper's strict conclusion is false at its own inclusive threshold. Take $m=n=1$, $F_0=0$, $F_1=c=Z^{(j)}=1$, $x^{(j)}=e^{-j}$, $\nu=\delta=1$, and $\varepsilon=e^{-1}$. Then $\psi=0$, each decrease is exactly one, and at $k=1$ the gap equals $\varepsilon$ times its initial value. The goal therefore uses $\le$, the strongest statement valid at the printed threshold. This correction is recorded in the theorem's description and moderation notes. Vandenberghe and Boyd, p. 77, Theorem 5.1.

A complete proof needs Mathlib's matrix order, determinant and trace identities, logarithm and exponential facts, and an arithmetic-geometric mean statement for positive eigenvalues. Matrix lemmas and the deviation inequality are welcome contributions alongside the final sequence bound. The definitions preserve the paper's full potential and feasible domain; replacing $\psi$ by zero or dropping the $\sqrt n$ factor would change the target.

Selected references

• Lieven Vandenberghe and Stephen Boyd, Semidefinite Programming, SIAM Review 38(1), 49–95, 1996. DOI: 10.1137/1038003.

Motivation

Subgradient methods are the basic tool for minimizing a nonsmooth convex function when only a black-box oracle returning one subgradient per query is available. In the classical method the new subgradient enters the iterate with a weight that decreases over time, so information collected late is counted less than information collected early, and the method has no natural certificate of its own accuracy.

Yu. Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009) 221–259; first circulated as a CORE discussion paper, March 2002, revised September 2005) introduces Dual Averaging (DA): the method accumulates all past subgradients with nondecreasing weights in the dual space and maps the aggregate back to the feasible set through a strongly convex prox-function. One analysis, Theorem 1 of the paper, gives at once an upper bound on a primal-dual gap, a bound on the iterates that holds even on unbounded feasible sets, and a bound on the averaged subgradients. From it the paper derives rates for minimization over simple sets, problems with functional constraints, saddle points, variational inequalities, and stochastic optimization. Dual Averaging later became a standard method in online learning and regularized stochastic optimization (e.g. L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, JMLR 11 (2010)).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$, and $E^*$ its dual. The value of $s \in E^*$ at $x \in E$ is $\langle s, x\rangle$, and the dual norm is $\|s\|_* = \max\{\langle s, x\rangle : \|x\| \le 1\}$. Balls are $B_r(x) = \{y : \|y - x\| \le r\}$.

Let $Q \subseteq E$ be closed and convex. A prox-function of $Q$ is a function $d$, continuous on $Q$, that is strongly convex on $Q$ with convexity parameter $\sigma > 0$:

$$d(\alpha x + (1-\alpha)y) \le \alpha d(x) + (1-\alpha) d(y) - \tfrac12\sigma\alpha(1-\alpha)\|x - y\|^2, \qquad x, y \in Q,\ \alpha\in[0,1].$$

The prox-center $x_0 \in Q$ minimizes $d$ on $Q$, and $d(x_0) = 0$. Two examples: the Euclidean norm with $d(x) = \frac12\|x - x_0\|_2^2$, and the $\ell_1$ norm on the simplex with the entropy $d(x) = \ln n + \sum_i x^{(i)}\ln x^{(i)}$.

For $D \ge 0$ and $\beta > 0$ set $F_D = \{x \in Q : d(x) \le D\}$ and

$$\xi_D(s) = \max_{x\in F_D}\langle s, x - x_0\rangle, \qquad V_\beta(s) = \max_{x\in Q}\{\langle s, x - x_0\rangle - \beta d(x)\},$$

and let $\pi_\beta(s) = \arg\min_{x\in Q}\{-\langle s, x\rangle + \beta d(x)\}$.

Given sequences $x_i \in E$, $g_i \in E^*$, $\lambda_i$, write $S_k = \sum_{i=0}^k \lambda_i$, $s_{k+1} = \sum_{i=0}^k \lambda_i g_i$ ($s_0 = 0$), $\hat s_{k+1} = s_{k+1}/S_k$, the gap function

$$\delta_k(D) = \max_{x\in F_D}\sum_{i=0}^k \lambda_i\langle g_i, x_i - x\rangle,$$

and the upper gap function $\Delta_k(\beta, D) = \beta D + \sum_{i=0}^k \lambda_i\langle g_i, x_i - x_0\rangle + V_\beta(-s_{k+1})$.

The DA-scheme (2.14) starts at $x_0$ with $s_0 = 0$ and $\beta_0 > 0$; at step $k \ge 0$ it receives $g_k$ (the oracle answer at $x_k$), chooses $\lambda_k > 0$ and $\beta_{k+1} \ge \beta_k$, and sets

$$s_{k+1} = s_k + \lambda_k g_k, \qquad x_{k+1} = \pi_{\beta_{k+1}}(-s_{k+1}).$$

A point $x^* \in Q$ is a solution in the sense (2.8) if $\langle g_i, x_i - x^*\rangle \ge 0$ for all $i$.

Formalization targets

Goal: Theorem 1 (p. 9)

For every run of the DA-scheme, every $k \ge 0$ and every $D \ge 0$,

$$\delta_k(D) \le \Delta_k(\beta_{k+1}, D) \le \beta_{k+1} D + \frac{1}{2\sigma}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2;$$

if $x^*$ is a solution in the sense (2.8), then

$$\tfrac12\sigma\|x_{k+1} - x^*\|^2 \le d(x^*) + \frac{1}{2\sigma\beta_{k+1}}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2;$$

and if moreover $B_r(x^*) \subseteq F_D$ for some $r, D > 0$, then

$$\|\hat s_{k+1}\|_* \le \frac{1}{r S_k}\Big[\beta_{k+1}D + \frac{1}{2\sigma}\sum_{i=0}^k \frac{\lambda_i^2}{\beta_i}\|g_i\|_*^2\Big].$$

The theorem leaves the step sizes $\lambda_k$ and the parameters $\beta_k$ free; every rate in the paper is obtained by choosing them.

Milestones

In the order the proof uses them: Lemma 6 (unique minimizer of a strongly convex function, quadratic growth (9.5), p. 36); Lemma 1 (convexity, differentiability, $\nabla V_\beta(s) = \pi_\beta(s) - x_0$ and its $1/(\beta\sigma)$-Lipschitz continuity, p. 7); (2.5) $V_\beta(s+\delta) \le V_\beta(s) + \langle\delta, \nabla V_\beta(s)\rangle + \frac{1}{2\sigma\beta}\|\delta\|_*^2$; (2.6) $V_\beta(\delta) \le \frac{1}{2\sigma\beta}\|\delta\|_*^2$; (2.2) monotonicity of $V_\beta$ in $\beta$; Lemma 2 $\xi_D(s) \le \beta D + V_\beta(s)$ (p. 8); (2.11) the representation $\delta_k(D) = \sum_i\lambda_i\langle g_i, x_i - x_0\rangle + \xi_D(-s_{k+1})$; (2.13) $\delta_k(D) \le \Delta_k(\beta, D)$; and (2.18), the telescoped estimate along the scheme (p. 10).

Significance

Theorem 1 is the single estimate behind the whole paper. With $\beta_k$ growing like $\sqrt k$ it gives the $O(1/\sqrt k)$ rate of Dual Averaging for nonsmooth convex minimization with simple or weighted averages (Theorems 2 and 3), and through the gap $\delta_k(D)$ it gives primal-dual certificates for saddle-point problems and variational inequalities (§§3–5) and the stochastic version (§6, the companion mission). Part 2 is the reason the method can run on unbounded feasible sets: the iterates stay in a ball around any solution. Part 3 bounds the averaged subgradients, which yields approximate dual solutions.

The result is proved in the paper. As far as a search of Mathlib and the Prove2Me catalog shows (October 2026), none of its statements is machine-checked: Mathlib has strong convexity (StrongConvexOn) and Fréchet derivatives, but no prox-functions in an arbitrary norm, no Danskin-type differentiability of a maximum, and no analysis of Dual Averaging. A formalization produces these as reusable pieces: Lemma 6 in an arbitrary finite-dimensional norm, the smoothness of $V_\beta$ (a form of the duality between strong convexity and Lipschitz gradients of the conjugate), and the definitions of the scheme and its gap functions, on which the paper's §§3–6 can then be built.

Difficulty

The bookkeeping of the proof is short; the analytic content sits in Lemma 1 and Lemma 6. Lemma 1 asserts differentiability of a function defined as a maximum over a possibly unbounded set, in an arbitrary norm, where the gradient lives in $E^{**}$ and no inner product is available to identify it with a vector. The prox-function is only continuous and strongly convex, never assumed differentiable (footnote 2, p. 5), so first-order optimality conditions for $\pi_\beta$ are not available. Lemma 6's existence claim needs boundedness of the level sets of $d$ in finite dimension; the printed argument ends with "this contradicts continuity of $d$", which does not by itself close the argument, so a complete proof has to supply the missing step. Finally, (2.18) pairs a sum from $i = 0$ with a sum from $i = 1$ and depends on $x_0$ being the prox-center, so an off-by-one in the indices of the scheme changes the statement.

Formalization scope

$E$ is a finite-dimensional real normed space with an arbitrary norm; $E^*$ is StrongDual ℝ E with the operator norm, which is $\|\cdot\|_*$, and $\langle s, x\rangle$ is s x. No inner product is used, so the $\ell_1$/entropy example remains an instance. The prox-function is a real function on $E$ of which only its values on $Q$ are used, strongly convex in Mathlib's sense StrongConvexOn Q σ d (exactly (1.8)), with $\sigma > 0$ (the paper's "$\sigma \ge 0$" at (1.8) is corrected by its Definition 1). The maxima $\xi_D$, $V_\beta$, $\delta_k$ are real suprema, finite for $D \ge 0$, $\beta > 0$; every statement assumes these ranges, including Lemma 2 and (2.13), where the page writes $\beta \ge 0$ but $V_0$ is not defined. The argmin map $\pi$ is a hypothesis on a given map, not a construction, and the run of (2.14) starts at the prox-center and takes the oracle answers $g_k$ as free data. Indices start at $0$. Pages and equation numbers are those of the CORE discussion-paper version (September 2005) used as source, not the journal's pp. 221–259.

A trivializing formalization is ruled out: the run must set $x_{k+1}$ to the argmin point $\pi_{\beta_{k+1}}(-s_{k+1})$ and $\pi$ must carry its argmin property, without which the statements would be false, and the setting is satisfiable (E = ℝ, $Q = ℝ$, $d(x) = x^2/2$, $\sigma = 1$, $\pi_\beta(s) = s/\beta$), so the theorem is not vacuous.

Needed infrastructure: Lemma 6 in an arbitrary norm; a Danskin-type differentiability lemma for $V_\beta$; Lipschitz continuity of the argmin map; suprema manipulations for $\xi_D$, $V_\beta$, $\delta_k$ under boundedness. Contributions of any of the milestones, of general lemmas on strongly convex functions in normed spaces, and of the remaining parts of Theorem 1 are welcome.

Selected references

• Yu. Nesterov, Primal-dual subgradient methods for convex problems, Math. Program. 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
• L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, J. Mach. Learn. Res. 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
• Yu. Nesterov, Smooth minimization of non-smooth functions, Math. Program. 103 (2005) 127–152. https://doi.org/10.1007/s10107-004-0552-5

Motivation

The proximal point algorithm replaces a hard optimization or equilibrium problem by a sequence of better-conditioned ones: from the current point $x^n$ it solves the original problem with a quadratic penalty $\|x-x^n\|^2$ added, and takes the solution as $x^{n+1}$. The method is a building block of modern convex optimization. Augmented Lagrangian methods, Douglas–Rachford and ADMM splitting, and many bundle methods are proximal point iterations applied to suitable problems (Rockafellar 1976; Eckstein–Bertsekas 1992).

The algorithm was introduced by B. Martinet in a five-page note in the Revue française d'informatique et de recherche opérationnelle in 1970 (Martinet 1970). The note treats three cases: monotone variational inequalities on a bounded convex set (§II), convex–concave min–max problems (§III), and convex minimization (§IV). This mission formalizes §IV.

Timeline.

• 1970, Martinet: the regularization (13) for convex minimization over a closed convex set in a Hilbert space; Théorème 3 (weak cluster points are minimizers, the sequence is minimizing), stated without proof.
• 1976, Rockafellar (SIAM J. Control Optim. 14): the proximal point algorithm for maximal monotone operators, with inexact steps and weak convergence of the whole sequence when a zero exists.
• 1991, Güler (SIAM J. Control Optim. 29): the rate $f(x^n)-\inf f = O(1/n)$ for convex minimization, and an example in which the iterates converge weakly but not strongly.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C\subseteq H$ be a nonempty, closed, convex set, and let $f:H\to\mathbb R$ be a convex, lower semicontinuous function such that, for every $a\in\mathbb R$, the sublevel set $\{x\in C \mid f(x)\le a\}$ is bounded. These are the standing hypotheses of §4.1 (Lean: Standing f C). The problem is

$$(12)\qquad \min\,\{\,f(x)\mid x\in C\,\},$$

and its solution set (solSet f C) is the set of $\bar x\in C$ with $f(\bar x)\le f(x)$ for all $x\in C$.

The regularization algorithm (13) starts from $x^0\in C$ and, given $x^n$, takes

$$(13)\qquad x^{n+1}\in C\ \text{ the minimizer of } \ f(x)+\|x-x^n\|^2\ \text{ over } x\in C .$$

Lean encodes one step as IsProxStep f C xn y ($y\in C$ and $f(y)+\|y-x^n\|^2\le f(x)+\|x-x^n\|^2$ for all $x\in C$) and a run as IsProxSeq f C x.

A point $\tilde x$ is a weak cluster point of $(x^n)$ (IsWeakClusterPt) if every neighbourhood of $\tilde x$ in the weak topology of $H$ contains $x^n$ for infinitely many $n$. A sequence is minimizing if $f(x^n)\to\inf_{x\in C} f(x)$.

Formalization targets

Existence for (12) and well-posedness of (13)

$$\exists\,\bar x\in C\ \ \forall x\in C:\ f(\bar x)\le f(x), \qquad \forall x^n\in C\ \ \exists!\,y\in C:\ y \text{ minimizes } f(x)+\|x-x^n\|^2 \text{ over } C .$$

These are the paper's claims in §4.1 ("Ces hypothèses assurent l'existence d'une solution pour (12)") and §4.2 ("solution unique").

Goal: Théorème 3

For every sequence generated by (13),

$$\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in \operatorname{sol}(12), \qquad \lim_{n\to\infty} f(x^n)=\inf_{x\in C} f(x)\in\mathbb R .$$

The goal asserts no rate and no constant. It is the statement the paper makes, with both conclusions in one theorem.

Stronger: Remarque 1

If in addition $f$ is uniformly convex, i.e. $f(ax+by)\le af(x)+bf(y)-ab\,\varphi(\|x-y\|)$ for $a,b\ge0$, $a+b=1$, with $\varphi(t)>0$ for $t>0$, then (12) has a unique solution $\bar x$ and $\|x^n-\bar x\|\to0$.

Significance

The result. Théorème 3 says that the proximal iterates make progress on the objective, not only on the distance to the solution set. A user of the method can stop on a value criterion. The convergence also needs no step-size tuning, no smoothness of $f$, and no bound on $f$ beyond the boundedness of the sublevel sets. The well-posedness of (13) is what makes the method an algorithm. Each step is a strongly convex subproblem with a unique solution, and later inexact and splitting variants rely on that.

Formalizing it. The note gives no proof of Théorème 3 ("On peut faire une démonstration directe de ce théorème") and none of Remarque 1. The mission asks for a complete machine-checked proof of the convex minimization case of the original proximal point paper. To our knowledge, none of these statements has a machine-checked proof. Mathlib has convexity, lower semicontinuity, the weak topology of a normed space and uniform convexity of functions, but no proximal point algorithm.

Difficulty

Each iterate $x^{n+1}$ is defined only implicitly, as the minimizer of a problem that changes with $n$. Monotonicity of $f(x^n)$ follows at once from comparing $x^{n+1}$ with $x^n$. Monotonicity alone gives convergence of $f(x^n)$ to some limit, but not to $\inf_C f$. Closing that gap needs information about the minimizers of (12) and their distance to the iterates.

The cluster-point statement is about the weak topology. A norm-continuity argument does not apply: $f$ is only lower semicontinuous in norm, and passing to weak limits requires the weak lower semicontinuity of convex lower semicontinuous functions. The boundedness that makes weak cluster points exist comes from the sublevel-set hypothesis, not from $C$, which may be unbounded.

For Remarque 1, the obvious argument controls $\varphi(\|x^n-\bar x\|)$, and the hypothesis on $\varphi$ is only positivity. Passing from $\varphi(\|x^n-\bar x\|)\to0$ to $\|x^n-\bar x\|\to0$ is not immediate without a monotone modulus.

Formalization scope

All statements live in MartinetReg.ConvexMin. The conventions the formalization commits to:

• $H$ is a real complete inner product space (InnerProductSpace ℝ H, CompleteSpace H). The paper says "espace de Hilbert", and its inequalities make it real.
• $C\neq\emptyset$ is a standing hypothesis. The paper leaves it implicit, but its existence claim for (12) is false for $C=\emptyset$.
• $f$ is real-valued, convex and lower semicontinuous on all of $H$, as printed. The constraint $x\in C$ stays explicit in (12) and (13). It is not absorbed into an extended-valued indicator.
• The penalty in (13) has weight $1$, as printed, not $\tfrac12$.
• The algorithm is a relation on sequences: IsProxSeq accepts any sequence with $x^0\in C$ satisfying (13) at every step. Existence and uniqueness of the step are a separate milestone, not built into a definition by choice.
• "Minimisante" is stated as: some real $m$ is the greatest lower bound of $f(C)$ and $f(x^n)\to m$. This avoids the junk value sInf takes on sets unbounded below. As a side effect, the theorem asserts that $f$ is bounded below on $C$.
• Weak cluster points are cluster points in WeakSpace ℝ H. A norm cluster point would weaken the conclusion and is not used.
• Remarque 1 uses Mathlib's UniformConvexOn Set.univ φ f with $\varphi(t)>0$ for $t>0$. It keeps every hypothesis of §4.1.

The goal does not assume that (12) has a solution, that $f$ is bounded below on $C$, or that the iterates are bounded. Each of these would remove part of the content of Théorème 3, and the first two are consequences proved as milestones.

Not formalized here: Remarque 2 (p. 158), a comment that convexity seems indispensable; and the Exemple (p. 158). The Exemple's linear system $(A^*A+2I)x^{n+1}=A^*b+2x^n$ corresponds to $f=\tfrac12\|Ax-b\|^2$. For the printed $f=\|Ax-b\|^2$, (13) gives $(A^*A+I)x^{n+1}=A^*b+x^n$. The variational inequality case (§II) is the companion mission I of this series.

Reusable beyond this mission: the existence of minimizers of convex lower semicontinuous functions with bounded sublevel sets on closed convex subsets of a Hilbert space, and the weak lower semicontinuity it rests on. Contributions of these general lemmas, and of strong-convexity facts for $x\mapsto f(x)+\|x-x^n\|^2$, are welcome.

Selected references

• B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3), 154–158, 1970. https://doi.org/10.1051/m2an/197004R301541
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14(5), 877–898, 1976. https://doi.org/10.1137/0314056
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29(2), 403–419, 1991. https://doi.org/10.1137/0329022
• J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Mathematical Programming 55, 293–318, 1992. https://doi.org/10.1007/BF01581204
• J. L. Lions and G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20, 493–519, 1967. https://doi.org/10.1002/cpa.3160200302

Why Euclidean distortion matters

Many algorithms for graphs and finite metric spaces begin by placing the points in a geometric space and then working with the geometry. Euclidean space is the most convenient target: distances there are controlled by inner products, so the question "where should the points go?" becomes a question about matrices. Linial, London and Rabinovich (Combinatorica 15 (1995)) made this viewpoint systematic and drew algorithmic consequences from it, among them the approximate multicommodity max-flow/min-cut theorem treated in a companion mission.

A finite metric space rarely embeds in Euclidean space without changing some distances. The natural measure of the damage is the distortion, and the least distortion $c_2(X)$ of a space $X$ is a basic invariant in metric geometry and in the analysis of approximation algorithms. Section 3.1 of the paper (pp. 221–225) shows that $c_2(X)$ is the value of a semidefinite program, so that it can be approximated in polynomial time, and Corollary 3.5 turns the dual of that program into a complete list of certificates that bound $c_2(X)$ from below.

Timeline. The isometric case ($c=1$) is classical: Schoenberg (1935) and Young–Householder (1938) characterised the finite metric spaces that embed isometrically in Euclidean space by positive semidefiniteness of an associated matrix; the paper cites this as its Remark 3.7. Bourgain (1985) proved that every $n$-point metric space embeds in Euclidean space with distortion $O(\log n)$. Linial, London and Rabinovich (1995) gave the semidefinite characterisation of $c_2(X)$ for every $c$ (Corollary 3.5) and showed that the $O(\log n)$ bound is tight for constant-degree expanders.

Setting

Let $X$ be a finite set of $n$ points and $d : X\times X\to\mathbb{R}$ a semi-metric: $d \ge 0$, $d(x,x)=0$, $d$ is symmetric and satisfies the triangle inequality. Distinct points may be at distance zero, as the paper allows. Write $d_{i,j}=d(i,j)$.

For $c \ge 1$, the space $(X,d)$ embeds in a Euclidean space with distortion at most $c$ if there are $m\in\mathbb{N}$ and $\varphi : X\to\mathbb{R}^m$ with

$$\|\varphi(x)-\varphi(y)\| \le d(x,y) \le c\,\|\varphi(x)-\varphi(y)\| \qquad (x,y\in X),$$

where $\|\cdot\|$ is the Euclidean norm (Definition 2.1, p. 218). The Lean predicate is EmbedsEuclidean d c.

$PSD = PSD_n$ is the cone of real symmetric positive semidefinite matrices indexed by $X$. For a matrix $Q=(q_{i,j})$, the condition $Q\cdot\vec 1=\vec 0$ says that every row of $Q$ sums to zero. The trace pairing of two matrices is $\sum_{i,j} p_{i,j}y_{i,j}$.

Formalization targets

Goal: Corollary 3.5 (p. 224)

For a finite semi-metric space $(X,d)$ and $c\ge 1$, $(X,d)$ embeds in a Euclidean space with distortion at most $c$ if and only if for every $Q\in PSD$ with $Q\cdot\vec 1=\vec 0$

$$\sum_{q_{i,j}>0} q_{i,j}\,d_{i,j}^2 + c^2\sum_{q_{i,j}<0} q_{i,j}\,d_{i,j}^2 \le 0 .$$

The sums run over ordered pairs. The statement is exact: distortion at most $c$ is attained, not approached.

Milestones, in the order the proof uses them

1. Gram reformulation (proof of Corollary 3.5, first display, p. 224; cf. p. 221): an embedding with distortion at most $c$ exists iff some $A\in PSD$ satisfies $d_{i,j}^2 \le a_{i,i}+a_{j,j}-2a_{i,j} \le c^2 d_{i,j}^2$ for all $i,j$.
2. Proposition 3.6 (p. 224): a symmetric matrix $P$ lies in $PSD$ iff $\sum_{i,j}p_{i,j}y_{i,j}\ge 0$ for every $Y\in PSD$.
3. Duality step (pp. 224–225): no such $A$ exists iff some $Q\in PSD$ together with a nonnegative combination of the inequalities $J_{i,j} : c^2d_{i,j}^2 \ge a_{i,i}+a_{j,j}-2a_{i,j} \ge d_{i,j}^2$ yields a contradiction, every $a$-term cancelling and a negative constant remaining.

Significance

The result. Corollary 3.5 makes the least Euclidean distortion a dual object: every positive semidefinite $Q$ with zero row sums is a certificate that $c_2(X) \ge \big(\sum_{q>0} q\,d^2 / \sum_{q<0}|q|\,d^2\big)^{1/2}$, and the corollary says that the best such certificate is exact. Lower bounds on distortion in later work, for expanders, hypercubes and other families, are proved by exhibiting such a $Q$, often a graph Laplacian. The same duality is the basis of the semidefinite relaxations used for sparsest cut and related problems.

Formalizing it. The result is proved in the literature, but nothing of it is machine-checked. A formal development produces three reusable pieces: the Gram-matrix description of Euclidean point configurations up to distortion, self-duality of the positive semidefinite cone under the trace pairing (not in Mathlib), and a theorem of alternatives for a specific semidefinite feasibility problem, where no constraint qualification can be assumed for free.

Difficulty

The direction from an embedding to the inequalities is short. The difficulty is the converse. "By convex programming duality" is not automatic for semidefinite systems: theorems of alternatives for cone programs can fail when the image of the cone under the relevant linear map is not closed, so the step that turns "no feasible $A$" into an explicit certificate $Q$ needs an argument specific to this system. A second subtlety is that the left side asks for an embedding with distortion exactly at most $c$; a separation argument that only produces embeddings with distortion $c+\varepsilon$ for every $\varepsilon>0$ does not prove the statement.

Formalization scope

• Points are an arbitrary finite type X (Fintype, DecidableEq); $n=|X|$ is not otherwise used. The semi-metric is a function d : X → X → ℝ with the axioms bundled in IsPseudometric.
• The target space is EuclideanSpace ℝ (Fin m) with m existentially quantified. Distortion is the contractive form of Definition 2.1 with both inequalities; with only one of them the zero map or a large scaling would make every space embed, so that reading is ruled out.
• $PSD$ is Matrix.PosSemidef (symmetric by definition); $Q\cdot\vec1=\vec0$ is Q.mulVec (fun _ => 1) = 0. Both hypotheses on $Q$ are needed: without zero row sums the all-ones matrix, and without semidefiniteness $J - nI$, would violate the inequality for every space with two points at positive distance.
• The paper's hypothesis $c\ge 1$ is kept.
• Proposition 3.6 adds the hypothesis that $P$ is symmetric, implicit in "belongs to $PSD_n$".
• The duality step is stated as an explicit theorem of alternatives: an identity of linear forms in $A$ plus a negative constant.
• Out of scope. The corollary's second sentence ("this inequality holds … with $c=O(\log n)$") rests on Bourgain's theorem, which the paper only cites; it is not stated. The algorithmic content of Theorem 3.2 (polynomial-time approximation of $c_2(X)$ by the ellipsoid method, dimension reduction) is not stated. Remark 3.7 and Corollary 3.8 are not stated.

Proofs of any milestone, alternative proofs of the goal, and reusable lemmas on the positive semidefinite cone are welcome.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2) (1995) 215–245. https://doi.org/10.1007/BF01200757
• J. Bourgain, On Lipschitz embedding of finite metric spaces in Hilbert space, Israel J. Math. 52 (1985) 46–52. https://doi.org/10.1007/BF02776078
• I. J. Schoenberg, Remarks to Maurice Fréchet's article "Sur la définition axiomatique d'une classe d'espaces distanciés vectoriellement applicables sur l'espace de Hilbert", Annals of Math. 36 (1935) 724–732. https://doi.org/10.2307/1968654
• G. Young, A. S. Householder, Discussion of a set of points in terms of their mutual distances, Psychometrika 3 (1938) 19–22. https://doi.org/10.1007/BF02287916

Motivation

The method of multipliers (augmented Lagrangian method) of Hestenes and Powell is one of the standard algorithms for constrained convex optimization. Each iteration minimizes the Lagrangian plus a quadratic penalty on the constraint residual, then updates the multiplier estimate. Rockafellar showed in 1976 that this method is the proximal point algorithm applied to the dual problem (Rockafellar, Math. Oper. Res. 1976), which explains its global convergence for convex programs without differentiability or constraint qualifications on the primal side.

The quadratic penalty is not the only one used in practice. Exponential and other nonquadratic penalties produce twice-differentiable augmented Lagrangians and were studied by Kort and Bertsekas and by Tseng and Bertsekas. Eckstein (Math. Oper. Res. 18(1), 1993, 202–226) gave a uniform convergence theory for such methods. He replaces the squared Euclidean distance in the proximal point algorithm by the D-function of a Bregman function $h$, proves convergence of the resulting algorithm for every maximal monotone operator (Theorem 1), and then derives nonquadratic multiplier methods by applying it to the dual of a convex program. This mission covers the linear-equality-constrained case, §4.1 and Theorem 6 of that paper.

Setting

Let $f : \mathbb R^n \to (-\infty, +\infty]$ be convex and lower semicontinuous, let $A$ be an $m \times n$ matrix, $b \in \mathbb R^m$, and $X \subseteq \mathbb R^n$ closed and convex, with $\inf\{f(x) \mid x \in X\} < \infty$. The problem is

$$\text{minimize } f(x) \quad\text{such that}\quad Ax = b,\ x \in X. \tag{7}$$

Write $\delta_X$ for the indicator function of $X$ ($0$ on $X$, $+\infty$ off $X$) and $f_X = f + \delta_X$. The dual functional is

$$d(p) = \inf_{x \in X}\bigl\{ f(x) + \langle p, Ax - b\rangle \bigr\}, \qquad p \in \mathbb R^m,$$

assumed not identically $-\infty$. An optimal multiplier (Lagrange multiplier) is a maximizer of $d$ over $\mathbb R^m$.

For an open set $S$, a Bregman function with zone $S$ is a function $h : \bar S \to \mathbb R$ that is continuously differentiable on $S$, strictly convex and continuous on $\bar S$, and satisfies the level-set and limit conditions (iv)–(vi) of Definition 1 on its D-function $D_h(x, y) = h(x) - h(y) - \langle \nabla h(y), x - y \rangle$. Here the zone is all of $\mathbb R^m$, and $\nabla h$ is assumed onto $\mathbb R^m$. Let $h^*(z) = \sup_p\{\langle p, z\rangle - h(p)\}$ be the convex conjugate of $h$, and let $c_k > 0$ with $\inf_k c_k > 0$. The nonquadratic method of multipliers generates $\{(x^k, p^k)\}$ by

$$x^{k+1} \in \operatorname*{arg\,min}_{x \in X}\Bigl\{ f(x) + \tfrac{1}{c_k}\, h^*\bigl(\nabla h(p^k) + c_k(Ax - b)\bigr)\Bigr\}, \qquad p^{k+1} = \nabla h^*\bigl(\nabla h(p^k) + c_k(Ax^{k+1} - b)\bigr). \tag{9}$$

For $h(p) = \frac12\|p\|^2$ this is the classical method of multipliers. A run of the general Bregman proximal point algorithm for an operator $T$ is a sequence with $\frac{1}{c_k}(\nabla h(x^k) - \nabla h(x^{k+1})) \in T(x^{k+1})$ for all $k$.

Formalization targets

Goal: Theorem 6 (pp. 212–213)

Under the assumptions above:

$$\exists\, p^\star \text{ optimal} \;\Longrightarrow\; p^k \to \text{some optimal multiplier, and every limit point of } \{x^k\} \text{ solves (7)};$$ $$\nexists\, p^\star \text{ optimal} \;\Longrightarrow\; \{p^k\} \text{ is unbounded}.$$

The statement fixes no penalty: it holds for every Bregman function with zone $\mathbb R^m$ and surjective gradient. It makes no claim that $\{x^k\}$ converges, which is false in general.

Milestones

1. Theorem 1 (pp. 206–207): for a maximal monotone $T$ and a Bregman function $h$ with zone $S$, $\bar S \supseteq \operatorname{dom} T$, a run of the Bregman proximal point algorithm converges to a zero of $T$ when one exists, under either (C1) $S \supseteq \overline{\operatorname{dom} T}$ or (C2) $T = \partial f$ for a closed proper convex $f$. If $T$ has no zero and (C1) holds, the run is unbounded.
2. Proof of Theorem 6, p. 213: the multipliers produced by (9) form a Bregman proximal point run on $\partial(-d)$,

$$p^{k+1} = \bigl(\nabla h + c_k \partial(-d)\bigr)^{-1}\bigl(\nabla h(p^k)\bigr).$$

3. Proof of Theorem 6, p. 214: if $p^k \to p^\star$ with $p^\star$ optimal, then $Ax^k \to b$, and every limit point $x^\infty$ of $\{x^k\}$ satisfies $Ax^\infty = b$, $-A^{\mathsf T}p^\star \in \partial f_X(x^\infty)$, and solves (7).

An additional item states the existence clause of Theorem 6: if the row space of $A$ meets $\operatorname{ri}(\operatorname{im} \partial(f + \delta_X))$, or $f$ and $X$ are polyhedral and the row space meets $\operatorname{im} \partial(f + \delta_X)$, then (9) has an infinite run from every starting point $(x^0, p^0)$.

Significance

Theorem 6 gives global convergence of a whole family of augmented Lagrangian methods at once, with the penalty chosen through $h$. For instance, Example 5 of the paper obtains the method with penalty $\frac{1}{r c_k}\sum_i |\mu_i + c_k(A_i x - b_i)|^r$ for any $r > 1$. Its multiplier sequence behaves exactly as the dual proximal point iterates do, and it detects dual unsolvability through divergence of $\{p^k\}$. Primal limit points are optimal without any assumption beyond existence of a Lagrange multiplier.

The result has a published proof (Eckstein 1993) but, to our knowledge, no machine-checked proof. Formalizing it requires a formal treatment of Bregman functions and of the Bregman proximal point algorithm (Theorem 1). It also requires the subdifferential calculus of the dual functional: conjugates, the chain rule $\partial(g \circ A^{\mathsf T})$, and the inverse relation between $\nabla h$ and $\nabla h^*$. The milestones isolate the reduction of (9) to Theorem 1 and the primal recovery argument, each of which can be proved independently of the others.

Difficulty

The reduction step is where a direct argument fails. Showing that $p^{k+1}$ is a proximal point of $\partial(-d)$ needs the inclusion $-(Ax^{k+1} - b) \in \partial(-d)(p^{k+1})$, where $-d(p) = (f_X)^*(-A^{\mathsf T}p) + \langle b, p\rangle$ is a composition of a conjugate with a linear map. The subdifferential chain rule holds with equality only under a qualification condition. The argument must therefore use only the inclusion that holds unconditionally, together with the optimality condition for the $x$-subproblem, which needs differentiability of $h^*$ everywhere (supplied by $\operatorname{im} \nabla h = \mathbb R^m$ and strict convexity of $h$). On the primal side, $\{x^k\}$ need not be bounded or convergent, so primal optimality can only be asserted for limit points, through closedness of the graph of $\partial f_X$. Theorem 1 itself rests on the Bregman conditions (iv)–(vi), which replace the Fejér monotonicity of the Euclidean proximal point argument.

Formalization scope

• $\mathbb R^k$ is EuclideanSpace ℝ (Fin k). $A$ is a continuous linear map $\mathbb R^n \to \mathbb R^m$ (equivalent to an $m \times n$ matrix), and $A^{\mathsf T}$ is its adjoint. Theorem 1 is stated on any finite-dimensional real inner product space.
• Functions into $(-\infty, +\infty]$ are EReal-valued with "never $-\infty$" as a hypothesis. $\partial f$ uses the published IsSubgradient; convexity is convexity of the epigraph (IsConvexFn). Maximal monotonicity, dom and zer are the published ThreeOpSplitting.Convergence definitions. The conjugate $h^*$ is the published fenchelConjugate, an EReal supremum.
• (9) uses the real value of $h^*$. This is faithful because $\operatorname{im}\nabla h = \mathbb R^m$ makes $h^*$ finite everywhere. Finiteness of $h^*$ is a consequence, never a hypothesis. The arg min in (9) is a minimality predicate, not a choice function, since the minimizer need not be unique.
• Recursion (3) is encoded through its equivalent form (4). Condition (vi) of Definition 1 is stated on the natural domain $\bar S \times S$ of $D_h$.
• "Limit point" means subsequential limit, and "unbounded" means the range of the sequence is not bounded. In the existence clause, ri is Mathlib's intrinsicInterior, and polyhedral sets and functions are finite intersections of closed half-spaces (for functions, of the epigraph).
• The paper's typo "monontone" in Theorem 1 is read as "monotone".
• The convergence claims must not be weakened to their trivial instances. A formalization that assumes $\{x^k\}$ converges, or adds finiteness of $h^*$ or boundedness of $\{p^k\}$ as a hypothesis, or encodes (9) with a choice function, does not state Theorem 6.
• Reusable beyond this mission: the Bregman function structure and Theorem 1 (shared with the other missions of this series), and the dual-functional and conjugate facts for linearly constrained programs. Contributions toward the conjugate calculus ($\nabla h^* = (\nabla h)^{-1}$, the chain rule inclusion) are welcome.

Selected references

• J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1) (1993) 202–226. https://doi.org/10.1287/moor.18.1.202
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2) (1976) 97–116. https://doi.org/10.1287/moor.1.2.97
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• Y. Censor, S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3) (1992) 451–464. https://doi.org/10.1007/BF00940051
• P. Tseng, D. P. Bertsekas, On the convergence of the exponential multiplier method for convex programming, Mathematical Programming 60 (1993) 1–19. https://doi.org/10.1007/BF01580598