Linear algebra

Motivation

Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of $\mathrm{PG}(r-1,q^t)$ of rank $rt/2$ is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.

Timeline.

• 2000, Blokhuis–Lavrauw: the rank of a scattered $\mathbb F_q$-linear set of $\mathrm{PG}(r-1,q^t)$ is at most $rt/2$, and for $r$ even this bound is attained.
• 2000, Ball–Blokhuis–Lavrauw: examples of rank $6$ in $\mathrm{PG}(2,q^4)$.
• Classical: for $r=3$, $t=2$ the bound $3$ is attained by Baer subplanes.
• 2000, Blokhuis–Lavrauw, Thm 4.4: existence (without explicit examples) for $r>3$, $t=2$, $q=2$ and for $r\ge3$, $(t-1)\mid r$, $t$ even, $q>2$.
• 2015, Bartoli, Giulietti, Marino and Polverino (arXiv:1512.07467v1, Combinatorica 37 (2017)): three explicit families in $\mathrm{PG}(2,q^{2n})$ and, by direct sums, maximum scattered linear sets in $\mathrm{PG}(r-1,q^t)$ for $t$ even in three families of $(q,t)$. This mission formalizes that result; the companion mission formalizes the paper's application to complete caps.

Setting

Let $q$ be a prime power, $t\ge1$, and let $V$ be an $r$-dimensional vector space over $\mathbb F_{q^t}$; $\mathrm{PG}(V,\mathbb F_{q^t})=\mathrm{PG}(r-1,q^t)$ has as points the spans $\langle v\rangle_{\mathbb F_{q^t}}$ of nonzero $v\in V$. An $\mathbb F_q$-subspace $U\subseteq V$ is a subset closed under addition and under multiplication by $\mathbb F_q$. It defines the $\mathbb F_q$-linear set

$$L_U=\{\langle u\rangle_{\mathbb F_{q^t}} : u\in U\setminus\{0\}\},$$

whose rank is $\dim_{\mathbb F_q}U$. A linear set comes paired with $U$, so every statement here is about $U$. The weight of a point $\langle v\rangle$ is $\dim_{\mathbb F_q}(\langle v\rangle_{\mathbb F_{q^t}}\cap U)$, and $L_U$ is scattered when every point of $L_U$ has weight $1$; equivalently, for every nonzero $u\in U$,

$$\lambda\in\mathbb F_{q^t},\ \lambda u\in U\ \Longrightarrow\ \lambda\in\mathbb F_q .$$

The plane construction (§2). Fix $n\ge2$ and the field $E=\mathbb F_{q^{6n}}$ with its subfields $\mathbb F_q\subseteq\mathbb F_{q^n}\subseteq\mathbb F_{q^{2n}}$ and $\mathbb F_{q^{3n}}$. As an $\mathbb F_{q^{2n}}$-space $E$ has dimension $3$, so $\mathrm{PG}(E,\mathbb F_{q^{2n}})=\mathrm{PG}(2,q^{2n})$. For $\omega\in\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$ and an $\mathbb F_q$-linear $f:\mathbb F_{q^{3n}}\to\mathbb F_{q^{3n}}$ the paper studies

$$U_f=\{f(x)+x\omega : x\in\mathbb F_{q^{3n}}\},$$

with $f$ a monomial $ax^{q^i}$ or a binomial $f_{i,a,b}(x)=ax^{q^i}+bx^{q^{2n+i}}$. The relative norms $N_{q^m/q^d}(x)=\prod_{j<m/d}x^{q^{dj}}$ enter the hypotheses.

Formalization targets

Goal: Theorem 1.2 (p. 3)

For $t$ even and $r\ge2$, in each of the cases (a) $q=2$, $t\ge4$; (b) $t\not\equiv0\pmod3$; (c) $q\equiv1\pmod3$, $t\equiv0\pmod3$,

$$\exists\,U\subseteq\mathbb F_{q^t}^{\,r}\ \ \mathbb F_q\text{-subspace}:\qquad \dim_{\mathbb F_q}U=\frac{rt}{2},\quad L_U\ \text{scattered}.$$

Milestones, in proof order

• Proposition 2.1 (p. 5): $U_f$ has rank $3n$, and $L_{U_f}$ is scattered iff $Q_f\cap\mathbb F_{q^{2n}}=\mathbb F_q$, where $Q_f$ is the set of quotients $\frac{f(x)+x\omega}{f(y)+y\omega}$, $y\ne0$.
• Proposition 2.2 (p. 6): the same criterion through the polynomial system (5)–(6).
• Theorems 2.3, 2.4 (pp. 7, 9): the monomial families, for $n\not\equiv0\pmod 3$ and for $q\equiv1\pmod3$.
• Theorem 2.5 (p. 10): existence in $\mathrm{PG}(2,q^{2n})$ in those two regimes.
• Lemma 2.6 (p. 11): $\varphi(x)/x$ and $\bar\varphi(x)/x$ have the same image, where $\bar\varphi$ is the trace adjoint.
• Proposition 2.7, Lemma 2.8, Proposition 2.9, Theorem 2.10 (pp. 12–16): the binomial family for $q=2$.
• Theorem 3.1 (p. 16): direct sums of scattered linear sets are scattered, of rank $rt/2$ iff each summand has rank $s_it/2$.
• The line example (p. 2, cited from Lavrauw's thesis) and the Baer-subplane case $r=3$, $t=2$ (p. 3).

Significance

Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many $(q,t)$ with $r$ odd, a regime where earlier existence results covered only a few values of $t$. The $q=2$ case feeds the paper's second main result: scattered $\mathbb F_2$-linear sets of $\mathrm{PG}(2,2^t)$ of rank $3t/2$ are translation caps, from which complete caps of size $2\sqrt{q^{\,n-1}}$ in $\mathrm{AG}(n,q)$ are built.

All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between $\mathbb F_q$-dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.

Difficulty

The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific $f$. For the monomials this rests on the solvability of $z^{q^i-1}=c$ in $\mathbb F_{q^{3n}}$, a norm condition interacting with the gcd hypotheses. For the binomial with $q=2$, the existence of a suitable $b$ (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound $\dim U\le st/2$ for scattered $U$ to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking $U=\mathbb F_q^{\,r}$ or any small subspace, is scattered but has the wrong rank; the content is in the rank $rt/2$.

Formalization scope

• Citation basis. arXiv:1512.07467v1; page numbers equal PDF pages.
• Fields. $\mathbb F_{q^m}\subseteq E$ is the fixed field of $x\mapsto x^{q^m}$ in a finite field $E$ of characteristic $p$ with $|E|=q^{6n}$, $q=p^h$. Norms and traces are explicit Frobenius products and sums.
• Subspaces and rank. An $\mathbb F_q$-subspace is a carrier set with closure conditions. Rank $k$ is $|U|=q^k$; in Theorem 3.1 rank $rt/2$ is $|W|^2=q^{rt}$.
• Points. Scatteredness takes the spanning field as an argument: $\mathbb F_{q^{2n}}$ in §2, the whole $\mathbb F_{q^t}$ in Theorem 1.2 and §3. $\mathrm{PG}(r-1,q^t)$ is modelled on Fin r → K; the plane of §2 on $E$ itself.
• Pinned readings.
  • Theorem 1.2 prints no range for $r$. The preceding sentence and the proof (p. 17) say $r\ge5$, and $r=1$ is false. The goal assumes $r\ge2$, covered by the line example ($r=2$), §2 with the Baer case ($r=3$) and Theorem 3.1 ($r\ge4$).
  • $\omega$ is quantified over all of $\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$.
  • The index ranges $1\le i\le3n-1$ (monomial) and $2n+i\le3n-1$ (binomial) come from the case headings on pp. 7 and 10.
  • Proposition 2.7's printed "$wx$" is $\omega x$.
  • Theorem 2.10 keeps its printed hypothesis $N_{2^{3n}/2^n}(b)\ne1$.
  • Theorem 3.1's rank clause assumes $t\ge2$; for $t=1$ it is false.
• Ruled out. Taking the span over $E$ or over $\mathbb F_q$, or dropping the rank, would make the statements false or trivial; every existence statement fixes the rank, and the span field is explicit.
• Contributions welcome. Frobenius-fixed-field cardinalities, norm surjectivity, the criteria of Propositions 2.1–2.2, the monomial and binomial families, and the direct-sum rank computation.

Selected references

• D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, arXiv:1512.07467v1 (2015); Combinatorica 37 (2017). https://arxiv.org/abs/1512.07467, https://doi.org/10.1007/s00493-016-3531-6
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
• O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2010.04.007
• S. Ball, A. Blokhuis, M. Lavrauw, Linear (q + 1)-fold blocking sets in PG(2, q⁴), Finite Fields Appl. 6 (2000), 294–301.
• M. Lavrauw, Scattered Spaces with respect to Spreads and Eggs in Finite Projective Spaces, Ph.D. thesis, TU Eindhoven, 2001.
• G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82.

Motivation

For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form $\mathbf x^\top A\mathbf x$ on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form $\mathcal A(\mathbf x,\mathbf x,\mathbf x)$ on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.

Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$. A set of vertices is stable if no two of its members are adjacent; the stability number $\alpha(G)$ is the size of a largest stable set, so $1\le\alpha(G)\le v$.

Put $n=v+v(v-1)/2$ and write a vector of $\mathbb R^n$ as $\mathbf z=(\mathbf x,\mathbf y)$, with $\mathbf x=(x_1,\dots,x_v)$ indexed by vertices and $\mathbf y=(y_{ij})_{i<j}$ indexed by pairs of vertices. The tensor $\mathcal S_G=[\![s_{abc}]\!]\in\mathbb R^{n\times n\times n}$ has entry $1$ at the six orderings of the triple of coordinates $(x_i,x_j,y_{ij})$ for every non-adjacent pair $i<j$, and $0$ elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.

For a real 3-tensor $\mathcal A=[\![a_{abc}]\!]$ the cubic form is $\mathcal A(\mathbf z,\mathbf z,\mathbf z)=\sum_{a,b,c}a_{abc}z_az_bz_c$, and a real $\lambda$ is a unit $\ell^2$-eigenvalue of $\mathcal A$ if

$$\sum_{a,b}a_{abc}z_az_b=\lambda z_c\quad\text{for all }c,\qquad\text{for some }\mathbf z\text{ with }\|\mathbf z\|_2=1 .$$

Finally, $\lambda_l=2\sqrt{\tfrac23\left(1-\tfrac1l\right)}$ for $l\ge1$. In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and $\alpha(G)$ is Mathlib's SimpleGraph.indepNum.

Formalization targets

Goal: Theorem 9.3, core

$$\alpha(G)=\max\{\,l\in\{1,\dots,v\}:\ \lambda_l\text{ is a unit }\ell^2\text{-eigenvalue of }\mathcal S_G\,\}.$$

That is, $\lambda_{\alpha(G)}$ is an eigenvalue of $\mathcal S_G$, and no $\lambda_l$ with $\alpha(G)<l\le v$ is. This is the statement on which the paper's $v$-query reduction rests; nothing is claimed about $l<\alpha(G)$.

Milestones, in the paper's order

1. Theorem 9.2 (Nesterov). With $\mathbb S^{n-1}=\{(\mathbf x,\mathbf y):\|\mathbf x\|_2^2+\|\mathbf y\|_2^2=1\}$,

$$\sqrt{1-\frac1{\alpha(G)}}=3\sqrt{\frac32}\cdot\max_{(\mathbf x,\mathbf y)\in\mathbb S^{n-1}}\ \sum_{i<j,\ \{i,j\}\notin E}x_ix_jy_{ij}.$$

2. The tensor. $\mathcal S_G$ is symmetric and $\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=6\sum_{i<j,\{i,j\}\notin E}x_ix_jy_{ij}$.
3. The maximum is an eigenvalue. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)$ is attained and is a unit $\ell^2$-eigenvalue of $\mathcal S_G$.
4. Its value. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=\lambda_{\alpha(G)}$.
5. Further result: Theorem 6.9 (Banach), (23). For every symmetric $\mathcal S\in\mathbb R^{n\times n\times n}$,

$$\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}=\sup_{\mathbf x\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf x,\mathbf x)|}{\|\mathbf x\|_2^3},$$

both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.

Significance

The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.

Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor $1/\sqrt2$ (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.

Difficulty

The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing $\mathbf x$ and maximizing over $\mathbf y$ by Cauchy–Schwarz, reduces the cubic problem to a quartic one in $\mathbf x$, whose value still has to be identified with $\alpha(G)$; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of $\mathcal S_G$ is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.

Formalization scope

• Tensors and indices. A 3-tensor is a function ι → ι → ι → ℝ on a finite index type. For $\mathcal S_G$ the index type is the disjoint union of the vertices Fin v and the pairs $\{(i,j): i<j\}$; this is $\mathbb R^n$ with coordinates labelled by name instead of by the paper's enumeration $\varphi(i,j)=(i-1)v-i(i-1)/2+j-i$. Vertices are $0,\dots,v-1$.
• Normalization. Eigenvalues are taken with a unit eigenvector. The paper's Problem 9.1 and Definition 5.1 say only $\mathbf x\ne\mathbf 0$; since $(\lambda,\mathbf x)\mapsto(t\lambda,t\mathbf x)$ preserves the eigen-equation, that reading would make every nonzero real an eigenvalue of $\mathcal S_G$ and the goal false. The unit sphere (13) is where the paper derives the notion.
• Explicit readings. The paper's index range "$1\le i<j<k\le v$" in the definition of $s_{ijk}$ is read as $k\le n$ (taken literally it gives $\mathcal S_G=0$). Every "max" is stated as a greatest element, so attainment is claimed. In (23) the suprema are real suprema over nonzero vectors with boundedness part of the conclusion. $v\ge1$ is assumed wherever the paper uses $\alpha(G)\in\{1,\dots,v\}$.
• Not formalized. The oracle procedure of the proof of Theorem 9.3, the polynomial size of $\mathcal S_G$, the input model of Problem 9.1 with quadratic irrationalities (Remark 9.4), and the NP-completeness of the stability number (Karp 1972, via $\alpha(G)=\omega(\overline G)$). The goal is the mathematical core of the Turing reduction, not a complexity statement.
• Trivializations ruled out. Without the unit normalization the eigenvalue statements are trivial or false; a goal stating only (a), or only an inequality between the maximum and $\lambda_{\alpha(G)}$, would not determine $\alpha(G)$; both are excluded by the statements above.
• Infrastructure. Everything rests on Mathlib (SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5: https://arxiv.org/abs/0911.1393)
• Yu. Nesterov, Random walk in a simplex and quadratic optimization over convex polytopes, CORE Discussion Paper 2003/71, 2003. http://edoc.bib.ucl.ac.be:83/archive/00000238/01/dp2003-71.pdf
• E. de Klerk, The complexity of optimizing over a simplex, hypercube or sphere: a short survey, Central European Journal of Operations Research 16, 111–125, 2008. https://doi.org/10.1007/s10100-007-0052-9
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian Journal of Mathematics 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in ($L^2$), Studia Mathematica 7(1), 36–44, 1938 (reference [Banach 1938] of Hillar–Lim).
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 1, 129–132, 2005. https://arxiv.org/abs/math/0607648
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40, 1302–1324, 2005. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).

The proof is a reduction from the clique number $\omega(G)$ of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses $\omega(G)$ as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding $\omega(G)\ge l$ is one of Karp's (1972) NP-complete problems.

Setting

A real 3-tensor is an array $\mathcal A=[\![a_{ijk}]\!]\in\mathbb R^{l\times m\times n}$ with trilinear form $\mathcal A(\mathbf x,\mathbf y,\mathbf z)=\sum_{i,j,k}a_{ijk}x_iy_jz_k$. With the Euclidean norm $\|\cdot\|_2$, its spectral norm is

$$\|\mathcal A\|_{2,2,2}=\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal A(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}.$$

A real $\sigma$ is a unit $\ell^2$-singular value of $\mathcal A$ if there are unit vectors $\mathbf u,\mathbf v,\mathbf w$ with

$$\textstyle\sum_{j,k}a_{ijk}v_jw_k=\sigma u_i,\quad \sum_{i,k}a_{ijk}u_iw_k=\sigma v_j,\quad \sum_{i,j}a_{ijk}u_iv_j=\sigma w_k$$

for all $i,j,k$: the stationarity conditions of $\mathcal A(\mathbf u,\mathbf v,\mathbf w)$ on a product of unit spheres.

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$, with $e$ edges $\{i_k,j_k\}$, $k=1,\dots,e$, and clique number $\omega$. Let $\Delta_v$ be the standard simplex, $A_G$ the adjacency matrix and $J$ the all-ones matrix. For a positive integer $l$ set $Q_l=A_G+\frac1lJ$ and $M_l=\max_{\mathbf x\in\Delta_v}\mathbf x^\top Q_l\mathbf x$. Let $E_k=\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$, and let $T_l$ be the maximum over unit $\mathbf u,\mathbf v\in\mathbb R^v$, $\mathbf w\in\mathbb R^{l+2e}$ of the multilinear form

$$\sum_{i=1}^l\Big(\mathbf u^\top\tfrac1lI\mathbf v\Big)w_i+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{l+k}+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{e+l+k}. \tag{26}$$

The graph tensor $\mathcal A_l\in\mathbb Q^{v\times v\times(l+2e)}$ has as entry $a_{ijk}$ the coefficient of $u_iv_jw_k$ in (26).

Formalization targets

Goal: Theorems 6.5 and 1.10, encoding-free core

For every graph $G$ on $v\ge1$ vertices and every enumeration of its edges:

$$\forall l\ge1:\ \|\mathcal A_l\|_{2,2,2}=1\iff l=\omega;\qquad 1\text{ is a unit singular value of }\mathcal A_\omega;\qquad \forall l>\omega:\ 1\text{ is not one of }\mathcal A_l,$$

so $\omega$ is the largest $l\in\{1,\dots,v\}$ for which $1$ is a unit singular value of $\mathcal A_l$. The paper's $v$-query Turing reductions rest on exactly this.

Milestones (in attack order)

1. Theorem 6.7 (Motzkin–Straus): $1-1/\omega=2\max_{\mathbf x\in\Delta_v}\sum_{\{i,j\}\in E}x_ix_j$.
2. (22): $M_l=1+\frac{\omega-l}{l\omega}$; so $M_\omega=1$, $M_l>1$ for $l<\omega$, $M_l<1$ for $l>\omega$.
3. Lemma 6.8: $M_l=N_l$, where $N_l=\max_{\|\mathbf u\|_2=1}\{\sum_{i=1}^l(\mathbf u^\top\frac1lI\mathbf u)^2+2\sum_k(\mathbf u^\top E_k\mathbf u)^2\}$.
4. Theorem 6.9 (Banach), (24): for a symmetric 4-tensor, $\|\mathcal S\|_{2,2,2,2}=\sup_{\mathbf x\neq\mathbf 0}|\mathcal S(\mathbf x,\mathbf x,\mathbf x,\mathbf x)|/\|\mathbf x\|_2^4$.
5. Proposition 6.10 (He–Li–Zhang): for symmetric $A_k$, $\max_{\|\mathbf u\|=\|\mathbf v\|=1}\sum_k(\mathbf u^\top A_k\mathbf v)^2=\max_{\|\mathbf v\|=1}\sum_k(\mathbf v^\top A_k\mathbf v)^2$.
6. Lemma 6.11: $T_l=M_l^{1/2}$, hence $T_l=1$ iff $l=\omega$, $T_l>1$ iff $l<\omega$, $T_l<1$ iff $l>\omega$.
7. Proof of Theorem 6.5: $\|\mathcal A_l\|_{2,2,2}=T_l$, $T_l$ is a unit singular value of $\mathcal A_l$, and every unit singular value has absolute value at most $T_l$.
8. §7 (content of Theorem 1.13): $\min_{\sigma\ge0,\ \text{unit }\mathbf u,\mathbf v,\mathbf w}\|\mathcal A-\sigma\,\mathbf u\otimes\mathbf v\otimes\mathbf w\|_F^2=\|\mathcal A\|_F^2-\|\mathcal A\|_{2,2,2}^2$, attained only with $\sigma=\|\mathcal A\|_{2,2,2}$.

Significance

The result. The goal shows that a single comparison with $1$ of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size $v\times v\times(l+2e)$ encodes whether $l=\omega(G)$. It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.

Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.

Difficulty

The construction of $\mathcal A_l$ is explicit, and the comparison with $1$ is arithmetic once $T_l=M_l^{1/2}$ is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.

Formalization scope

Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with $v\ge1$, clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. $\mathcal A_l$ is a rational tensor, read over $\mathbb R$ by casting.

Explicit readings of the paper:

• Definition 6.1 has no norm constraint. Since $(\sigma,\mathbf u,\mathbf v,\mathbf w)\mapsto(t\sigma,t\mathbf u,t\mathbf v,t\mathbf w)$ preserves (20), unnormalized singular values make every nonzero real a singular value of $\mathcal A_l$, so the clause "not for $l>\omega$" would be false. Singular vectors are therefore unit vectors, as in the paper's derivation on p. 0:21.
• The statement of Lemma 6.11 prints $w_{m+l+k}$. There is no $m$ in §6, and the proof uses $w_{e+l+k}$, which is formalized.
• $E_k$ is written entrywise as $\frac12[\{i,j\}=\{i_k,j_k\}]$, which equals $\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ for a loopless edge.
• "$T_l$ is just the maximum $\ell^2$-singular value of $\mathcal A_l$" is made explicit as milestone 7.
• The goal does not claim that $1$ fails to be a singular value of $\mathcal A_l$ for $l<\omega$; the paper neither claims nor uses this.

This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of $\mathcal A_l$, the $v$-query procedure, the scaling to a general fixed $0\ne\sigma\in\mathbb Q$, and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.

Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.

Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (final version arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393v5)
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian J. Math. 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in (L²), Studia Math. 7, 36–44, 1938. https://doi.org/10.4064/sm-7-1-36-44
• S. He, Z. Li, S. Zhang, Approximation algorithms for homogeneous polynomial optimization with quadratic constraints, Math. Program. Ser. B 125(2), 353–383, 2010. https://doi.org/10.1007/s10107-010-0409-z
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.

Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.

Timeline:

• 2002, Ahlswede–Winter: matrix Laplace transform method; matrix Chernoff bound for i.i.d. summands via Golden–Thompson.
• 2010, Oliveira: a variant of the Laplace transform method used in Proposition 3.1 of the paper.
• 2010–2012, Tropp: master tail bound via Lieb's theorem (Theorem 3.6), and Theorem 5.1 / Corollary 5.2 for independent, non-identical psd summands.

Setting

All matrices are $d\times d$ complex matrices with $d\ge1$. For a self-adjoint (Hermitian) matrix $A$, $\lambda_{\max}(A)$ and $\lambda_{\min}(A)$ are its algebraically largest and smallest eigenvalues. The semidefinite order $A\preccurlyeq B$ means that $B-A$ is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if $A = Q\Lambda Q^*$ then $f(A) = Qf(\Lambda)Q^*$; this gives the matrix exponential $e^A$ and, on positive-definite matrices, the matrix logarithm $\log A$.

A random matrix is a measurable map $X:\Omega\to\mathbb C^{d\times d}$ on a probability space $(\Omega,\mathcal F,\mathbb P)$, and its expectation $\mathbb E X$ is taken entrywise. The matrix moment generating function of $X$ is $\theta\mapsto\mathbb E\,e^{\theta X}$.

The objects of the mission are independent random Hermitian matrices $X_1,\dots,X_n$ that are almost surely psd contractions: $X_k\succcurlyeq0$ and $\lambda_{\max}(X_k)\le1$. Their average expectation has extreme eigenvalues

$$\bar\mu_{\min} = \lambda_{\min}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),\qquad \bar\mu_{\max}=\lambda_{\max}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),$$

and the binary information divergence is

$$\mathrm D(a\,\|\,u) = a(\log a-\log u)+(1-a)(\log(1-a)-\log(1-u)),\qquad a,u\in[0,1].$$

In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.

Formalization targets

Goal: Theorem 5.1 (Matrix Chernoff I)

$$\mathbb P\Big\{\lambda_{\min}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\le\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\min})}\quad(0\le\alpha\le\bar\mu_{\min}),$$ $$\mathbb P\Big\{\lambda_{\max}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\ge\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\max})}\quad(\bar\mu_{\max}\le\alpha\le1).$$

Milestones

1. Theorem 3.6 (master tail bound): for every $\theta>0$ at which the mgfs exist, $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le e^{-\theta t}\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$.
2. Corollary 3.9: the same with the mgfs under one logarithm, $d\cdot\exp(-\theta t+n\log\lambda_{\max}(\frac1n\sum_k\mathbb E\,e^{\theta X_k}))$.
3. Lemma 5.8 (Chernoff mgf): $\mathbb E\,e^{\theta X}\preccurlyeq\mathbf I+(e^\theta-1)\mathbb E X$ for a random psd contraction $X$.
4. Display (5.1): $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le d\exp(-\theta t+n\log(1+(e^\theta-1)\bar\mu_{\max}))$.
5. Display (5.2): $\mathbb P\{\lambda_{\min}(\sum_kX_k)\le t\}\le d\exp(\theta t+n\log(1-(1-e^{-\theta})\bar\mu_{\min}))$.

Further statement

Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with $\lambda_{\max}(X_k)\le R$, $\mu_{\min},\mu_{\max}$ the extreme eigenvalues of $\sum_k\mathbb E X_k$,

$$\mathbb P\{\lambda_{\min}(\textstyle\sum_kX_k)\le(1-\delta)\mu_{\min}\}\le d\Big[\tfrac{e^{-\delta}}{(1-\delta)^{1-\delta}}\Big]^{\mu_{\min}/R},\quad \mathbb P\{\lambda_{\max}(\textstyle\sum_kX_k)\ge(1+\delta)\mu_{\max}\}\le d\Big[\tfrac{e^{\delta}}{(1+\delta)^{1+\delta}}\Big]^{\mu_{\max}/R}.$$

Significance

Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor $d$, which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound $\mathbb E\lambda_{\max}(\sum_kX_k)\le C\max\{\mu_{\max},R\log d\}$.

The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.

Difficulty

The scalar Chernoff argument uses $\mathbb E\,e^{\theta(X+Y)}=\mathbb E\,e^{\theta X}\,\mathbb E\,e^{\theta Y}$ for independent $X,Y$. For matrices $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. $\lambda_{\max}$, $\lambda_{\min}$ are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "$\lambda_{\max}\le1$" hold almost surely. The sequence has $n\ge1$ terms wherever an average $1/n$ appears. An infimum over $\theta>0$ is stated as a bound for every admissible $\theta>0$; integrability of $e^{\theta X_k}$ is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean $\log 0=0$, so at the boundary values $\bar\mu\in\{0,1\}$ the divergence is finite where the paper's is $+\infty$; this only weakens the stated bound.

A formalization in which $d=0$ (empty spectrum, $\lambda_{\max}=0$) or $n=0$ (the average $1/0=0$) were allowed, or in which the range of $\alpha$ were dropped, would state a different, partly false theorem; these cases are excluded.

A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in $\theta$. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede, A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821

Motivation

A spectral sparsifier of a weighted graph $G$ is a graph $\widetilde G$ on the same vertices, with few edges, whose Laplacian quadratic form is within a factor $\sigma$ of that of $G$ on every vector. Spielman and Teng introduced the notion in their work on nearly-linear-time solvers for symmetric diagonally dominant linear systems (Spielman–Teng 2004; arXiv:0808.4134): a sparsifier can replace a dense graph as a preconditioner, and it preserves every cut value up to the same factor, strengthening the cut sparsifiers of Benczúr and Karger (BK96).

Their construction first handles graphs whose edge weights lie in a bounded range. Arbitrary weights need an extra idea, which §10.2 of Spectral Sparsification of Graphs formalizes as Lemma 10.2 (Pullback): when a graph's vertex classes are held together by edges far heavier than those between them, one may contract each class to a single vertex, sparsify the much smaller contracted graph, and pull the result back to the original vertices. The approximation factor degrades only by $(1+1/c)^2$, where $c$ measures the gap between heavy and light weights. The same contraction idea goes back to Benczúr and Karger's treatment of weighted cut sparsifiers.

Setting

A weighted graph $G=(V,E,w)$ on a finite set $V$, $n=|V|$, is a symmetric function $w:V\times V\to\mathbb R_{\ge 0}$ with $w(v,v)=0$; its edges are the pairs with $w(u,v)\ne 0$. Its Laplacian quadratic form is

$$x^TL_Gx=\sum_{(u,v)\in E}w(u,v)\,(x(u)-x(v))^2,\qquad x\in\mathbb R^V .$$

A graph $\widetilde G$ is a $\sigma$-approximation of $G$ if $\frac1\sigma x^TL_{\widetilde G}x\le x^TL_Gx\le\sigma\, x^TL_{\widetilde G}x$ for all $x$. We write $G\preccurlyeq G'$ when $x^TL_Gx\le x^TL_{G'}x$ for all $x$, $G+G'$ for the graph whose weights are the sums, and $(u,v)$ for the single edge $\{u,v\}$ of weight $1$.

Let $V_1,\dots,V_k$ be a partition of $V$ with map $\pi:V\to\{1,\dots,k\}$. Write $E_0=\partial(V_1,\dots,V_k)$ for the edges between different parts, $E_1=E-E_0$, and $G_0=(V,E_0,w)$, $G_1=(V,E_1,w)$. The contraction of $G$ under $\pi$ is the graph $H$ on $\{1,\dots,k\}$ with weight $z(i,j)=\sum_{\pi(u)=i,\,\pi(v)=j}w(u,v)$ for $i\ne j$ and no self-loops. Given a graph $\widetilde H$ on $\{1,\dots,k\}$, a graph $\widetilde G$ on $V$ is a pullback of $\widetilde H$ under $\pi$ if every edge of $\widetilde G$ joins different parts, $\widetilde H$ is the contraction of $\widetilde G$, and for every edge $(i,j)$ of $\widetilde H$ exactly one edge $(u,v)$ of $\widetilde G$ has $\pi(u)=i$, $\pi(v)=j$. A pullback thus has as many edges as $\widetilde H$.

Formalization targets

Goal: Lemma 10.2 (Pullback), pp. 36–37

Let $0\le\epsilon<1/2$, $c\ge3$, let $\widetilde H$ be a $(1+\epsilon)$-approximation of the contraction of $G_0$ under $\pi$, and let $\widetilde G_0$ be a pullback of $\widetilde H$. Assume (1) each $V_i$ is connected by edges in $E_1$, (2) every edge in $E_1$ has weight at least $c^2n^3$, (3) every edge in $E_0$ has weight $1$. Then

$$\widetilde G_0+G_1\ \text{ is an }\ \alpha\text{-approximation of } G,\qquad \alpha=(1+\epsilon)\Big(1+\frac1c\Big)^2 .$$

Milestones (proof of Lemma 10.2, pp. 37–38)

Choose representatives $v_i\in V_i$; let $F$, $\widetilde F$ be the copies of $H$, $\widetilde H$ on $\{v_1,\dots,v_k\}$, and $I=F+G_1$, $\widetilde I=\widetilde F+G_1$.

• Lemma 10.3 (path inequality): for a path from $u$ to $v$ with edge weights $w_1,\dots,w_k>0$, $(u,v)\preccurlyeq(1/w_1+\dots+1/w_k)F$.
• (20), (21): for $a,b$ in different parts and $f$ the unit edge between $v_{\pi(a)},v_{\pi(b)}$,

$$(a,b)\preccurlyeq\Big(1+\frac1c\Big)\Big(f+\frac{1}{cn^2}G_1\Big),\qquad f\preccurlyeq\Big(1+\frac1c\Big)\Big((a,b)+\frac{1}{cn^2}G_1\Big).$$

• Summed bound: $G_0\preccurlyeq(1+1/c)\,[F+\tfrac1{2c}G_1]$.
• Claim (a): $I$ is a $(1+1/c)$-approximation of $G$.
• Claim (b): $\widetilde I$ is a $(1+\epsilon)$-approximation of $I$.
• Claim (c): $\widetilde I$ is a $(1+1/c)$-approximation of $\widetilde G_0+G_1$.

The constants are the paper's; the goal is the lemma as printed.

Significance

Lemma 10.2 is the reduction from arbitrary weights to bounded weights in Spielman and Teng's sparsification algorithm (Sparsify, §10.2): the edges of each weight scale are sparsified on a graph in which all much heavier edges have been contracted, so the number of vertices handled at each scale stays small, and the total size of the sparsifier is only a logarithmic factor larger than in the bounded-weight case. The statement itself is purely about quadratic forms and holds for any approximation $\widetilde H$ of the contraction, however it was obtained; it applies equally to later sparsification methods such as sampling by effective resistances.

The lemma is proved in the paper. As far as is known, none of these statements has a machine-checked proof: Mathlib has the Laplacian of a simple graph (SimpleGraph.lapMatrix) but no weighted Laplacian order, no contraction of weighted graphs and no notion of spectral approximation. The mission produces those objects and a complete formal proof of the lemma and its intermediate claims.

Difficulty

The individual steps are elementary, but the proof combines three kinds of bookkeeping. Lemma 10.3 is a Cauchy–Schwarz inequality along a path, which must be applied to a path assembled from two walks inside parts and one edge between representatives; obtaining a simple path of length at most $n$ from the connectivity hypothesis requires shortening walks. The summed bounds require recognising that the copies of the unit edges between representatives add up exactly to $F$, which uses hypothesis 3 and the fact that contraction counts each edge between two parts once. Claim (c) needs, in addition, that the total weight of $\widetilde F$ is at most $(1+\epsilon)$ times that of $F$ and that each pullback edge has the weight of its image edge. The constants are tight in one place: $(1+1/c)(1+\epsilon)\le 2$ requires both $c\ge3$ and $\epsilon\le 1/2$.

A natural shortcut, comparing $\widetilde G_0$ with $G_0$ directly, fails: $\widetilde G_0$ and $G_0$ have different edges, and their Laplacians are only comparable through the heavy intra-part edges.

Formalization scope

A weighted graph is a function w : V → V → ℝ on a Fintype V with IsWGraph w (symmetric, nonnegative, zero diagonal); sums and scalar multiples are pointwise. lapForm w x is $\frac12\sum_{u,v}w(u,v)(x(u)-x(v))^2$, IsApprox σ w̃ w keeps both inequalities of the definition, and GraphLE is $\preccurlyeq$. The partition is a surjective map π : V → Fin k (nonempty parts). $G_0$, $G_1$ are crossPart w π, intraPart w π; hypothesis 1 is reachability, between any two vertices of the same part, in the simple graph of $E_1$-edges. Representatives are any r : Fin k → V with π (r i) = i, and liftAlong r z places a graph on Fin k on them; the goal does not mention representatives. $n$ is Fintype.card V.

Two hypotheses implicit in the paper are explicit: $\epsilon\ge0$ (with $\epsilon<0$ the lemma is false), and that every edge of a pullback joins two different parts (contraction cannot see an edge inside a part, so without this a pullback could carry an arbitrary heavy edge and the lemma would be false). In Lemma 10.3 the edge weights are positive and the path has at least one edge.

A trivializing formalization is ruled out: dropping hypothesis 2 or 3, allowing $\epsilon<0$ or intra-part pullback edges, or letting the pullback forget the uniqueness of the edge over each $(i,j)$ makes the statement false or weaker, and stating only one of the two inequalities of $\sigma$-approximation is a different theorem. Every statement here keeps both.

The algorithm Sparsify and its analysis (Lemma 10.4, Theorem 10.5, Proposition 10.6, Theorem 10.7, Lemmas 10.8–10.9) and all running-time claims are out of scope. The weighted Laplacian form, its additivity and nonnegativity, and the transport of a quadratic form along an injective vertex map are reusable beyond this mission; contributions of such general lemmas, and a proof of Lemma 10.3 by Cauchy–Schwarz, are welcome.

Selected references

• D. A. Spielman, S.-H. Teng, Spectral Sparsification of Graphs, arXiv:0808.4134v3, 2010; SIAM J. Comput. 40(4), 2011. https://arxiv.org/abs/0808.4134
• D. A. Spielman, S.-H. Teng, Nearly-Linear Time Algorithms for Graph Partitioning, Graph Sparsification, and Solving Linear Systems, STOC 2004. https://arxiv.org/abs/cs/0310051
• A. A. Benczúr, D. R. Karger, Approximating s-t Minimum Cuts in Õ(n²) Time, STOC 1996; Randomized Approximation Schemes for Cuts and Flows in Capacitated Graphs, arXiv:cs/0207078. https://arxiv.org/abs/cs/0207078
• P. Diaconis, D. Stroock, Geometric Bounds for Eigenvalues of Markov Chains, Ann. Appl. Probab. 1(1), 1991. https://doi.org/10.1214/aoap/1177005980

Motivation

Minimizing the sum of the $k$ largest eigenvalues of a symmetric matrix that depends affinely on parameters is a basic problem of eigenvalue optimization (survey: A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 1996, doi:10.1017/S0962492900002646). Its objective is convex, and $f_k$ is differentiable at $B$ exactly when $\lambda_k(B)>\lambda_{k+1}(B)$; at optimal solutions the eigenvalues tend to coalesce, which makes the problem a model problem of nonsmooth optimization. G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues (Math. Oper. Res. 23(2), 1998, doi:10.1287/moor.23.2.339), gives a quantitative explanation in terms of the number of free parameters.

The paper also proves a bound on the rank of extreme points of semidefinite programs, now often called the Pataki bound (also obtained by Barvinok, 1995): an extreme point $X$ of $\{X\succeq0: A_i\bullet X=b_i,\ i\le m\}$ satisfies $\operatorname{rank}X(\operatorname{rank}X+1)/2\le m$. This bound is used throughout low-rank semidefinite optimization, for instance in the Burer–Monteiro approach.

Setting

$\mathcal S^n$ is the space of real symmetric $n\times n$ matrices, $X\succeq0$ means $X$ is symmetric positive semidefinite, and $A\bullet B=\sum_{i,j}a_{ij}b_{ij}$. For $B\in\mathcal S^n$, $\lambda_1(B)\ge\dots\ge\lambda_n(B)$ are its eigenvalues and, for $k\in\{1,\dots,n\}$,

$$f_k(B)=\lambda_1(B)+\dots+\lambda_k(B).$$

The multiplicity $\operatorname{mult}(\lambda_i(B))$ is the largest $p\ge1$ with $\lambda_j(B)=\dots=\lambda_{j+p-1}(B)$ for some $j\le i\le j+p-1$.

A face of a convex set $S$ is a convex $F\subseteq S$ such that $x\in F$, $y,z\in S$, $x=\tfrac12(y+z)$ imply $y,z\in F$; an extreme point is a one-point face; $\dim S$ is the maximal number of affinely independent points of $S$, minus one. Write $t(i)=i(i+1)/2$ and

$$\tau(l,r,s)=\max\{\,i+j:\ t(i)+t(j)\le l,\ i\le r,\ j\le s\,\}.$$

Let $A_0,A_1,\dots,A_m\in\mathcal S^n$ be linearly independent, $A(x)=A_0+\sum_{i=1}^mx_iA_i$, and assume $m\ge1$ and $k<n$ (the standing assumptions of §4). The affine eigenvalue problem is

$$(EV_k)\qquad\min\{f_k(A(x)):\ x\in\mathbb R^m\},$$

and $\Theta$ denotes its set of optimal solutions, a closed convex set. For $B\in\mathcal S^n$ the semidefinite program

$$\min\ kz+I\bullet V\quad\text{s.t.}\quad V,W\succeq0,\quad zI+V-W=B \tag{3.14}$$

has optimal value $f_k(B)$; $\Omega_k(B)$ is its set of optimal solutions $(z,V,W)$.

Formalization targets

Goal: Theorem 4.3

If $x^*$ is an extreme point of $\Theta$ and $m>k(n-k)$, then

$$\lambda_k(A(x^*))=\lambda_{k+1}(A(x^*))\qquad\text{and}\qquad \operatorname{mult}(\lambda_k(A(x^*)))\ \ge\ n-\tau\big(t(n)-m-1,\,k-1,\,n-k-1\big).$$

Milestones

1. Theorem 2.1: on a face $F$ of the primal feasible set, $t(\operatorname{rank}X)\le m+\dim F$; on a face $G$ of the dual feasible set, $t(\operatorname{rank}Z)\le t(n)-m+\dim G$.
2. Theorem 2.2: the multi-block version $\sum_jt(\operatorname{rank}X_j)\le m-q+\dim G$ for programs with $p$ semidefinite blocks and $q$ free variables.
3. Lemmas 3.1, 3.2 and Theorem 3.3: the optimal value of (3.14) and an explicit description of $\Omega_k(B)$ through an eigendecomposition $B=Q\operatorname{Diag}(\lambda)Q^T$.
4. The rank identity of §3: $\operatorname{rank}V+\operatorname{rank}W+\operatorname{mult}(\lambda_k(B))=n$ on $\Omega_k(B)$ when $\lambda_k(B)=\lambda_{k+1}(B)$.
5. Lemma 4.2 and (4.31): $\{x^*\}\times\Omega_k(A(x^*))$ is a face of the feasible set of the lifted SDP (4.26), of dimension $1$ or $0$ according as $\lambda_k>\lambda_{k+1}$ or $\lambda_k=\lambda_{k+1}$.
6. Lemma 4.1: $\Theta$ contains no line, so it has extreme points whenever it is nonempty.

Significance

The theorem says that once the number of free parameters $m$ exceeds $k(n-k)$, the $k$-th and $(k+1)$-st eigenvalues necessarily coincide at extreme optimal solutions, so $f_k\circ A$ is typically nonsmooth at its minimizers, and it bounds from below the dimension of the subdifferential $\partial f_k(A(x^*))$, which is $t(\operatorname{mult}(\lambda_k))$. The intermediate rank bounds of §2 are reusable on their own for any semidefinite program.

The results are proved in the paper. As far as is known, none of them (neither the Pataki rank bound, nor the semidefinite characterization of $f_k$, nor Theorem 4.3) has a machine-checked proof. Formalizing them produces a library of faces and dimensions of spectrahedra, the SDP representation of the Ky Fan sum $f_k$, and the multiplicity bound itself.

Difficulty

Extremality of $x^*$ in $\Theta$ is a statement in the parameter space $\mathbb R^m$ and gives no direct information on the spectrum of $A(x^*)$: perturbation arguments on the eigenvalues alone break down precisely at the coalesced eigenvalues the theorem is about, where $f_k$ is not differentiable. The quantitative bound (4.30) also needs more than the optimal value $f_k(A(x^*))$: it depends on the whole optimal set $\Omega_k(A(x^*))$, on the dimension of faces of spectrahedra, and on an exact count relating the ranks of the optimal $V,W$ to the multiplicity of $\lambda_k$. None of these (faces and dimension of spectrahedra, the semidefinite representation of $f_k$, eigenvalue run lengths) is in Mathlib.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $A\bullet B$ is the published BurerMonteiro.RankIncrease.frob, the primal and dual feasible sets are the published IsPrimalFeasible/IsDualFeasible, and $\lambda_i(B)$ is the published ProjLikeRetr.Spectral.eig B ⟨i-1,_⟩ (Mathlib's nonincreasing eigenvalues, 0-based). Every matrix whose eigenvalues are taken is assumed symmetric. Faces, extreme points and dimension are defined as on p. 341; dimension is integer valued with $\dim\emptyset=-1$. All rank bounds are compared in $\mathbb Z$. $\Theta$ is the argmin set $\{x: f_k(A(x))\le f_k(A(y))\ \forall y\}$ and $\Omega_k(B)$ is the set of feasible points no worse than every feasible point; no infimum is used. Optimal values are stated as least elements of the set of feasible objective values.

Hypotheses added relative to the page, each disclosed in its item: $1\le k<n$ in the statements of §3, which mention $\lambda_{k+1}$; $k\ge1$ (p. 340) in every §4 statement; one common matrix order in Theorem 2.2; and $\lambda_k(B)=\lambda_{k+1}(B)$ in the rank identity of p. 348, which is false as printed when $\lambda_k(B)>\lambda_{k+1}(B)$ ($n=2$, $k=1$, $B=\operatorname{diag}(2,0)$ gives $3\ne2$) and is used in the paper only in the equal case. The linear independence of $A_0,\dots,A_m$ is kept with $A_0$ included, as on p. 348.

Trivializing formalizations are ruled out: $\Theta$ is not defined through a possibly junk infimum, a face must be convex and contained in the set, the dimension is not a junk $0$, $\operatorname{mult}$ is the run length of equal eigenvalues and not a constant or an index, and the eigenvalues are only ever taken of symmetric matrices.

A complete development needs: the rank–dimension bound for faces of spectrahedra (reusable for any SDP), the semidefinite characterization of $f_k$ with its optimal set, and convexity facts on $\Theta$. Proofs of any milestone, alternative proofs of the rank bounds, and the general smooth case of §5 are welcome.

Selected references

• G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23(2), 339–358, 1998. https://doi.org/10.1287/moor.23.2.339
• A. I. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13, 189–202, 1995. https://doi.org/10.1007/BF02574037
• M. L. Overton and R. S. Womersley, Optimality conditions and duality theory for minimizing sums of the largest eigenvalues of symmetric matrices, Mathematical Programming 62, 321–357, 1993. https://doi.org/10.1007/BF01585173
• F. Alizadeh, Interior point methods in semidefinite programming with applications to combinatorial optimization, SIAM Journal on Optimization 5(1), 13–51, 1995. https://doi.org/10.1137/0805002
• A. S. Lewis and M. L. Overton, Eigenvalue optimization, Acta Numerica 5, 149–190, 1996. https://doi.org/10.1017/S0962492900002646
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.