Linear algebra

Completed

Harmonic Analysis Machine Learning·Captain: mikedeng1

Geometric Deep Learning III: An n × n Matrix Commutes with the Cyclic Shift S if and only if It Is Circulant, So Convolution Is Shift EquivarianceTextbook

Why convolution, and why the shift

Convolutional neural networks process images, audio and time series with layers whose weights are shared across positions. The Geometric Deep Learning programme of Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2) explains this architecture by symmetry: on a grid the relevant symmetry is translation, and a linear layer that respects translations is forced to be a convolution. Section 4.2 of the book makes this precise in the simplest setting, a one-dimensional periodic grid, and then derives the discrete Fourier transform from the same symmetry, as the common eigenbasis of all convolution operators. The material is classical in signal processing (see the tutorial of Bamieh, arXiv:1805.05533), and the book uses it as the template that the later chapters generalise to groups, graphs and manifolds; for example, graph signal processing (Sandryhaila and Moura, arXiv:1210.4752) replaces the shift by an adjacency matrix.

This mission formalises the characterisation the book calls the basis of "the overall philosophy of Geometric ML": a matrix is circulant if and only if it commutes with the shift (§4.2, p. 37). It is the third mission of a series on the book. The book numbers no theorems, lemmas or definitions; every item is cited by section, equation or position, and printed page.

Setting

Fix $n \ge 1$ and the ring graph with nodes $\mathbb Z_n = \{0, 1, \dots, n-1\}$ , arithmetic taken modulo $n$ . A signal is a vector $x = (x_0, \dots, x_{n-1})$ with entries in a commutative ring $R$ , for instance $\mathbb R$ .

The circulant matrix of a vector $\theta = (\theta_0, \dots, \theta_{n-1})$ is $C(\theta) = (\theta_{u - v \bmod n})_{u, v}$ : each row is the previous one shifted circularly by one position.
The circular convolution of a signal $x$ with a filter $\theta$ is $(x \star \theta)_u = \sum_{v=0}^{n-1} x_v\, \theta_{u - v \bmod n}$ .
The right shift $S$ is the circulant matrix of $\theta = (0, 1, 0, \dots, 0)^\top$ . It moves a vector one position to the right, $(Sx)_u = x_{u-1}$ .
Over $\mathbb C$ , the discrete Fourier basis is $\varphi_k(u) = n^{-1/2} e^{2\pi i k u / n}$ for $k = 0, \dots, n-1$ . The Fourier matrix $\Phi = (\varphi_0, \dots, \varphi_{n-1})$ has the $\varphi_k$ as columns, and $\Phi^*$ is its conjugate transpose.

In Lean the index set is ZMod n with [NeZero n], $C(\theta)$ is Mathlib's Matrix.circulant θ, and the mission's definitions GeomDL.Grids.conv, GeomDL.Grids.shift, GeomDL.Grids.fourierVec and GeomDL.Grids.fourierMatrix are the four objects above.

Formalization targets

Goal: commuting with the shift characterises circulant matrices

For every $n \times n$ matrix $M$ over a commutative ring $R$ ,

M S = S M \iff M = C(\theta) \text{ for some } \theta \in R^n .

The book states the converse direction tentatively ("the opposite direction appears to be true as well"); it is a theorem, and it is stated here without the hedge.

Milestones, in attack order

Circulant matrices are convolutions, $C(\theta)x = x \star \theta$ , and $S = C(0, 1, 0, \dots, 0)$ shifts right, $(Sx)_u = x_{u-1}$ (p. 37).
The left shift is $S^\top$ , and $S^\top S = S S^\top = I$ (side-note, p. 37).
Shift equivariance of convolution, $S\,C(\theta)\,x = C(\theta)\,S\,x$ (p. 37).
The Fourier basis vectors are eigenvectors of $S$ : $S\varphi_k = e^{-2\pi i k/n}\varphi_k$ , with eigenvalues that are $n$ -th roots of unity (p. 38 and side-note).
These eigenvalues are pairwise distinct (side-note, p. 37).
$\Phi^*\Phi = I$ (side-note, p. 38).

Companion: the Convolution Theorem

With $(\mathcal F\theta)_k = \sum_w \theta_w e^{-2\pi i k w/n}$ ,

C(\theta)\varphi_k = (\mathcal F\theta)_k\,\varphi_k, \qquad C(\theta) = \Phi\,\operatorname{diag}(\mathcal F\theta)\,\Phi^* .

The book prints this with $\hat\theta = \Phi^*\theta = n^{-1/2}\mathcal F\theta$ in place of $\mathcal F\theta$ , which is off by a factor $\sqrt n$ for $n \ge 2$ ; the corrected identity is stated. The transform form of the Convolution Theorem, $\mathcal F(u \star v) = \mathcal F u \cdot \mathcal F v$ with Mathlib's ZMod.dft, is already Proved on the platform as IntMul.HvdH.dft_cyclic_conv and is included as a reference item.

Significance

The goal identifies the space of linear translation-equivariant maps on $R^{\mathbb Z_n}$ with the convolutions, an $n$ -dimensional space parametrised by the filter $\theta$ . This is the statement that lets the book define convolution as a translation-equivariant linear operation, and it is the grid case of the general principle the book develops in §4.3 and §5: a linear map that commutes with a group action is a group convolution. Milestones 4–6 and the companion are the other half of §4.2: the shift has distinct eigenvalues, so every matrix commuting with it is diagonal in the shift's eigenbasis, and that eigenbasis is the Fourier basis; hence the Fourier transform diagonalises every convolution.

Mathlib contains circulant matrices, their commutativity (Matrix.circulant_mul_comm) and the discrete Fourier transform on ZMod n, but neither the converse characterisation nor the diagonalisation of circulant matrices by the normalised Fourier matrix. The mission adds these, in a form that later missions of the series (group convolutions, graph Fourier transforms) can be compared against.

Difficulty

The direction " $\Leftarrow$ " is a one-line consequence of the commutativity of circulant matrices. The content is " $\Rightarrow$ ": the equation $MS = SM$ is an equation between matrices, and it has to be turned into the statement that the entries of $M$ are constant along every cyclic diagonal, with the indices handled modulo $n$ . The spectral argument of the book (commuting matrices with a common eigenbasis) only applies over a field containing the $n$ -th roots of unity in which $n$ is invertible; over a general commutative ring, such as $\mathbb Z$ or $\mathbb Z/2$ , the goal has to be proved without it. For the Fourier statements the work is in the geometric sums of roots of unity and in the bookkeeping between the representatives $\{0, \dots, n-1\}$ used in the exponents and the arithmetic of $\mathbb Z_n$ .

Formalization scope

Indices live in ZMod n with [NeZero n], so $n \ge 1$ and matrices are finite; no lower bound $n \ge 2$ is needed (for $n = 1$ , $S = I$ and every matrix is circulant, so the goal holds). Exponents use the representatives ZMod.val $\in \{0, \dots, n-1\}$ , as on the page.
The goal and milestones 1–3 are stated over an arbitrary commutative ring $R$ ; milestones 4–6 and the companion are over $\mathbb C$ .
"Circulant" means equal to Matrix.circulant θ for some θ. Defining a matrix to be circulant when it commutes with $S$ would make the goal true by definition; the mission does not do that. A sanity file checks that the shift moves vectors to the right on $\mathbb Z_3$ and that $\operatorname{diag}(1, 0)$ on $\mathbb Z_2$ does not commute with $S$ .
The side-note on p. 38 calls $\Phi$ "orthogonal"; the property it writes, $\Phi^*\Phi = I$ with the conjugate transpose, is unitarity, and that is what is stated.
The Fourier normalisation is the book's $n^{-1/2}$ in $\varphi_k$ ; the eigenvalues in the companion use Mathlib's unnormalised ZMod.dft, and the factor $\sqrt n$ is written out in its statement.

No new infrastructure beyond Mathlib is required. Proofs of any item, and proofs of the goal that avoid the spectral argument, are welcome; the shift and Fourier lemmas are reusable for the graph Fourier transform later in the book.

Selected references

M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021 (v2). §4.2, pp. 35–38. https://arxiv.org/abs/2104.13478
B. Bamieh, Discovering Transforms: A Tutorial on Circulant Matrices, Circular Convolution, and the Discrete Fourier Transform, arXiv preprint, 2018. https://arxiv.org/abs/1805.05533
A. Sandryhaila, J. M. F. Moura, Discrete Signal Processing on Graphs, IEEE Transactions on Signal Processing, 2013. https://arxiv.org/abs/1210.4752
D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics, 2021 (source of the platform's proved IntMul.HvdH.dft_cyclic_conv). https://hal.science/hal-02070778

9 thms3 active usersReviewed

Quantum Information Representation Theory·Captain: mikedeng1

Commutant Structure of U⊗(n−1) ⊗ U* Transformations: The Operator Basis v^{ab}_{ij}(α) Is a Linear Combination of Partially Transposed Permutation Operators, and ConverselyResearch Paper

Motivation

Operators on $n$ copies of $\mathbb C^d$ that commute with every $U^{\otimes n}$ , $U$ unitary, are exactly the linear combinations of permutation operators $V(\sigma)$ , $\sigma\in S(n)$ (Schur–Weyl duality). Many protocols in quantum information carry a different symmetry: the first $n-1$ systems transform by $U$ and the last by the complex conjugate $\bar U$ . It is the symmetry of port-based teleportation (Ishizaka–Hiroshima 2008), whose optimal performance is computed from the representation theory of exactly this commutant (Studziński et al. 2017). The commutant of $U^{\otimes(n-1)}\otimes\bar U$ is the algebra $\mathcal A$ spanned by the partially transposed permutation operators $V'(\sigma)$ : the permutation operators with the transpose taken on the last system.

Studziński, Horodecki and Mozrzymas give an explicit operator basis of an ideal of $\mathcal A$ adapted to the irreducible representations of $S(n-2)$ . Their main structural result, Theorem 9, states that this basis and the partially transposed permutation operators are linear combinations of each other, with coefficients that are irrep matrix elements.

Setting

Let $\mathcal H=\mathbb C^d$ and $n\ge2$ . For $\sigma\in S(n)$ , the permutation operator $V(\sigma)$ on $\mathcal H^{\otimes n}$ is $V(\sigma)|i_1\dots i_n\rangle=|i_{\sigma^{-1}(1)}\dots i_{\sigma^{-1}(n)}\rangle$ . The partial transposition $X\mapsto X'$ transposes the last system: $(|x_1\dots x_n\rangle\langle y_1\dots y_n|)'=|x_1\dots x_{n-1}y_n\rangle\langle y_1\dots y_{n-1}x_n|$ . The algebra $\mathcal A$ is the span of all $V'(\tau)$ , $\tau\in S(n)$ . $S(k)$ is regarded inside $S(n)$ as the permutations fixing the systems after $k$ .

Fix $\pi_1,\dots,\pi_{n-1}\in S(n-1)$ with $\pi_k(n-1)=k$ , and write $\Pi_k=V(\pi_k)$ . For labels $a,b\in\{1,\dots,n-1\}$ , the maps $f_{ab}:S(n-2)\to S(n)$ are

f_{ab}(\sigma)=\pi_b\circ\sigma\circ(n\ n-1)\circ\pi_a^{-1}.

The standing data are a family of real orthogonal, irreducible, pairwise inequivalent matrix representations $\varphi^\alpha$ of $S(n-2)$ , of dimensions $d_\alpha$ , and a Schur basis: an orthonormal basis $|\phi_i(\alpha,r)\rangle$ of $\mathcal H^{\otimes(n-2)}$ , where $r$ ranges over the multiplicity of $\alpha$ , such that $V(\sigma)|\phi_j(\alpha,r)\rangle=\sum_i\varphi^\alpha_{ij}(\sigma)|\phi_i(\alpha,r)\rangle$ . With $|\Phi^+\rangle=\frac1{\sqrt d}\sum_l|ll\rangle$ on the last two systems, the paper defines

|\psi^k_i(\alpha,r)\rangle=\sqrt d\,\Pi_k|\phi_i(\alpha,r)\rangle|\Phi^+\rangle,\qquad v^{ab}_{ij}(\alpha)=\sum_r|\psi^a_i(\alpha,r)\rangle\langle\psi^b_j(\alpha,r)|,

and $E^\alpha_{ij}=\sum_r|\phi_i(\alpha,r)\rangle\langle\phi_j(\alpha,r)|$ . In Lean these are IrrepFamily, SchurBasis, psi, vOp, EOp, with ptLast for $'$ , fPerm for $f_{ab}$ and algA for $\mathcal A$ .

Formalization targets

Goal: Theorem 9

For all $a,b$ , $\alpha$ , $i,j$ :

v^{ab}_{ij}(\alpha)=\frac{d_\alpha}{(n-2)!}\sum_{\sigma\in S(n-2)}\varphi^\alpha_{ij}(\sigma)\,V'\big(f_{ba}(\sigma)\big)\in\mathcal A,

and for every $\sigma\in S(n-2)$ , with $\sigma_{ab}=f_{ab}(\sigma)$ ,

V'(\sigma_{ab})=\bigoplus_\alpha\sum_{i,j}\varphi^\alpha_{ij}\big(f_{ab}^{-1}(\sigma_{ab})\big)\,v^{ba}_{ij}(\alpha).

The goal is the whole theorem, both directions and the membership in $\mathcal A$ .

Milestones

Permutations of $S(n-1)$ are invariant under $'$ and pass through it: $V(\rho)V'(\tau)V(\rho')=V'(\rho\tau\rho')$ (proof of Lemma 26).
Lemma 26: $V'(\sigma_{ab})=\Pi_bV(f^{-1}_{ab}(\sigma_{ab}))V'(n\ n-1)\Pi_a^{-1}$ with $f^{-1}_{ab}(\sigma_{ab})\in S(n-2)$ .
Eq. (9): the $S_{ab}=f_{ab}(S(n-2))$ and $S(n-1)$ partition $S(n)$ , and each $f_{ab}$ is injective.
$V'(n-1,n)=\mathbb 1\otimes\sum_{l,l'}|ll\rangle\langle l'l'|$ .
Eq. (21): $E^\alpha_{ij}\in\mathbb C[S(n-2)]$ maps to $v^{ab}_{ij}(\alpha)=\Pi_a(E^\alpha_{ij}\otimes\mathbb 1)V'(n\ n-1)\Pi_b^{-1}\in\mathcal M$ .
Eq. (139): the orthogonality relation $\frac1{|G|}\sum_g\varphi^\alpha_{ij}(g)\varphi^\beta_{kp}(g^{-1})=\frac1{d_\alpha}\delta^{\alpha\beta}\delta_{ip}\delta_{jk}$ for $G=S(n-2)$ .
Eq. (86): $E^\alpha_{ij}=\frac{d_\alpha}{(n-2)!}\sum_\sigma\varphi^\alpha_{ij}(\sigma)V(\sigma)$ .
Eq. (86): $V(\sigma)=\bigoplus_\alpha\sum_{ij}\varphi^\alpha_{ij}(\sigma)E^\alpha_{ij}$ .

Significance

Theorem 9 shows that the $v^{ab}_{ij}(\alpha)$ span the same space as the operators $V'(\sigma)$ with $\sigma(n)\neq n$ . That space is the ideal of $\mathcal A$ on which the partial transposition acts non-trivially. Because the $v^{ab}_{ij}(\alpha)$ multiply like block matrices (Lemma 8 of the paper), the theorem converts questions about $\mathcal A$ into finite matrix computations indexed by irreps of $S(n-2)$ . The later constructions of the paper rest on this: the Gram matrices $Q(\alpha)$ , the biorthogonal basis and the explicit irreps of $\mathcal A$ . The same formalism underlies the eigenvalue analysis of port-based teleportation (Mozrzymas–Studziński–Horodecki 2018).

The result has a published proof but no machine-checked one. This mission adds that check, together with a reusable Lean vocabulary: the partial transpose on one site of $(\mathbb C^d)^{\otimes n}$ , the embeddings $S(k)\hookrightarrow S(n)$ , and Schur-basis data for permutation operators. It also pins down the conventions that the printed text leaves inconsistent (see Formalization scope).

Difficulty

The algebraic manipulations are short on paper; the work lies in the bookkeeping they hide. Lemma 26 requires checking that $\pi_b^{-1}\circ\sigma_{ab}\circ\pi_a\circ(n\ n-1)$ fixes both of the last two systems, which uses $\pi_k(n-1)=k$ in an essential way. The partial transposition is not multiplicative, so every step that moves an operator through $'$ needs the specific invariance of milestone 1. Eq. (86) is the identification of the Schur-basis matrix units with group-algebra elements; it needs completeness of the basis together with Schur's orthogonality relations for real irreps, and it is false without irreducibility and inequivalence. Mathlib has Schur's lemma but no coordinate form of the orthogonality relations for matrix representations, and nothing on partial transposes of tensor-power permutation operators.

Formalization scope

Indexing. The paper's $n$ is $m+2$ . $S(n-2)$ , $S(n-1)$ , $S(n)$ are Equiv.Perm (Fin m), Equiv.Perm (Fin (m+1)), Equiv.Perm (Fin (m+2)). Systems are 0-based, so systems $n-1,n$ are indices $m,m+1$ , and labels $a,b$ are Fin (m+1). Permutation products compose right to left.
Operators are complex matrices indexed by $\{1..d\}^k$ . $V(\sigma)$ is the published QAlgorithms.Schur.tensorPermutation. $'$ is on the last system only. groupAlg is the represented $\mathbb C[S(n-2)]$ ; algM spans the $V'(\tau)$ with $\tau(n)\ne n$ .
Standing data. IrrepFamily m contains real orthogonal matrix representations of $S(m)$ of positive dimension, irreducible over $\mathbb C$ and pairwise inequivalent over $\mathbb C$ (p. 7 and Notation 32 of the paper). SchurBasis F d is an orthonormal, spanning family of vectors on which $V(\sigma)$ acts by the $\varphi^\alpha$ . Multiplicities may be zero. The family is not required to list every irrep of $S(m)$ . Every $\pi_k$ satisfies $\pi_k(n-1)=k$ (Definition 24).
Constants are literal: $d_\alpha/(n-2)!$ , the factor $\sqrt d$ of $\psi$ and the $1/\sqrt d$ of $|\Phi^+\rangle$ . $\bigoplus_\alpha$ is a sum over all labels.
Ruled out. $v^{ab}_{ij}(\alpha)$ is defined from the vectors $\psi$ (Definition 5) and $E^\alpha_{ij}$ from the Schur basis (footnote 4). Neither is defined as a group sum or through $\mathcal F^t_{ab}$ , and the Schur basis carries no orthogonality relation. A formalization that builds (86) or (21) into the definitions makes Theorem 9 a tautology and is not this mission.
Source slips. Eq. (11) prints $\sigma_{ab}(n)=a$ , $\sigma^{-1}_{ab}[n]=b$ , contrary to Notation 1 and eq. (7); the Lean statements follow Notation 1 ( $\sigma_{ab}(a)=n$ , $\sigma_{ab}(n)=b$ ). Eq. (139) is stated with $1/|G|$ and a sum over $g$ , correcting the printed $1/n!$ and $\sum_h$ .
Welcome contributions: the coordinate Schur orthogonality relations for matrix representations of finite groups, and lemmas on ptLast and on liftPerm. Both are reusable beyond this paper.

Selected references

M. Studziński, M. Horodecki, M. Mozrzymas, Commutant structuture of $U^{\otimes(n-1)}\otimes U^*$ transformations, arXiv:1305.6183v2, 2013. https://arxiv.org/abs/1305.6183
S. Ishizaka, T. Hiroshima, Asymptotic teleportation scheme as a universal programmable quantum processor, Phys. Rev. Lett. 101, 240501, 2008. https://arxiv.org/abs/0807.4568
M. Studziński, S. Strelchuk, M. Mozrzymas, M. Horodecki, Port-based teleportation in arbitrary dimension, Sci. Rep. 7, 10871, 2017. https://arxiv.org/abs/1612.09260
M. Mozrzymas, M. Studziński, M. Horodecki, A simplified formalism of the algebra of partially transposed permutation operators with applications, J. Phys. A 51, 125202, 2018. https://arxiv.org/abs/1708.02434

11 thms3 active usersReviewed

Quantum Information·Captain: mikedeng1

On a Family of a Linear Maps from Mₙ(ℂ) to Mₙ²(ℂ): Φ[α, β] on M₃(ℂ) Is 2-Positive and Not Completely Positive Exactly When β ≤ −0.2 and α Lies in an Explicit IntervalResearch Paper

Motivation

Positive linear maps on complex matrix algebras provide tests for quantum entanglement: applying such a map to one part of a bipartite state can expose a state that cannot be written as a mixture of product states. The distinction between ordinary positivity, positivity with an auxiliary matrix system, and complete positivity is therefore substantive. Collins, Osaka, and Sapra study an explicit two-parameter family that makes these distinctions visible through inequalities in the parameters. Their paper identifies the exact region where a map from three-by-three matrices to nine-by-nine matrices is 2-positive but fails to be completely positive. This is the stated main result of their 2018 paper, rather than an open conjecture.

Setting

Write $M_n(\mathbb C)$ for the algebra of $n\times n$ complex matrices. A matrix $X$ is positive semidefinite, written $X\geq0$ , when it is Hermitian and has no negative eigenvalues. A complex-linear map $\Psi:M_{d_1}(\mathbb C)\to M_{d_2}(\mathbb C)$ is positive when $X\geq0$ implies $\Psi(X)\geq0$ . It is $k$ -positive when the same condition holds after the identity map on $M_k(\mathbb C)$ is tensored with $\Psi$ . It is completely positive when it is $k$ -positive for every $k$ . A map is completely copositive when its composition with transpose on the source is completely positive. These are the paper's definitions on page 2.

Let $B_n=\sum_{i=1}^n e_i\otimes e_i$ be the unnormalized Bell vector, and let $B_{n^2}=B_nB_n^*$ denote its rank-one projector. For real $\alpha,\beta$ and $n\geq3$ , the family on page 3 is

\Phi_{\alpha,\beta,n}(A) =A^{\mathsf T}\otimes I_n+I_n\otimes A +\operatorname{Tr}(A)\bigl(\alpha I_{n^2}+\beta B_{n^2}\bigr).

The transpose belongs to the first tensor factor. The mission concentrates on $\Phi[\alpha,\beta]=\Phi_{\alpha,\beta,3}$ . Its Choi matrix is $C_\Psi=\sum_{i,j}e_{ij}\otimes\Psi(e_{ij})$ . For this finite-dimensional setting, the Choi criterion relates complete positivity to $C_\Psi\geq0$ ; it does not define complete positivity. The paper also identifies an equivariance property: unitary conjugation of the input corresponds to conjugation of the output by a matrix associated with the same unitary.

Formalization targets

For $\beta\in\mathbb R$ , define two boundary curves and a cubic root:

\ell_P(\beta)=\frac{-(2+3\beta)+\sqrt{9\beta^2-4\beta+4}}2, \qquad \ell_{CP}(\beta)=\frac{-(3+3\beta)+\sqrt{9\beta^2-10\beta+17}}2,

S_\beta=\min\{x\in\mathbb R:x^3+(-2-3\beta)x^2+(-2+4\beta)x+2\beta=0\}.

The goal is Theorem 3.9, page 10:

\Phi[\alpha,\beta]\text{ is 2-positive and not completely positive} \quad\Longleftrightarrow\quad \beta\leq-\tfrac15, \quad\alpha\in[\ell_P(\beta),\ell_{CP}(\beta)) \cap[1,\infty)\cap[-S_\beta,\infty).

The left endpoint of the first interval is included and the right endpoint is excluded. The milestones record the paper's earlier criteria for positivity, complete positivity, and 2-positivity, together with its general equivariance criterion and the computation for this family. Their inequalities are separate targets; none is built into the definitions of these map properties.

Significance

The goal gives an exact, parameter-level example of 2-positivity without complete positivity. It identifies all such members of this family on $M_3(\mathbb C)$ , including the boundary cases, rather than only exhibiting one map. The surrounding results locate the positive and completely positive regions and give a criterion for testing $k$ -positivity of equivariant maps. Together, they provide a compact source of concrete maps with different strengths of positivity, as described in Sections 2 and 3 of the paper.

The mathematical result was proved in 2018. This mission seeks a machine-checked account of the stated criteria, with the family, Choi matrix, Bell projector, and positivity predicates exposed as reusable declarations. A finished proof would connect elementary matrix positivity and tensor products to explicit real-algebraic parameter bounds. It would also make each boundary independently inspectable. The Lean theorem statements here are draft targets with sorry; they are not existing machine-checked proofs of the paper.

Difficulty

Testing only $\Phi[\alpha,\beta](e_{11})\geq0$ yields ordinary positivity, not 2-positivity. Testing only the Choi matrix addresses complete positivity, which is stronger than the desired property. The 2-positive condition quantifies over every positive semidefinite matrix in $M_2(\mathbb C)\otimes M_3(\mathbb C)$ ; the paper's criterion reduces that universal condition under equivariance to positivity of a specific block matrix. The block matrix has parameter-dependent eigenvalues, including roots of a cubic. This makes a simple comparison of the two square-root boundary curves insufficient: the smallest cubic root supplies an additional lower bound on $\alpha$ . The endpoint $\beta=-1/5$ also needs attention because the case descriptions for complete positivity meet there.

Formalization scope

The Lean model uses Matrix (Fin n) (Fin n) ℂ for $M_n(\mathbb C)$ and Fin n × Fin n for the output tensor indices, with the first coordinate corresponding to the transposed factor. The paper's one-based $e_{11}$ is Matrix.single 0 0 1. Positive semidefiniteness is Mathlib's Matrix.PosSemidef. The shared QAlgorithms.idTensorSuperop applies a map blockwise with the auxiliary index first, and the published QAlgorithms.Entanglement.IsCompletelyPositive quantifies over all auxiliary sizes. Size zero is harmless for that quantifier because the corresponding matrix type is empty. The paper's $n\geq3$ appears on the general-family results; the main goal fixes $n=3$ .

The Bell projector is unnormalized, matching the paper's $B_nB_n^*$ . The two square roots have positive radicands on the real parameter range. The cubic root $S_\beta$ is defined as the infimum of its real root set; the odd-degree cubic has a nonempty, finite set of real roots, so this is its least root. The proof development needs reusable facts about unitary conjugation of positive matrices, Kronecker products, Choi matrices, and positivity of the parameterized block matrix. Direct calculations of the boundary inequalities are also welcome. Defining $k$ -positivity by the block criterion, complete positivity by Choi positivity, omitting the transpose in $\Phi$ , or treating $S_\beta$ as an arbitrary parameter would make the targets lose their intended content.

Selected references

Benoît Collins, Hiroyuki Osaka, and Gunjan Sapra, On a family of a linear maps from Mn(C) to Mn2(C), Linear Algebra and its Applications, 2018; cited here from arXiv:1802.07553v1, pp. 2–10.

12 thms3 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: Shuze Chen

Lectures on Modern Convex Optimization V: Semidefinite Representability of Symmetric Functions of EigenvaluesTextbook

Motivation

A convex optimization problem can be handed to a semidefinite programming solver only after its constraints and objective have been written as linear matrix inequalities (LMIs): conditions of the form $\mathcal A(x,u) \succeq 0$ , where $\mathcal A$ is affine in the decision variables $x$ and in auxiliary variables $u$ , and $\succeq 0$ means positive semidefinite. A large share of modern engineering optimization is built this way, in robust control, structural design, and statistics and machine learning (nuclear-norm and spectral-norm regularization, eigenvalue optimization). Modeling tools such as CVX and YALMIP rest on a catalog of functions known to admit such a description.

Lecture 4 of A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), builds that catalog for the semidefinite cone. Its central entry is a general rule: a convex function of a symmetric matrix that depends only on the eigenvalues, symmetrically, is expressible by LMIs whenever the underlying function of a vector is. This covers the largest eigenvalue, sums of the $k$ largest eigenvalues (Ky Fan, 1949), Schatten norms $\|X\|_p$ and powers of the determinant at once. The tool behind it is the theory of majorization (Hardy, Littlewood and Pólya, 1929; Rado, 1952) together with Birkhoff's theorem on double-stochastic matrices (1946).

Setting

For a symmetric $m\times m$ real matrix $X$ , $\lambda(X) = (\lambda_1(X),\dots,\lambda_m(X))$ denotes its eigenvalues counted with multiplicity in nonascending order, $\lambda_1(X) \ge \cdots \ge \lambda_m(X)$ . $S_k(X) = \lambda_1(X) + \cdots + \lambda_k(X)$ is the sum of the $k$ largest. For a vector $y \in \mathbb R^m$ , $S_j(y)$ is the sum of its $j$ largest entries, and $X[x]$ is the convex hull of the $m!$ coordinate permutations of $x$ . A function $g : \mathbb R^m \to \mathbb R\cup\{+\infty\}$ is symmetric if permuting the coordinates of its argument leaves its value unchanged. A matrix is double-stochastic if its entries are nonnegative and every row and column sums to $1$ .

A function $g$ is semidefinite representable (SDr) if there is a map $\mathcal S(x,t,u)$ , affine in $(x,t,u) \in \mathbb R^m\times\mathbb R\times\mathbb R^k$ with values in the symmetric $N\times N$ matrices, such that

t \ge g(x) \iff \exists u : \mathcal S(x,t,u) \succeq 0 \qquad \text{for all } x \in \mathbb R^m,\ t\in\mathbb R.

For a $k\times l$ matrix $X$ ( $k \le l$ ), the singular values are $\sigma_i(X) = \lambda_i((XX^T)^{1/2})$ , and $\Sigma_j(X) = \sigma_1(X)+\cdots+\sigma_j(X)$ .

Formalization targets

Goal: Proposition 4.2.1 (p. 151)

Let $g$ be symmetric and SDr with representation $\mathcal S$ . Then for every symmetric $m\times m$ matrix $X$ and real $t$ ,

t \ge g(\lambda(X)) \iff \exists\, x \in \mathbb R^m,\ u:\ \ \mathcal S(x,t,u)\succeq 0,\ \ x_1\ge\cdots\ge x_m,\ \ S_j(X)\le x_1+\cdots+x_j\ (j=1,\dots,m-1),\ \ \operatorname{Tr}X = x_1+\cdots+x_m. \tag{4.2.3}

Milestones, in attack order

(A), p. 148: $X \succeq X' \Rightarrow \lambda_i(X) \ge \lambda_i(X')$ for every $i$ .
Example 18.c, p. 147: for $k \le m$ , $S_k(X) \le t$ iff there are $s \in \mathbb R$ and $Z$ with $t - ks - \operatorname{Tr}Z \ge 0$ , $Z \succeq 0$ , $Z - X + sI_m \succeq 0$ (4.2.2).
Birkhoff's theorem, p. 281: the double-stochastic matrices are exactly the convex combinations of permutation matrices. This is referenced, already proved on the platform as FamousTheorems.birkhoff_von_neumann.
(C), p. 281: $f(Px) \le f(x)$ for a convex symmetric $f$ , $x \in \operatorname{Dom} f$ and double-stochastic $P$ .
Claim (majorization principle), p. 285: $X[x] = \{y : S_j(y) \le S_j(x),\ j = 1,\dots,m-1,\ \sum_i y_i = \sum_i x_i\}$ .
(D), p. 282: for a real-valued convex symmetric $f$ , $f(\lambda(A)) = \max_{V \text{ orthogonal}} f(\operatorname{Dg}(V^TAV))$ .
Proposition 4.2.2, p. 154: for $g$ symmetric, monotone on $\mathbb R^k_+$ and SDr, $t \ge g(\sigma(X))$ iff $\exists x, u$ with $\mathcal S(x,t,u)\succeq 0$ , $x_1 \ge \cdots \ge x_k$ , $\Sigma_j(X) \le x_1+\cdots+x_j$ for $j = 1,\dots,k$ (4.2.4).

A further level

A strengthened variant of the goal states that (4.2.3) remains exact when the ordering constraint $x_1 \ge \cdots \ge x_m$ is removed.

Significance

The result itself. Proposition 4.2.1 reduces semidefinite representability of a spectral function on $\mathbf S^m$ , a space of dimension $m(m+1)/2$ , to semidefinite representability of a symmetric function on $\mathbb R^m$ . The extra cost is $m$ scalar variables, $m-1$ ordering inequalities, $m-1$ Ky Fan constraints (each an LMI of size $m$ by 18.c) and one trace equation. The representation is explicit, so a modeling language can generate it mechanically. Proposition 4.2.2 does the same for functions of singular values, which covers the nuclear norm and the operator norm of rectangular matrices. Fact (D) is the variational description that makes $X \mapsto g(\lambda(X))$ convex (Davis, 1957; Lewis, 1996).

Formalizing it. All results here are classical and proved in the book, partly through exercises (4.14–4.16 for the goal). None of them is formalized on Prove2Me beyond Birkhoff's theorem, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix. A related proved platform item, Matrix.IsHermitian.sorted_eigenvalues_le_add_of_re_dotProduct_le, is a Weyl-type inequality that implies (A) when its slack is zero. Mathlib has sorted eigenvalues of Hermitian matrices (eigenvalues₀) but no Ky Fan sums, no majorization theory and no notion of semidefinite representation. This mission produces them.

Difficulty

The forward direction of every representation is a choice of witness. The content is in the converse: from an arbitrary feasible point of the LMI system one must recover the inequality for the eigenvalues. For (4.2.3) this means showing that partial-sum domination plus equal totals places $\lambda(X)$ inside the convex hull of the permutations of the witness $x$ . The obvious coordinatewise comparison fails, because $\lambda(X)$ is not dominated entrywise by $x$ . The hard half of the majorization principle (Exercise 4.15) is this step, and it does not follow from convexity of $S_j$ alone. In Proposition 4.2.2 the witness only dominates the singular values in partial sums, with no equality of totals, so majorization alone does not suffice there.

Formalization scope

Vectors are Fin m → ℝ (0-based indices) and matrices Matrix (Fin m) (Fin m) ℝ. Symmetric means Matrix.IsHermitian and $\succeq 0$ means Matrix.PosSemidef, which includes symmetry. $\lambda(X)$ is Mathlib's antitone IsHermitian.eigenvalues₀; it is applied only to symmetric matrices. Functions with values in $\mathbb R\cup\{+\infty\}$ are EReal-valued and never $-\infty$ , and only order comparisons with real numbers are made on them. A representation $\mathcal S$ is an explicit affine map with symmetric coefficient matrices. In Proposition 4.2.2 the function $g$ , given on $\mathbb R^k_+$ only, is extended by $+\infty$ outside $\mathbb R^k_+$ . The singular values are written as $\sqrt{\lambda_i(XX^T)}$ , which equals $\lambda_i((XX^T)^{1/2})$ . Typos on the page are corrected and listed in the items: $S_k(x)$ for $S_k(X)$ in 18.c, and $f$ and $j = 1,\dots,m$ in Proposition 4.2.2.

The claim " $f$ is SDr" admits a trivializing formalization: asserting that some LMI system projects onto the epigraph, with no control over its shape or size, says nothing beyond convexity. Every statement here instead pins the representation down as the book's explicit system (4.2.2), (4.2.3) or (4.2.4), quantified over every symmetric matrix and every real $t$ .

Beyond the paper. One strengthened variant is posed: Proposition 4.2.1 with the constraint $x_1 \ge \cdots \ge x_m$ removed from (4.2.3) (finding F1). The evidence is that $x_1+\cdots+x_j$ never exceeds the sum of the $j$ largest entries of $x$ , so the remaining constraints already express majorization. The variant is not a milestone, and the book's statement stays the goal.

A complete development needs:

majorization on $\mathbb R^m$ (sums of largest entries, the permutation hull);
Birkhoff's theorem, available in Mathlib;
monotonicity of sorted eigenvalues in the Loewner order;
spectral decomposition for constructing witnesses;
singular values through $XX^T$ .

Majorization, the Ky Fan representation and fact (A) are reusable well beyond this chapter, for instance in eigenvalue optimization and the analysis of interior-point methods. Contributions of these as standalone results are welcome.

Selected references

A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, MPS/SIAM Series on Optimization, SIAM, 2001. doi:10.1137/1.9780898718829
G. Birkhoff, Tres observaciones sobre el álgebra lineal, Univ. Nac. Tucumán Rev. Ser. A 5 (1946), 147–151.
K. Fan, On a theorem of Weyl concerning eigenvalues of linear transformations I, Proc. Natl. Acad. Sci. USA 35 (1949), 652–655. doi:10.1073/pnas.35.11.652
A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6 (1996), 164–177. doi:10.1137/0806009
A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. doi:10.1007/978-0-387-68276-1

9 thms3 active usersReviewed

Completed

Quantum Information·Captain: mikedeng1

Improvements in Quantum SDP-Solving with Applications 1: A Unitary Preparing a Purification of a Subnormalized Density Operator ϱ Gives an Exact (1, w+a+1, 0)-Block-Encoding of ϱResearch Paper

Motivation

Quantum algorithms for semidefinite programming need a way to use an input matrix inside a quantum circuit. In the quantum state input model, an oracle prepares a purification of a density operator. In the quantum operator input model, a unitary instead exposes that operator as a block of a larger unitary. The two kinds of access serve different subroutines. Lemma 12 of van Apeldoorn and Gilyén’s 2018 preprint connects them for a subnormalized density operator. The same paper uses this connection when comparing its input models for quantum SDP solving.

The result concerns a precise finite-dimensional construction. It matters even without the paper’s query-complexity estimates: it specifies which registers must be present, what happens to probability mass outside the accepted flag state, and which block of the resulting unitary equals the desired operator. These details are easy to lose when a statement is shortened to “purification gives a block-encoding.”

Setting

A w-qubit register has basis labels in $\{0,1\}^{w}$ . A subnormalized density operator $\varrho$ on that register is a positive semidefinite complex matrix with $\operatorname{Tr}\varrho\leq1$ . Its trace may be strictly below one. A purification is a unit vector $|\varphi\rangle$ on three registers: the w-qubit system, one flag qubit, and a c-qubit junk register. The operator $\varrho$ is the flag-zero block after tracing out the junk. In entries,

\varrho_{ij}=\sum_{t\in\{0,1\}^{c}}\varphi_{i,0,t}\,\overline{\varphi_{j,0,t}}.

Thus probability in the flag-one branch does not contribute to $\varrho$ . Let $a=c+1$ , so a unitary $G$ preparing $|\varphi\rangle$ acts on $w+a$ qubits and $|\varphi\rangle=G|0\rangle^{\otimes(w+a)}$ . The result adds an initial w-qubit system and one extra qubit. Its register swap $S$ exchanges the initial $(\text{system},\text{extra})$ register with the $(\text{prepared system},\text{flag})$ register and leaves the c junk qubits fixed. The construction is

V=(I_{2^{w+1}}\otimes G^{\dagger})S(I_{2^{w+1}}\otimes G).

A $(\alpha,k,\varepsilon)$ block-encoding of an operator $A$ is a unitary on the system and k ancilla qubits whose all-zero ancilla block differs from $A/\alpha$ in operator norm by at most $\varepsilon/\alpha$ . Here the scale is one and the error is zero. The block of $V$ is taken at the all-zero state of the extra qubit and the entire register of $G$ .

Formalization targets

The goal is Lemma 12 with the ancilla count given by its displayed construction:

\left\|\varrho-(I_{2^w}\otimes\langle0|^{\otimes(w+a+1)})V (I_{2^w}\otimes|0\rangle^{\otimes(w+a+1)})\right\|=0.

The target includes that $V$ is unitary, making it an exact $(1,w+a+1,0)$ block-encoding of $\varrho$ . The theorem identifies $V$ explicitly, so its use of one $G$ and one $G^{\dagger}$ is part of the construction. The source’s Lemma 12 prints $(1,w+a,0)$ , while its proof says $V$ has $2w+a+1$ qubits and takes the block at $1+w+a$ ancillas. This mission uses the proof’s consistent count and labels the correction. The four milestones follow the proof’s stated steps: unitarity of $V$ , identification of its zero block, elimination of the flag-one component, and equality of the remaining SWAP sandwich with $\varrho$ .

Significance

The exact identity shows that a state-preparation unitary can be used where the paper’s quantum operator model expects a block-encoding. It also covers genuinely subnormalized operators, for which a normalized-state argument is insufficient: a preparation may have nonzero amplitude in the flag-one branch even though only the flag-zero branch defines $\varrho$ . The explicit ancilla count prevents such lost probability mass from being silently included in the output block.

Formalizing this known result gives a reusable interface between a purification predicate and a block-encoding predicate. The mission statement is open on Prove2Me; the paper’s mathematical argument is known. A related open block-encoding statement in Nannicini’s treatment concerns a normalized density matrix and a circuit-level construction with a different ancilla arrangement. It does not state this paper’s subnormalized, flag-qubit identity. The finite-register definitions and SWAP identities can be reused by later matrix-level quantum algorithms, whether or not the paper’s larger complexity bounds are formalized.

Difficulty

The first apparent shortcut is to use the ordinary purification identity without the flag qubit. That recovers the trace over both flag outcomes, which can have trace one even when $\operatorname{Tr}\varrho<1$ . The required block must select flag zero. A second source of error is register order: the paper displays the system first, while the existing Lean block-encoding predicate places the ancilla register first. Equality of matrix blocks depends on the explicit reindexing. Complex conjugation also matters: swapping the vector and covector amplitudes would produce a transpose of $\varrho$ instead of $\varrho$ for complex states.

Formalization scope

The Lean system register is QAlgorithms.Qubits w; the flag and extra register are each Bool; and the junk is QAlgorithms.Qubits c. The identity $a=c+1$ makes the flag register present even at $c=0$ . The all-zero state is the all-false basis label. Matrices are over $\mathbb C$ , tensor products are matrix Kronecker products, and $S$ is a permutation matrix fixing the junk. The paper’s printed identity factor beside the swap has size $2^a$ ; the consistent factor is $2^{a-1}=2^c$ , since the swap already acts on two $w+1$ -qubit registers.

The referenced QAlgorithms.IsBlockEncoding definition includes unitarity and measures error with the operator norm. Lean reindexes $V$ to put its $(\text{extra},\text{prepared system},\text{flag},\text{junk})$ ancilla first. The theorem requires $G$ unitary, $\varrho$ subnormalized, and the exact purification relation between $G|0\rangle$ and $\varrho$ . The purification relation prevents a vacuous claim about an unrelated matrix. The optional quantum gate-count clause of the printed lemma is outside this matrix-level formalization; the register swap is explicitly the swap of $w+1$ qubit pairs. A circuit-level gate-count theorem would require an additional gate-list representation.

The needed reusable components are finite complex matrices, unitary permutation matrices, Kronecker products, partial traces, and the operator norm. Contributions can address the four milestone identities, the main theorem, or a circuit-level refinement of the gate count. None of the statements introduces the proof’s Schmidt decomposition as an assumption.

Selected references

J. van Apeldoorn and A. Gilyén, Improvements in Quantum SDP-Solving with Applications, arXiv preprint, 2018, arXiv:1804.05058v1, Definition 1 (p. 3), Definition 2 (p. 4), Lemma 12 and proof (pp. 15–16).
G. Nannicini, Quantum Algorithms for Optimizers, arXiv preprint, 2024, arXiv:2408.07086, Definition 7.11 and the normalized density-matrix construction.

8 thms3 active usersReviewed

Quantum Information·Captain: mikedeng1

Improvements in Quantum SDP-Solving with Applications 2: A Two-Outcome Measurement Implemented With Bias ε Gives a (1, a+1, ε)-Block-Encoding of Its POVM Element MResearch Paper

Motivation

Many recent quantum algorithms for linear algebra and optimization take their input as a block-encoding: a unitary circuit whose top-left block, after projecting a set of ancilla qubits onto $|0\rangle$ , approximates the matrix of interest. The quantum semidefinite-programming solver of van Apeldoorn and Gilyén (arXiv:1804.05058) introduces the quantum operator model, in which every constraint matrix of the SDP is given this way (Definition 2, p. 4). Block-encodings are also the input format of quantum singular value transformation and of Hamiltonian simulation by qubitization (Low and Chuang, arXiv:1610.06546).

A natural question is where block-encodings come from in applications. In §4.1, on shadow tomography, the constraint matrices are the elements $E_j$ of two-outcome measurements, and what a user can do is perform those measurements, not write down their matrices. The closing remark of §4.1 (pp. 24–25) answers the question for that setting: if a two-outcome measurement can be implemented on a quantum computer with small bias, then a block-encoding of its measurement operator can be built from the same circuit with one extra qubit and one CNOT gate. The remark is credited to the same observation by Low and Chuang (arXiv:1707.05391).

Setting

A two-outcome POVM on a finite-dimensional system is a pair $\{M, I - M\}$ of operators with $M$ and $I - M$ positive semidefinite. A mixed state (density matrix) is a positive semidefinite operator $\rho$ with $\operatorname{Tr}\rho = 1$ ; outcome $M$ occurs with probability $\operatorname{Tr}(M\rho)$ .

An implementation of the measurement on a quantum computer, as the paper fixes it, takes the input $\rho$ , attaches $a$ ancilla qubits in the state $|0\rangle^{\otimes a}$ , applies a unitary $U$ to system and ancillas, measures in the computational basis, and accepts when the last qubit reads $|0\rangle$ :

\rho \to \rho\otimes|0\rangle\langle 0|^{\otimes a} \to U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger \to \operatorname{Tr}\Big((I\otimes|0\rangle\langle 0|)\,U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger\Big).

The implementation has bias at most $\varepsilon$ if, for every state $\rho$ ,

\Big|\operatorname{Tr}\Big((I\otimes|0\rangle\langle 0|)\,U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger\Big) - \operatorname{Tr}(M\rho)\Big| \le \varepsilon. \qquad (14)

Write $K = (I\otimes\langle 0|^{\otimes a})\,U^\dagger(I\otimes|0\rangle\langle 0|)U\,(I\otimes|0\rangle^{\otimes a})$ , an operator on the system. A unitary $V$ on $a'$ ancilla qubits and the system is an $(\alpha, a', \varepsilon)$ -block-encoding of $A$ (Definition 2) if $\|A - \alpha(\langle 0|^{\otimes a'}\otimes I)V(|0\rangle^{\otimes a'}\otimes I)\| \le \varepsilon$ in the operator norm. Finally $U' = U\otimes I_2$ adds one fresh qubit, and $I\otimes\mathrm{CNOT}$ is a CNOT gate whose control is the measured qubit and whose target is the fresh qubit.

Formalization targets

Goal (§4.1, p. 25)

\text{(14)} \;\Longrightarrow\; U'^\dagger(I\otimes\mathrm{CNOT})U' \text{ is a } (1,\ a+1,\ \varepsilon)\text{-block-encoding of } M .

The subnormalization is $1$ , the ancilla count is $a' = a + 1$ and the error is the same $\varepsilon$ as the bias; none of these is weakened.

Milestones (all p. 25, in the order of the derivation)

The trace identity: $\rho\otimes|0\rangle\langle 0|^{\otimes a} = (I\otimes|0\rangle^{\otimes a})\rho(I\otimes\langle 0|^{\otimes a})$ , hence the acceptance probability equals $\operatorname{Tr}(K\rho)$ .
The equivalence $\forall\rho:\ |\operatorname{Tr}([K - M]\rho)| \le \varepsilon \iff \|K - M\| \le \varepsilon$ , with $\rho$ over density matrices.
The CNOT identity $K = (I\otimes\langle 0|^{\otimes a'})\,U'^\dagger(I\otimes\mathrm{CNOT})U'\,(I\otimes|0\rangle^{\otimes a'})$ .

Significance

The result. It converts an operational primitive, performing a measurement, into the input format that block-encoding algorithms consume, with an additive error equal to the measurement's bias and at the cost of one qubit and one CNOT. In the paper it is what makes the shadow-tomography application of §4.1 meaningful: the cost of the SDP solver is stated in terms of block-encodings of the $E_j$ , and this remark lets one replace that by the cost of controlled implementations of the measurements. More generally it shows that the quantum operator model is no stronger than the ability to measure.

Formalizing it. The paper proves the remark in a few displayed lines, one of which ("it is easy to see") is left to the reader and whose CNOT direction is not printed. No machine-checked version exists. A formal proof fixes the register conventions, makes the direction of the CNOT explicit, and contributes a reusable fact about matrices: for a Hermitian $X$ , $\sup_\rho |\operatorname{Tr}(X\rho)| = \|X\|$ over density matrices. The block-encoding predicate itself is already published on the platform and is reused.

Difficulty

The algebra of milestones 1 and 3 is bookkeeping over tensor-product index sets, and the main cost there is choosing representations that make the registers line up.

The one step with mathematical content is the direction " $\Rightarrow$ " of milestone 2. The bias condition controls $|\operatorname{Tr}(X\rho)|$ only for density matrices $\rho$ , that is, it bounds the numerical radius of $X = K - M$ , while a block-encoding needs the operator norm. For a general matrix these differ by up to a factor of two, so the step needs $X$ to be Hermitian: $M$ is Hermitian as a POVM element, and $K$ is Hermitian because it is a compression of the projector $I\otimes|0\rangle\langle 0|$ . A formal proof must use both facts and exhibit a state that attains the norm.

Formalization scope

The Lean development lives in the namespace QuantumSDP18.MeasureBE. Its conventions are:

The system register is an arbitrary finite type $\iota$ (a $w$ -qubit system is $\iota = \{0,1\}^w$ ). Operators are complex matrices; $\dagger$ is the conjugate transpose; the operator norm is the platform's QAlgorithms.specNorm.
The ancilla register is Qubits c × Bool, so $a = c + 1 \ge 1$ and the Bool factor is the last, measured qubit. The basis state $|0\rangle$ of any register is its all-false index.
(14) ranges over all density matrices (PosSemidef with trace $1$ ), and its absolute value is the modulus of a complex trace.
The CNOT is the platform's QAlgorithms.cnot (control first), placed on the measured qubit (control) and the fresh qubit (target). With the opposite direction the block is $U^\dagger U$ and the goal is false; the chosen direction is the only reading under which the page's identity holds.
The block-encoding predicate is the platform's QAlgorithms.IsBlockEncoding, which puts the ancilla register first, as Definition 2 does; the circuit, written system-first as on p. 25, is reindexed to match.
Added hypothesis: $\varepsilon \ge 0$ (a bias is nonnegative). It matters only for a zero-dimensional system, where (14) holds vacuously.

The goal keeps both POVM hypotheses ( $M \succeq 0$ and $I - M \succeq 0$ ), and the bias condition quantifies over all states rather than one fixed state, under which the conclusion would be false. A formalization in which (14) ranges over arbitrary matrices, or which drops the CNOT and states only $\|K - M\| \le \varepsilon$ , is a different theorem.

Needed infrastructure: Kronecker products and reindexing of matrices, the unitarity of permutation matrices and of Kronecker products, and the variational characterization of the operator norm of a Hermitian matrix through its eigenvectors. The last is reusable beyond this mission. Proofs of the three milestones are welcome independently.

Selected references

J. van Apeldoorn, A. Gilyén, Improvements in quantum SDP-solving with applications, arXiv preprint, 2018 (ICALP 2019). https://arxiv.org/abs/1804.05058
G. H. Low, I. L. Chuang, Hamiltonian simulation by qubitization, arXiv preprint, 2016 (Quantum 3, 163, 2019). https://arxiv.org/abs/1610.06546
G. H. Low, I. L. Chuang, Hamiltonian simulation by uniform spectral amplification, arXiv preprint, 2017. https://arxiv.org/abs/1707.05391
S. Aaronson, Shadow tomography of quantum states, STOC 2018. https://arxiv.org/abs/1711.01053

8 thms3 active usersReviewed

Control Theory Convex Optimization Optimization·Captain: mikedeng1

Quadratic Matrix Inequalities with Applications to Data-Based Control IV: Noisy Data Are Informative for Quadratic Stabilization iff an LMI in (P, L, β) Is FeasibleResearch Paper

Motivation

Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by unknown process noise, many systems explain the same data, and a controller designed from the data alone is only trustworthy if it stabilizes every one of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) show that this robust design problem is an implication between two quadratic matrix inequalities (QMIs), and they develop matrix versions of Yakubovich's S-lemma and of Finsler's lemma to decide such implications by a linear matrix inequality (LMI).

Timeline:

1971: Yakubovich proves the S-lemma for one quadratic constraint under a Slater condition (English translation 1977; see the Pólik–Terlaky survey).
2022: van Waarde, Camlibel and Mesbahi (IEEE Trans. Automat. Control 67, pp. 162–175, Thms. 13–14) give an LMI condition for informativity for quadratic stabilization from noisy data, assuming $\Phi_{22}<0$ and a generalized Slater condition.
2023: the present paper removes the Slater condition and the definiteness of $\Phi_{22}$ : Theorem 5.1 holds for every noise model in the class $\boldsymbol\Pi_{n,T}$ , including exact measurements and noise confined to a subspace.

Setting

All matrices are real. $\mathbb{S}^k$ is the set of symmetric $k\times k$ matrices; $A\geqslant 0$ ( $A>0$ ) means $A$ is symmetric positive semidefinite (definite), and $A\leqslant 0$ means $-A\geqslant 0$ .

QMI solution sets. For $\Pi\in\mathbb{S}^{q+r}$ partitioned with $\Pi_{11}\in\mathbb{S}^q$ , $\Pi_{22}\in\mathbb{S}^r$ ,

\mathcal Z_r(\Pi)=\Big\{Z\in\mathbb{R}^{r\times q}:\begin{bmatrix}I_q\\Z\end{bmatrix}^{\!\top}\Pi\begin{bmatrix}I_q\\Z\end{bmatrix}\geqslant 0\Big\},

with $\mathcal Z_r^+(\Pi)$ and $\mathcal Z_r^0(\Pi)$ defined by " $>0$ " and " $=0$ ". The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$ , with $\dagger$ the Moore–Penrose pseudo-inverse, and $\boldsymbol\Pi_{q,r}$ is the class of $\Pi\in\mathbb{S}^{q+r}$ with $\Pi_{22}\leqslant 0$ , $\Pi\,|\,\Pi_{22}\geqslant 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$ .

Data. The unknown system is $x(t+1)=A_sx(t)+B_su(t)+w(t)$ with $x,w\in\mathbb{R}^n$ , $u\in\mathbb{R}^m$ . The measured data are $X=[x(0)\ \cdots\ x(T)]$ and $U_-=[u(0)\ \cdots\ u(T-1)]$ ; $X_-$ and $X_+$ are the first and last $T$ columns of $X$ . The unknown noise $W_-=[w(0)\ \cdots\ w(T-1)]$ satisfies $W_-^\top\in\mathcal Z_T(\Phi)$ for a given $\Phi\in\boldsymbol\Pi_{n,T}$ . The systems compatible with the data form

\Sigma=\{(A,B): X_+=AX_-+BU_-+W_- \text{ for some } W_- \text{ with } W_-^\top\in\mathcal Z_T(\Phi)\},

and $(A_s,B_s)\in\Sigma$ . The data are informative for quadratic stabilization (Definition 2.1) if some $K$ and $P>0$ satisfy $P-(A+BK)P(A+BK)^\top>0$ for all $(A,B)\in\Sigma$ .

Formalization targets

Goal: Theorem 5.1

Let $\mathcal L_\beta(P,L)$ be the $(n+n+m+n)$ -square matrix

\begin{bmatrix}P-\beta I&0&0&0\\0&-P&-L^\top&0\\0&-L&0&L\\0&0&L^\top&P\end{bmatrix}-\begin{bmatrix}I&X_+\\0&-X_-\\0&-U_-\\0&0\end{bmatrix}\Phi\begin{bmatrix}I&X_+\\0&-X_-\\0&-U_-\\0&0\end{bmatrix}^{\!\top}.

For $\Phi\in\boldsymbol\Pi_{n,T}$ and data generated by the system:

(a) the data are informative if and only if $\exists\,P>0,\ L,\ \beta>0$ with $\mathcal L_\beta(P,L)\geqslant 0$ (5.5);

(b) if moreover $\Phi_{22}<0$ and $\operatorname{rank}[X_-;U_-]=n+m$ , the data are informative if and only if $\exists\,P>0,\ L$ with $\mathcal L_0(P,L)>0$ (5.6);

(c) whenever (5.5) or (5.6) holds, $K=LP^{-1}$ satisfies the Lyapunov inequality with that $P$ and makes $A+BK$ Schur stable for every $(A,B)\in\Sigma$ .

Milestones

The vector S-lemma, strict S-lemma and Finsler's lemma (Lemmas 4.1–4.3); the completion and lifting lemmas 4.4–4.5; the reduction of matrix inclusions to vector implications (Theorem 4.6); the matrix S-lemmas

\mathcal Z_r(N)\subseteq\mathcal Z_r(M)\iff\exists\,\alpha\geqslant 0:\ M-\alpha N\geqslant 0,\qquad \mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)\iff\exists\,\alpha\geqslant 0,\ \beta>0:\ M-\alpha N\geqslant\begin{bmatrix}\beta I&0\\0&0\end{bmatrix}

(Theorems 4.7, 4.10–4.12, Corollary 4.13); and the three claims of §5.1 that put Theorem 5.1 in the form of Corollary 4.13: $\Sigma=\mathcal Z_{n+m}(N)$ , the Lyapunov inequality is $[A\ B]^\top\in\mathcal Z^+_{n+m}(M)$ , and $N\in\boldsymbol\Pi_{n,n+m}$ , $M_{22}\leqslant 0$ .

Significance

Theorem 5.1(a) is an exact test, with no rank condition on the data and no Slater condition on the noise model, for the existence of one state-feedback gain with a common quadratic Lyapunov function that stabilizes every system consistent with noisy data. The test is a semidefinite feasibility problem in $(P,L,\beta)$ and returns the controller $K=LP^{-1}$ . It covers energy bounds, per-sample bounds, sample-covariance bounds, noise in a known subspace and exact data within one statement, and its matrix S-lemmas are the tools reused in the paper's further results (the reduced LMI and explicit gain of §5.2, Petersen's lemma in §4.5).

None of these results has a machine-checked proof. Mathlib has the Loewner order, positive (semi)definiteness and spectral theory of symmetric matrices, but no S-lemma, no Finsler lemma, no Moore–Penrose pseudo-inverse for matrices and no theory of QMI solution sets. A formalization would supply these as reusable linear-algebra results and would certify the design rule $K=LP^{-1}$ .

Difficulty

The "if" directions are direct computations: multiply out a Schur complement. The difficulty is in the "only if" directions. The S-lemma's converse relies on the hidden convexity of the joint range of two quadratic forms (Dines' theorem), which is not a consequence of finite-dimensional convex duality alone. Passing from matrices $Z$ to vectors requires Lemma 4.5, which builds a full matrix solution of the QMI from one vector; it uses the pseudo-inverse factorization of $N$ and fails without $\ker N_{22}\subseteq\ker N_{12}$ . In Theorem 4.11 the existence of the margin $\beta>0$ comes from a compactness argument on an unbounded solution set, after splitting off the kernel of $N_{22}$ . The obvious approach, applying the strict matrix S-lemma (Theorem 4.10) directly, does not work because $N_{22}$ is only semidefinite in the noise models of interest.

Formalization scope

Matrices are Matrix ι ι ℝ over finite index types; a matrix in $\mathbb{S}^{q+r}$ is indexed by ι ⊕ κ, and block matrices are Matrix.fromBlocks / Matrix.fromRows. $\geqslant 0$ and $>0$ are Mathlib's PosSemidef and PosDef, which include symmetry, as the paper's §1.1 convention does. The pseudo-inverse is defined as the unique matrix satisfying the four Penrose conditions, not Matrix.inv, which returns $0$ on singular matrices. "Stabilizing gain for all of $\Sigma$ " is stated as the Lyapunov inequality with the LMI's $P$ together with $(A+BK)^k\to 0$ .

The following are added or made explicit:

the hypothesis that the data are generated by the system ( $\Sigma\neq\emptyset$ ). Without it informativity holds vacuously and the goal is false;
$q\geqslant 1$ in the "only if" parts of Theorem 4.12 and Corollary 4.13. These parts fail at $q=0$ , e.g. for $N=[0]$ , $M=[-1]$ , and the paper's proofs choose a nonzero vector of $\mathbb{R}^q$ ;
$n=k+1$ in Lemma 4.4, to avoid natural-number subtraction.

The goal adds no hypothesis $n\geqslant 1$ . A formalization in which $\Sigma$ may be empty, or in which the pseudo-inverse is a junk value, would be trivial or false, and the definitions rule both out.

Contributions are welcome for the pseudo-inverse API (existence, uniqueness, $\ker$ identities), the S-lemma and Finsler's lemma (reusable beyond this mission), and the Schur-complement factorizations (3.2)–(3.4). Platform items ConvexOptimization.s_procedure (inhomogeneous S-procedure) and ConvexOptimization.field_of_values_psd_witness (Dines) are natural proof tools for Lemma 4.1.

Selected references

H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023. arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
H. J. van Waarde, M. K. Camlibel, M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022), pp. 162–175.
I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007). https://doi.org/10.1137/S003614450444614X
V. A. Yakubovich, S-procedure in nonlinear control theory, Vestnik Leningrad Univ. Math. 4 (1977), pp. 73–93 (English translation).
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

17 thms3 active usersReviewed

Completed

Dynamical Systems·Captain: mikedeng1

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 2: Chains to the Rows of Sum ≥ 1 of a Super-Stochastic F Give ρ(F) < 1 under Condition (2.5)Research Paper

Why spectral bounds for super-stochastic matrices

Discrete-time linear iterations $x(k+1)=Fx(k)$ with entrywise nonnegative $F$ appear wherever a quantity is redistributed along the edges of a network: consensus and tracking protocols for multi-agent systems, positive switched systems, and Markov-type averaging schemes. Such an iteration converges to zero exactly when the spectral radius $\rho(F)$ , the largest modulus of an eigenvalue, is less than one. For a sub-stochastic matrix (all row sums at most one) the classical bound $\rho(F)\le\|F\|_\infty\le 1$ settles marginal stability, and strict stability needs only one row of sum below one that "reaches" the others.

Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) study bipartite tracking over signed networks, where asynchronous updates and larger step sizes produce iteration matrices with some row sums above one. For these matrices the norm bound is useless: $\|F\|_\infty>1$ . Their §2.2 introduces super-stochastic matrices and gives conditions under which the spectral radius is nevertheless below one. These conditions are what the later sections use to allow larger control gains than a sub-stochastic analysis permits. This mission formalizes the main spectral result for a single super-stochastic matrix, Theorem 2.6, together with its companions Theorem 2.7 and Theorem 2.8 (products).

Setting

Let $F=[f_{ij}]$ be a real $n\times n$ matrix. Its $i$ -th row sum is $\Lambda_i[F]=\sum_{j=1}^n f_{ij}$ , and its infinity norm is $\|F\|_\infty=\max_i\sum_j|f_{ij}|$ . The eigenvalues of $F$ are complex numbers, and $\rho(F)$ is the largest of their moduli.

$F$ is super-stochastic (Definition 2.5) if $f_{ij}\ge0$ for all $i,j$ and there is a set $\mathcal W_1$ of rows with $\Lambda_i[F]\ge1$ for $i\in\mathcal W_1$ and $\Lambda_i[F]<1$ otherwise. The rows split into

\mathcal R_1=\{s\mid\Lambda_s[F]<1\},\qquad \mathcal R_2=\{s\mid\Lambda_s[F]\ge1\}.

A non-zero element chain from row $i$ to row $k$ is a list of entries $\mathcal C_{i\to k}=[F]_{ki_r},\dots,[F]_{i_2i_1},[F]_{i_1i}$ , all non-zero, with consecutive indices distinct; $|\mathcal C_{i\to k}|=r+1$ is its number of elements. The theorem assumes one chain $\mathcal C_{i\to k}$ from some $i\in\mathcal R_1$ for each $k\in\mathcal R_2$ , and $|\mathcal C^*|$ is the largest number of elements among these chains. The constants are

\alpha_1=\max\{\Lambda_s[F]\mid\Lambda_s[F]<1\},\quad \alpha_2=\min\{[F]_{ij}\mid[F]_{ij}>0\},\quad \alpha_3=\max\{\Lambda_s[F]\mid\Lambda_s[F]\ge1\}.

For a sequence $F_1,\dots,F_q$ , the product is ordered with later factors on the left, $\prod_{s=1}^qF_s=F_q\cdots F_1$ .

Formalization targets

Goal: Theorem 2.6 (p. 9)

If $\mathcal R_1$ and $\mathcal R_2$ are non-empty, the chains exist, and

\sqrt[|\mathcal C^*|]{\alpha_3^{|\mathcal C^*|+1}-(\alpha_3-\alpha_1)\alpha_2^{|\mathcal C^*|}}<1, \tag{2.5}

then

\rho(F)<1 .

Milestones (the steps of the proof on p. 9)

At the end $k$ of a chain of $r+1$ elements starting in $\mathcal R_1$ : $\Lambda_k[F^{r+2}]\le\alpha_3^{r+2}-(\alpha_3-\alpha_1)\alpha_2^{r+1}$ .
For every $k\in\mathcal R_2$ : $\Lambda_k[F^{|\mathcal C^*|+1}]\le\alpha_3^{|\mathcal C^*|+1}-(\alpha_3-\alpha_1)\alpha_2^{|\mathcal C^*|}<1$ .
The same bound for every $i\in\mathcal R_1$ .
$\|F^{|\mathcal C^*|+1}\|_\infty\le\alpha_3^{|\mathcal C^*|+1}-(\alpha_3-\alpha_1)\alpha_2^{|\mathcal C^*|}<1$ .
The general fact $|\mu|^m\le\|A^m\|_\infty$ for every eigenvalue $\mu$ of a real square matrix $A$ (quoted on p. 5).

Companion results

Theorem 2.7 (p. 9). If $[F]_{ii}=0$ for all $i$ and $\mathcal R_2$ has exactly one element, then $\rho(F)\le\sqrt{\alpha_1\alpha_3}$ .
Theorem 2.8 (pp. 10–11), pinned reading. For super-stochastic $F_1,\dots,F_q$ with positive diagonals, with $g$ the largest row sum above one, $c$ the largest row sum below one and $\varphi$ the least positive entry, the condition $g^q-(g-c)\varphi^{q-1}<1$ gives $\Lambda_{i_2}[\prod_sF_s]<1$ for every row $i_2$ fed by an earlier deficient row, and $\rho(\prod_sF_s)<1$ if every row is so fed.

Significance

Theorem 2.6 is a stability criterion that applies when the standard norm test fails because some row sums exceed one. The criterion is computable: it needs only the row sums, the smallest positive entry and the lengths of paths in the directed graph of $F$ from rows of sum below one to the remaining rows. Theorem 2.8 extends this to products, which is the form needed for switched systems in which every subsystem may be individually unstable ( $\rho(F_s)>1$ ) while the periodic product is stable. The paper's tracking results for second-order and general linear agents (§§5–13) use these product bounds.

On the formal side, Mathlib has the spectrum of a matrix, Gershgorin's circle theorem and the norm on matrices, but no bounds on the spectral radius in terms of row sums along paths, and nothing on sub- or super-stochastic matrices. None of these results has a machine-checked proof. The mission produces the first formal version of these chain arguments and a reusable eigenvalue–norm inequality for real matrices.

Difficulty

The obvious argument — $\rho(F)\le\|F\|_\infty$ — fails at once, because $\|F\|_\infty=\alpha_3\ge1$ . One has to pass to a power $F^{m}$ and show that every row sum of $F^m$ drops below one. For the rows of $\mathcal R_2$ the drop comes only from the deficit of a row of $\mathcal R_1$ , transported along a chain whose length varies from row to row; the bound must be made uniform in the length, which is where $|\mathcal C^*|$ and the exponents $|\mathcal C^*|+1$ enter, and where the growth factor $\alpha_3>1$ competes with the gain $(\alpha_3-\alpha_1)\alpha_2^{|\mathcal C^*|}$ . Formally, the induction mixes matrix powers, row sums of products and the indexing of chains. The final step needs the inequality between eigenvalues of $F$ , viewed over $\mathbb C$ , and the infinity norm of a power of $F$ , which is not available in Mathlib in this form.

Formalization scope

All statements live in the namespace SubSuperStoch.SuperSpec. Matrices are Matrix (Fin n) (Fin n) ℝ with $0$ -based indices. Row sums, the infinity norm (a supremum over Fin n, equal to $0$ when $n=0$ ), the complex spectrum, chains, super-stochasticity and ordered products are defined in one definitions file. Committed conventions:

Eigenvalues are the spectrum of $F$ as a complex matrix; $\rho(F)<1$ is stated as $|\mu|<1$ for every eigenvalue $\mu$ . A real spectrum or a real supremum of eigenvalue moduli is not used, since either would miss complex eigenvalues or take a junk value.
Extrema $\alpha_1,\alpha_2,\alpha_3,|\mathcal C^*|,g,c,\varphi$ are values with hypotheses that they are the greatest or least element of exactly the printed set, so no default value for an empty set can enter.
Chains are given by a length function on rows; $|\mathcal C^*|$ is its greatest value over $\mathcal R_2$ , the chains being the ones the hypothesis supplies.
The root in (2.5) is the real power $x^{1/|\mathcal C^*|}$ . Its radicand is nonnegative under the hypotheses, and (2.5) is equivalent to $\alpha_3^{|\mathcal C^*|+1}-(\alpha_3-\alpha_1)\alpha_2^{|\mathcal C^*|}<1$ .
$\mathcal W_1\subset\{1,\dots,n\}$ in Definition 2.5 is read as a subset that may be all rows, as the paper's own examples require; condition 2) then fixes vocabulary only.
Theorem 2.8 is stated with $\varphi$ the least positive entry, as in Lemma 5.4 (p. 25). The printed $\varphi$ , the least entry overall, is $0$ for any family with a zero entry and turns (2.7) into $g^q<1$ , which is impossible as $g>1$ ; that version would be vacuous. The row claim and the spectral claim carry the quantifiers their proofs need (the existence hypothesis for one row, respectively for every row).
The proof of Theorem 2.6 ends with $\rho(F)\le\sqrt[|\mathcal C^*|]{\cdots}$ , a $|\mathcal C^*|$ -th root of a bound on $\|F^{|\mathcal C^*|+1}\|_\infty$ . That display is not a target; the theorem claims only $\rho(F)<1$ .
Theorem 2.7 claims no " $<1$ " and none is added.

A trivializing formalization is excluded: the hypotheses are satisfied by the paper's own example $\tilde F$ on p. 9 ( $\alpha_1=0.6$ , $\alpha_2=0.5$ , $\alpha_3=1.05$ , $|\mathcal C^*|=1$ , radicand $0.8775$ ), checked in Lean.

Contributions welcome: proofs of the milestones, the general eigenvalue–norm inequality (reusable for any spectral-radius argument over real matrices), and the two companion theorems.

Selected references

L. Shi, W. X. Zheng, J. Shao, Y. Cheng, Sub/super-stochastic matrix with applications to bipartite tracking control over signed networks, arXiv:2004.01867v2, 2020; SIAM J. Control Optim., 2021. https://arxiv.org/abs/2004.01867 , https://doi.org/10.1137/19M1239982
R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013 (spectral radius and induced norms, Ch. 5). https://doi.org/10.1017/CBO9781139020411

8 thms3 active usersReviewed

Completed

Captain: mikedeng1

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 1: Chains to the Unit Rows of a Sub-Stochastic F Give ρ(F) ≤ (1 − (1 − α₁)α₂^|C|)^(1/(|C|+1)) < 1Research Paper

Motivation

In distributed control, many convergence questions come down to one test: is the spectral radius of a nonnegative iteration matrix strictly below one? Consensus and tracking protocols for multi-agent systems (MASs) produce such matrices. The agents that hear the leader directly give rows whose sum is below one, and the agents that only average their neighbours give rows that sum to exactly one. When the agents update asynchronously, the matrices change from step to step, and eigenvalue computations on each matrix give little insight. Conditions read off the sign pattern and row sums of the matrix are much easier to use.

Shi, Zheng, Shao and Cheng (arXiv:2004.01867, SIAM J. Control Optim. 2021) develop such conditions for sub-stochastic and super-stochastic matrices. They then apply them to asynchronous bipartite tracking over signed networks: agents that cooperate or compete must track a leader's state or its negative. This mission covers the first block of results, the spectral bounds for sub-stochastic matrices in §2.2 (pp. 4–6). The classical background is the Perron–Frobenius theory of nonnegative matrices and the convergence analysis of products of stochastic matrices in consensus problems (Ren–Beard 2005).

Setting

Let $F=[f_{ij}]\in\mathbb R^{n\times n}$ . Write $\Lambda_i[F]=\sum_{j=1}^n f_{ij}$ for the row sum of row $i$ , and $\|F\|_\infty=\max_i\sum_j|f_{ij}|$ for the infinite norm. $\rho(F)$ is the spectral radius, the largest modulus of a complex eigenvalue of $F$ .

$F$ is sub-stochastic (Definition 2.1) if $f_{ij}\ge 0$ for all $i,j$ and $\Lambda_i[F]\le 1$ for every $i$ . Its rows split into

\mathcal S_1=\{s\mid \Lambda_s[F]<1\},\qquad \mathcal S_2=\{s\mid \Lambda_s[F]=1\}.

Two numbers measure how far $F$ is from stochastic:

\alpha_1=\max\{\Lambda_s[F]\mid \Lambda_s[F]<1\},\qquad \alpha_2=\min\{[F]_{ij}>0\mid i,j=1,\dots,n\},

the largest row sum below one and the smallest positive entry.

A non-zero element chain $\mathcal C_{i\to k}$ from $i$ to $k$ is a list of entries

[F]_{k i_r},\ \dots,\ [F]_{i_2 i_1},\ [F]_{i_1 i}

that are all non-zero, with consecutive indices distinct ( $i\ne i_1$ , $i_1\ne i_2$ , …, $i_r\ne k$ ). Each entry has the later index as its row. The chain's number of elements is $|\mathcal C_{i\to k}|=r+1$ . If for each $k\in\mathcal S_2$ a chain $\mathcal C_{i\to k}$ with $i\in\mathcal S_1$ is given, $|\mathcal C^*|$ is the largest number of elements among them.

In the Lean development these are rowSum F i, normInf F, specC F (the complex spectrum), IsSubStochastic F and IsChain F c L, all in the file SubSuperStoch.SubSpec.Setting.

Formalization targets

Goal: Theorem 2.2 (pp. 4–5)

If $F$ is sub-stochastic, $\mathcal S_1$ and $\mathcal S_2$ are non-empty, and every $k\in\mathcal S_2$ is the end of a non-zero element chain starting in $\mathcal S_1$ , then

\rho(F)\le\sqrt[|\mathcal C^*|+1]{1-(1-\alpha_1)\alpha_2^{|\mathcal C^*|}}<1. \tag{2.1}

Milestones: the steps of the proof (p. 5)

At the end $k$ of a chain of $r+1$ elements that starts in $\mathcal S_1$ : $\Lambda_k[F^{r+2}]\le 1-(1-\alpha_1)\alpha_2^{r+1}<1$ .
For every $k\in\mathcal S_2$ : $\Lambda_k[F^{|\mathcal C^*|+1}]\le 1-(1-\alpha_1)\alpha_2^{|\mathcal C^*|}<1$ .
For every $i\in\mathcal S_1$ : $\Lambda_i[F^{|\mathcal C^*|+1}]\le 1-(1-\alpha_1)\alpha_2^{|\mathcal C^*|}$ .
$\|F^{|\mathcal C^*|+1}\|_\infty\le 1-(1-\alpha_1)\alpha_2^{|\mathcal C^*|}<1$ .
The two facts the proof cites as known: for every real square matrix $A$ and every complex eigenvalue $\mu$ , $|\mu|^m\le\|A^m\|_\infty$ , i.e. $\rho(A)^m=\rho(A^m)\le\|A^m\|_\infty$ .

Companion: Theorem 2.3 (pp. 5–6)

If $F$ is sub-stochastic, $[F]_{ii}=0$ for all $i$ , and $\mathcal S_2$ has exactly one element, then

\rho(F)\le\sqrt{\alpha_1}<1. \tag{2.2}

Its proof uses the eigenvector bounds (2.3) $|\lambda|\le\Lambda_p[F]|x_q|/|x_p|$ and (2.4) $|\lambda|\le\Lambda_q[F]|x_p|/|x_q|$ for the two largest coordinates $x_p,x_q$ of an eigenvector. These bounds are also drafted, with the denominators cleared.

Significance

Theorem 2.2 replaces an eigenvalue computation with a reachability check on the zero pattern of $F$ together with two scalar quantities, and the bound it gives is explicit. In the paper it is the basic tool for the products of sub-stochastic matrices (Theorem 2.4) and for the convergence of asynchronous bipartite tracking over signed digraphs (§3 onward). In that setting, "every row of sum one is reached by a chain from a row of sum below one" becomes "every follower is reachable from the leader." Theorem 2.3 covers matrices with a zero diagonal and a single unit row, and there the bound needs no chain condition at all.

The results are proved in the paper. Nothing in this mission is formalized anywhere we know of. Mathlib has Gershgorin's circle theorem and the spectrum of a matrix, but it has no row-sum or chain criterion for nonnegative matrices and no stated link between the spectral radius of a power and its infinite norm. A complete formalization would supply a reusable stability criterion for nonnegative matrices, a statement of $\rho(A)^m\le\|A^m\|_\infty$ in eigenvalue form, and machine-checked versions of the inequalities that the paper's control results rest on.

Difficulty

The obvious first idea is to bound $\rho(F)$ by $\|F\|_\infty$ . That fails: whenever $\mathcal S_2$ is non-empty, $\|F\|_\infty=1$ , so it only gives $\rho(F)\le 1$ . Strict stability cannot be seen in any single row of $F$ . Each unit row only becomes deficient after the deficit of a row in $\mathcal S_1$ has propagated to it along a chain, and this happens at different powers for different rows. The proof needs one power that works for every row at once, and it has to control how the deficit decays (a factor of $\alpha_2$ per chain element). For Theorem 2.3 the difficulty is different: no power of $F$ need have norm below one, so the argument has to work with an eigenvector directly.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ with 0-based indices. $\rho(F)\le b$ is stated as $|\mu|\le b$ for every $\mu$ in the complex spectrum of $F$ , never as a real supremum and never over real eigenvalues only. $\alpha_1$ , $\alpha_2$ and $|\mathcal C^*|$ are passed as values together with IsGreatest/IsLeast hypotheses over exactly the printed sets, so an empty set cannot produce a default value. The hypothesis "there exist chains for each $k\in\mathcal S_2$ " is encoded with a length function len: for every unit row $k$ there is a chain of len k elements from some deficient row to $k$ , and $|\mathcal C^*|$ is the largest len k over the unit rows, i.e. the longest of the chosen chains. The $(|\mathcal C^*|+1)$ -st root is the real power $x^{1/(|\mathcal C^*|+1)}$ .

The formalization does not assume $\|F\|_\infty<1$ , and it does not assume that every row lies in $\mathcal S_1$ . Either assumption would make the goal a one-line consequence of the norm bound. The chain direction is fixed (the entry $[F]_{i_{t+1}i_t}$ has row $i_{t+1}$ ), and $\alpha_2$ is the least positive entry; a chain in the opposite direction, or the least entry overall, gives a different statement.

Needed infrastructure: row sums of powers of nonnegative matrices, the relation $\mu\in\sigma(A)\Rightarrow\mu^m\in\sigma(A^m)$ , and Gershgorin's theorem applied to $\|A^m\|_\infty$ . The eigenvalue-power bound and the chain bound are reusable outside this paper. Proofs of any milestone are welcome, as are alternative proofs of Theorem 2.3.

Selected references

L. Shi, W. X. Zheng, J. Shao, Y. Cheng, Sub/super-stochastic matrix with applications to bipartite tracking control over signed networks, arXiv:2004.01867v2, 2020; SIAM J. Control Optim., 2021 (DOI 10.1137/19m1239982). https://arxiv.org/abs/2004.01867
W. Ren, R. W. Beard, Consensus seeking in multiagent systems under dynamically changing interaction topologies, IEEE Trans. Automat. Control 50 (2005) 655–661. https://doi.org/10.1109/TAC.2005.846556
R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139020411

7 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

From Differential Equation Solvers to Accelerated First-Order Methods for Convex Optimization 1: Gauss–Seidel Splitting of the HB and NAG Transforms Has ρ(E(α, G)) ≤ 1/√(1 + 2α) If 0 < α ≤ 2/√κ(A)Research Paper

Motivation

Accelerated first-order methods, the heavy-ball method of Polyak and Nesterov's accelerated gradient (NAG) method, reach an error $\varepsilon$ on a $\mu$ -strongly convex, $L$ -smooth problem in $O(\sqrt{\kappa}\log(1/\varepsilon))$ gradient steps, $\kappa=L/\mu$ , against $O(\kappa\log(1/\varepsilon))$ for plain gradient descent. A long line of work has tried to explain where this square root comes from by reading the methods as discretizations of ordinary differential equations: Su, Boyd and Candès (arXiv:1503.01243), Wibisono, Wilson and Jordan (arXiv:1603.04245), and others.

Luo and Chen (arXiv:1909.03145, Math. Program. 2022) take the view from numerical analysis. Section 2 of their paper treats the quadratic case: the gradient flow $x'=-Ax$ is stiff, and an explicit scheme for it needs step size $O(1/\kappa(A))$ . They embed $A$ in a $2\times2$ block matrix $G$ whose spectrum lies in the left half-plane with condition number $\sqrt{\kappa(A)}$ , and they show that an explicit Gauss–Seidel splitting scheme for $y'=Gy$ is stable with step size of order $1/\sqrt{\kappa(A)}$ . This is the linear-algebra core of the paper's argument. The later sections build the nonlinear schemes (missions 2–8 of this series) on it.

Setting

Let $A$ be a real symmetric $d\times d$ matrix. Its eigenvalues are real, and we assume

0<\mu=\lambda_{\min}(A)\le\lambda\le\lambda_{\max}(A)=L\qquad\text{for all }\lambda\in\sigma(A),

with condition number $\kappa(A)=L/\mu$ . For any real square matrix $M$ , the spectrum $\sigma(M)$ is the set of its eigenvalues, which are complex in general, and the spectral radius is $\rho(M)=\max_{\lambda\in\sigma(M)}|\lambda|$ .

The two transformations (39) of the paper are the $2d\times2d$ block matrices

G_{\mathrm{HB}}=\begin{pmatrix}0 & I\\ -A/\mu & -2I\end{pmatrix},\qquad G_{\mathrm{NAG}}=\begin{pmatrix}-I & I\\ I-A/\mu & -I\end{pmatrix}.

For the linear system $y'=Gy$ , write $G=M+N$ , where $M$ is the block lower triangular part of $G$ (the two diagonal blocks and the lower-left block) and $N=G-M$ . The Gauss–Seidel splitting scheme (41) with step size $\alpha>0$ is

\frac{y_{k+1}-y_k}{\alpha}=My_{k+1}+Ny_k,\qquad\text{i.e.}\qquad y_{k+1}=E(\alpha,G)\,y_k,\quad E(\alpha,G)=(I-\alpha M)^{-1}(I+\alpha N).

The matrix $I-\alpha M$ is block lower triangular with diagonal blocks that are multiples of $I$ , so the scheme is explicit and never inverts $A$ . A one-step scheme is A-stable if $\rho(E(\alpha,G))<1$ .

Appendix A works with the scalar model $R=\begin{pmatrix}-a&c\\-b&-d\end{pmatrix}$ , where $a,b,c,d\ge0$ and $\operatorname{tr}R<0<\det R$ , and with its Gauss–Seidel matrix $E(\alpha,R)$ , defined in the same way from the lower triangular part of $R$ .

Formalization targets

Goal: Theorem 2.1 (p. 10)

For $G=G_{\mathrm{HB}}$ or $G=G_{\mathrm{NAG}}$ , if $0<\alpha\le2/\sqrt{\kappa(A)}$ , then the scheme is A-stable and

\rho(E(\alpha,G))\le\frac{1}{\sqrt{1+2\alpha}}.

Milestones (Appendix A, pp. 35–36)

(124): the closed form of $E(\alpha,R)$ , and $0<\det E(\alpha,R)=1/(1+|\operatorname{tr}R|\alpha+ad\alpha^2)<1$ .
Lemma A.1: if $|\operatorname{tr}R|-2\sqrt{\det R}\le bc\,\alpha\le|\operatorname{tr}R|+2\sqrt{\det R}$ , then $\rho(E(\alpha,R))=1/\sqrt{1+|\operatorname{tr}R|\alpha+ad\alpha^2}<1$ .
The heavy-ball reduction: a closed block form of $E(\alpha,G_{\mathrm{HB}})$ , and $\sigma(E(\alpha,G_{\mathrm{HB}}))=\bigcup_{\lambda\in\sigma(A)}\sigma(E(\alpha,R(\lambda)))$ with $R(\lambda)=\begin{pmatrix}0&1\\-\lambda/\mu&-2\end{pmatrix}$ .
Heavy-ball spectral radius: under (127), $\rho(E(\alpha,G_{\mathrm{HB}}))=1/\sqrt{1+2\alpha}$ .
NAG spectral radius: under (127), $\rho(E(\alpha,G_{\mathrm{NAG}}))=1/\sqrt{1+2\alpha+\alpha^2}\le1/\sqrt{1+2\alpha}$ .

Companion statements

Proposition 2.1 (p. 9): $\operatorname{Re}\lambda<0$ on $\sigma(G)$ and $\kappa(G_{\mathrm{HB}})=\kappa(G_{\mathrm{NAG}})=\sqrt{\kappa(A)}$ .
The choice $\alpha=2/\sqrt{\kappa(A)}$ (p. 36): $\rho(E(\alpha,G))\le1/\sqrt{1+4/\sqrt{\kappa(A)}}\le1/(1+1/\sqrt{\kappa(A)})$ .

The goal is the weakest of these statements. Milestones 4 and 5 show that it is attained for heavy ball and strict for NAG.

Significance

The result. Theorem 2.1 gives a contraction factor $1/(1+1/\sqrt{\kappa(A)})$ per step for an explicit, matrix-free scheme. Applied to $f(x)=\tfrac12x^\top Ax$ , that is the accelerated linear rate. Eliminating $v$ from $y=(x,v)$ shows that both transformations discretize the same second-order ODE $\mu x''+2\mu x'+\nabla f(x)=0$ . The theorem therefore explains acceleration as a stability property of an ODE solver, not as an algebraic trick. The paper's nonlinear schemes (predictor–corrector, gradient correction, Nesterov's method, the proximal variants) are built from this splitting. Their Lyapunov analyses generalize the spectral computation formalized here.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization has to make the paper's "it is clear that" spectral reduction rigorous: the block diagonalisation through $A=U\Lambda U^\top$ and the identification of the spectrum of a structured $2d\times2d$ non-symmetric matrix with a union of $2\times2$ spectra. It also has to treat spectra of real matrices over $\mathbb C$ . Both are reusable well beyond this paper, since every spectral analysis of a momentum method (heavy ball, NAG, their discretizations) runs through the same reduction.

Difficulty

The obvious route bounds a norm of $E(\alpha,G)$ . It fails: $E(\alpha,G)$ is not normal, and the paper stresses that $\|E\|_2$ is not controlled by $\rho(E)$ . The bound concerns eigenvalues only, and the eigenvalues are complex.

A second naive route applies a Gershgorin or field-of-values estimate to $G$ directly. It loses the square root, because the off-diagonal blocks $A/\mu$ have norm $\kappa(A)$ . The real content is that for each eigenvalue $\lambda$ of $A$ , the $2\times2$ Gauss–Seidel matrix has a negative discriminant exactly when the step-size condition holds. Its eigenvalues are then a conjugate pair on the circle of radius $\sqrt{\det E}$ , and $\det E$ does not depend on $\lambda$ . Reaching this needs three things: the reduction of the block spectrum to scalar spectra, the explicit inverse of $I-\alpha M$ , and a careful equivalence of the discriminant condition with (126).

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℝ, and the block matrices live on Fin d ⊕ Fin d, built with Matrix.fromBlocks.

The splitting. It is blockwise: $M$ takes the two diagonal blocks and the lower-left block of $G$ . That is how the paper's own formula for $E(\alpha,G_{\mathrm{HB}})$ reads it; the entrywise lower triangle would split $A$ itself.
Spectra. The spectrum of a real matrix is spectrum ℂ of its complexification. " $\rho(M)=r$ " is IsGreatest of the set of eigenvalue moduli. " $\rho(M)\le r$ " and " $\rho(M)<1$ " are stated eigenvalue by eigenvalue, so no junk supremum over an empty set can make a bound vacuous.
The model matrix. $\mu=\lambda_{\min}(A)$ and $L=\lambda_{\max}(A)$ are encoded as hypotheses: both are eigenvalues of $A$ and bound every eigenvalue. $\kappa(A)$ is the number $L/\mu$ . Every statement assumes $\mu>0$ , the case of §2.3 where $G_{\mathrm{HB}}$ and $G_{\mathrm{NAG}}$ are defined.
Step size and inverse. The step size satisfies $\alpha>0$ , which the paper leaves implicit in (124). The matrix inverse in $E$ is Mathlib's. It is genuine here, because $I-\alpha M$ is invertible for $\alpha>0$ .

Two trivializations are ruled out explicitly. A spectral radius defined as sSup over a possibly empty spectrum would make every bound hold vacuously at $d=0$ . A spectrum taken over $\mathbb R$ would miss the complex eigenvalues, which are all of them here.

A complete development needs:

block-diagonalisation of the structured block matrices by $\operatorname{diag}(U,U)$ and a permutation;
the spectrum of a block-diagonal matrix of $2\times2$ blocks;
the eigenvalues of a real $2\times2$ matrix with negative discriminant;
explicit $2\times2$ and block-triangular inverses.

Lemmas of this kind, stated for general symmetric $A$ , are welcome as separate theorems.

Selected references

H. Luo, L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Math. Program. 195 (2022); arXiv:1909.03145v4. https://arxiv.org/abs/1909.03145
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, JMLR 17 (2016). https://arxiv.org/abs/1503.01243
A. Wibisono, A. C. Wilson, M. I. Jordan, A variational perspective on accelerated methods in optimization, PNAS 113 (2016). https://arxiv.org/abs/1603.04245
B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4 (1964). https://doi.org/10.1016/0041-5553(64)90137-5
E. Hairer, G. Wanner, Solving Ordinary Differential Equations II: Stiff and Differential-Algebraic Problems, Springer, 1996 (A-stability). https://doi.org/10.1007/978-3-642-05221-7

7 thms3 active usersReviewed

Completed

Combinatorics Optimization Theoretical Computer Science·Captain: mikedeng1

Optimal Approximation for Submodular and Supermodular Optimization with Bounded Curvature II: Column-Subset Selection Has Total Curvature at Most 1 − 1/κ(A)²Research Paper

Why column-subset selection and curvature

The column-subset selection problem (CSSP) asks for $k$ columns of a real matrix $A$ whose span approximates all of $A$ as well as possible in squared Frobenius norm. It is a basic primitive of low-rank approximation, feature selection and numerical linear algebra, studied both for its exact complexity and for approximation algorithms (see Boutsidis, Drineas and Magdon-Ismail, doi:10.1137/12086755X, cited as [2] in the source paper).

Sviridenko, Vondrák and Ward study submodular maximization and supermodular minimization when the objective has bounded total curvature, a parameter $c \in [0,1]$ introduced by Conforti and Cornuéjols that measures how far a monotone set function is from being linear. Their guarantees improve as $c$ decreases. Section 8 of the paper applies this to CSSP: it bounds the curvature of the CSSP objective in terms of the condition number of $A$ , so that a well-conditioned matrix has small curvature. This mission formalizes that bound (Lemma 8.2) and the steps of its proof.

Setting

Let $A$ be a real $m \times n$ matrix with columns $c_1, \dots, c_n \in \mathbb{R}^m$ , so that $Ax = \sum_i x_i c_i$ for $x \in \mathbb{R}^n$ , and let $\|\cdot\|$ be the Euclidean norm. For $S \subseteq [n]$ write $\mathrm{proj}_S(x)$ for the orthogonal projection of $x$ onto $\mathrm{span}\{c_i : i \in S\}$ , the point of that subspace nearest to $x$ ( $\mathrm{proj}_\emptyset = 0$ ). The CSSP objective is

f^A(S) = \sum_{i=1}^n \|c_i - \mathrm{proj}_S(c_i)\|^2 ,

the squared Frobenius distance from $A$ to the nearest matrix whose columns lie in the span of the selected columns.

For a set function $f$ on a finite set $X$ , the marginal value of $i$ at $A$ is $f_A(i) = f(A+i) - f(A)$ . The function $f$ is monotone decreasing if every $f_A(i) \le 0$ . Following (1.1) of the paper, a monotone decreasing $f$ has total curvature at most $c$ when, for every $j \in X$ ,

f_{X-j}(j) \le (1-c)\, f_\emptyset(j),

i.e. the last marginal of $j$ is at least a $(1-c)$ fraction of its first marginal in absolute value.

When the columns of $A$ are linearly independent, the condition number is

\kappa(A) = \frac{\sup_{\|x\|=1}\|Ax\|}{\inf_{\|x\|=1}\|Ax\|} \in [1, \infty).

Formalization targets

Goal: Lemma 8.2 (p. 11)

For $A$ with linearly independent columns,

f^A_{[n]-j}(j) \le \frac{1}{\kappa^2(A)}\, f^A_\emptyset(j) \quad \text{for all } j \in [n], \qquad \text{i.e.}\quad c(f^A) \le 1 - \frac{1}{\kappa^2(A)} .

Milestones

The identity $f^A(S) = \sum_i (\|c_i\|^2 - \|\mathrm{proj}_S(c_i)\|^2)$ (p. 11).
Lemma 8.1, monotone part: $S \mapsto \|\mathrm{proj}_S(v)\|^2$ is monotone increasing (p. 11).
$f^A$ is monotone decreasing (p. 11).
$|f^A_\emptyset(i)| = \sum_j \|\mathrm{proj}_{\{i\}}(c_j)\|^2$ (p. 11).
Some unit $x$ has $\|Ax\| \ge \sqrt{|f^A_\emptyset(i)|}$ (p. 12).
$|f^A_{[n]-i}(i)| = \|c_i - \mathrm{proj}_{[n]-i}(c_i)\|^2$ (p. 12).
Some unit $x'$ has $\|Ax'\| \le \sqrt{|f^A_{[n]-i}(i)|}$ (p. 12).
$\kappa^2(A) \ge f^A_\emptyset(i)/f^A_{[n]-i}(i)$ for each $i$ , under independence (p. 12).

Items 1–7 hold for arbitrary columns; only item 8 and the goal assume independence.

Significance

Lemma 8.2 turns a spectral quantity into a combinatorial one. With it, any curvature-dependent guarantee for monotone decreasing set functions can be stated for CSSP in terms of $\kappa(A)$ . The paper's Lemma 8.3 shows the bound is asymptotically tight, so $1 - \Theta(1/\kappa^2)$ is the right order of the curvature.

There is a caveat that the formalization makes explicit. The paper deduces from Lemma 8.1 that $f^A$ is supermodular, and on that basis quotes its supermodular-minimization algorithm for CSSP with factor $1 + (\kappa^2 - 1)e^{-1} + \kappa^2 O(\epsilon)$ (p. 12). Both the submodularity half of Lemma 8.1 and the supermodularity of $f^A$ are false as printed. With $c_1 = e_1$ , $c_2 = e_1 + e_2$ and $v = e_2$ in $\mathbb{R}^2$ , the function $F(S) = \|\mathrm{proj}_S(v)\|^2$ has $F(\{1,2\}) + F(\emptyset) = 1 > \tfrac12 = F(\{1\}) + F(\{2\})$ . With columns $e_1, e_1+e_2, 2e_2$ , $f^A(\{1\}) + f^A(\{2\}) = \tfrac{15}{2} > 7 = f^A(\{1,2\}) + f^A(\emptyset)$ . A small perturbation gives a counterexample with independent columns. This is the "suppressor variable" phenomenon of regression. The curvature bound itself does not depend on supermodularity and is true, so it is the goal here. The approximation factor for CSSP is not posed, because it rests on the false claim and is stated with $O(\epsilon)$ .

As far as is known, none of these statements has a machine-checked proof. The results are proved on paper, except the two false claims above. The mission adds a formal proof of the curvature–conditioning bound, and makes explicit which parts of §8 survive.

Difficulty

The individual steps are short linear algebra, but they rest on infrastructure that has to be assembled: orthogonal projections onto spans of finite column families, the Pythagorean identities that relate $f^A$ to projections, and the variational characterization of $\sup$ and $\inf$ of $\|Ax\|$ over the unit sphere.

The paper's own route to the large unit vector (milestone 5) does not work as printed. It sets $x_j \propto \|\mathrm{proj}_{\{i\}}(c_j)\|$ and uses $c_i \cdot c_j = \|c_i\|\,\|\mathrm{proj}_{\{i\}}(c_j)\|$ , which is false when $c_i \cdot c_j < 0$ , so the signs of the inner products have to be accounted for. In the final step, the ratio $f^A_\emptyset(i)/f^A_{[n]-i}(i)$ is a quotient of two negative numbers. Comparing it with $\kappa^2$ requires the supremum to be finite and the infimum to be strictly positive, which is exactly what independence of the columns provides.

Formalization scope

Columns are a family c : Fin n → EuclideanSpace ℝ (Fin m), and $Ax$ is ∑ j, x j • c j. Subsets of $[n]$ are Finset (Fin n). $[n] - i$ is Finset.univ.erase i and $S + i$ is insert i S.
$\mathrm{proj}_S$ is Mathlib's Submodule.starProjection onto Submodule.span ℝ (c '' S), which is finite-dimensional, so the argmin of the page exists and is unique.
$\kappa(A)$ is a real quotient of ⨆ and ⨅ of $\|Ax\|$ over the unit-sphere subtype of $\mathbb{R}^n$ . It is used only under LinearIndependent ℝ c, the page's "non-singular", where both are finite and positive. The page's $\kappa = \infty$ for dependent columns is not encoded.
Monotonicity is the marginal form of §2.1. Curvature is the product form above, which agrees with the ratio of (1.1) whenever $f_\emptyset(j) \ne 0$ and avoids Lean's $x/0 = 0$ .
For $n = 0$ the goal has no $j$ and is empty, as on the page.
A trivializing reading is ruled out by the encoding: had $\kappa$ evaluated to a junk value $0$ , the goal would reduce to monotonicity. Under independence the supremum and infimum are genuine, so the bound $1 - 1/\kappa^2$ is the paper's.
Not in scope: Lemma 8.3 (stated with $O(\cdot)$ ), the CSSP approximation factor, and the false submodularity and supermodularity claims.

Useful infrastructure that would be reusable beyond this mission includes Pythagoras for starProjection, monotonicity of projection norms under inclusion of subspaces, and extremal characterizations of $\sup_{\|x\|=1}\|Ax\|$ and $\inf_{\|x\|=1}\|Ax\|$ . Contributions of any of the milestones, or of these general lemmas, are welcome.

Selected references

M. Sviridenko, J. Vondrák, J. Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature, SODA 2015 (version of Oct. 9, 2014); journal version Math. Oper. Res. 42(4), 2017. https://doi.org/10.1287/moor.2016.0842
M. Conforti, G. Cornuéjols, Submodular set functions, matroids and the greedy algorithm: tight worst-case bounds and some generalizations of the Rado–Edmonds theorem, Discrete Appl. Math. 7(3), 1984. https://doi.org/10.1016/0166-218X(84)90003-9
C. Boutsidis, P. Drineas, M. Magdon-Ismail, Near-optimal column-based matrix reconstruction, SIAM J. Comput. 43(2), 2014. https://doi.org/10.1137/12086755X
A. Das, D. Kempe, Submodular meets spectral: greedy algorithms for subset selection, sparse approximation and dictionary selection, ICML 2011. https://arxiv.org/abs/1102.3975

11 thms3 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Optimization-Based Algorithms for Tensor Decompositions: Canonical Polyadic Decomposition, Decomposition in Rank-(Lr, Lr, 1) Terms, and a New Generalization 2: The Cogradient Is ½(Ā·W − T̄·V)Research Paper

Motivation

Tensor decompositions are a standard tool in signal processing, chemometrics, telecommunications and blind source separation. The canonical polyadic decomposition (CPD) writes a tensor as a sum of rank-one tensors; the rank- $(L_r,L_r,1)$ block term decomposition (BTD) replaces each rank-one term by the outer product of a rank- $L_r$ matrix and a vector. Sorber, Van Barel and De Lathauwer (SIAM J. Optim. 23(2), 2013) introduced a common generalization, the (rank- $L_r\circ$ rank-1) BTD, and derived optimization algorithms that compute all three decompositions of complex tensors. Their quasi-Newton and nonlinear conjugate gradient methods are built on complex Taylor models in $z$ and $\bar z$ (Sorber, Van Barel and De Lathauwer, SIAM J. Optim. 22(3), 2012), and each iteration needs the complex cogradient of the least-squares objective. This mission formalizes the closed form of that cogradient, Theorem 4.4 of the paper. The algorithms were released in the MATLAB toolbox Tensorlab.

Setting

Let $\mathcal T\in\mathbb C^{I_1\times\cdots\times I_N}$ be a tensor of order $N=P+Q$ . Fix block sizes $L_1,\dots,L_R$ and put $R'=\sum_r L_r$ . The unknowns are complex matrices $A^{(p)}\in\mathbb C^{I_p\times R'}$ for $1\le p\le P$ and $C^{(q)}\in\mathbb C^{I_{P+q}\times R}$ for $1\le q\le Q$ , collected in the vector

z=(\operatorname{vec}A^{(1)},\dots,\operatorname{vec}A^{(P)},\operatorname{vec}C^{(1)},\dots,\operatorname{vec}C^{(Q)}).

Let $E=\operatorname{diag}(1_{1\times L_1},\dots,1_{1\times L_R})$ be the $R\times R'$ block-diagonal matrix of row vectors of ones. The (rank- $L_r\circ$ rank-1) BTD is read as a structured CPD with $N$ factor matrices

A^{(1)},\dots,A^{(P)},\qquad A^{(P+q)}=C^{(q)}E\quad(1\le q\le Q).

Its residual tensor is $\mathcal F_{\mathrm{BTD}}=\sum_{r'=1}^{R'}a^{(1)}_{r'}\circ\cdots\circ a^{(N)}_{r'}-\mathcal T$ , and the objective is the nonlinear least-squares function

f_{\mathrm{BTD}}=\tfrac12\|\mathcal F_{\mathrm{BTD}}\|^2 ,

with the Frobenius norm induced by $\langle\mathcal T,\mathcal U\rangle=\sum\overline{t_{i_1\cdots i_N}}\,u_{i_1\cdots i_N}$ .

For a set $\sigma$ of modes, $V^\sigma=\bigodot_{n\notin\sigma}A^{(n)}$ is the Khatri–Rao product (column-wise Kronecker product) of the factor matrices outside $\sigma$ , and $W^\sigma=\ast_{n\notin\sigma}A^{(n)\mathrm H}A^{(n)}$ is the Hadamard product of their Gramians. The mode- $n$ unfolding $T_{(n)}$ arranges the mode- $n$ fibres of $\mathcal T$ as columns, ordered like the rows of $V^{\{n\}}$ .

The objective is real-valued, hence not holomorphic in $z$ . The cogradient $\partial f/\partial z$ is the vector of Wirtinger derivatives

\frac{\partial f}{\partial z_\beta}=\frac12\Big(\frac{\partial f}{\partial x_\beta}-\mathrm i\frac{\partial f}{\partial y_\beta}\Big),\qquad z_\beta=x_\beta+\mathrm i y_\beta,

the derivative with respect to $z_\beta$ with $\bar z_\beta$ held constant. Overbars denote entrywise complex conjugation.

Formalization targets

Goal: Theorem 4.4

For every tensor $\mathcal T$ and every $z$ , for $1\le p\le P$ and $1\le q\le Q$ ,

2\,\frac{\partial f_{\mathrm{BTD}}}{\partial A^{(p)}}=\overline{A}^{(p)}\,W^{\{p\}}-\overline{T}_{(p)}\,V^{\{p\}},

2\,\frac{\partial f_{\mathrm{BTD}}}{\partial C^{(q)}}=\overline{C}^{(q)}\,E\,W^{\{P+q\}}\,E^{\mathrm T}-\overline{T}_{(P+q)}\,V^{\{P+q\}}\,E^{\mathrm T}.

The identity (4.4), which assembles $\partial f/\partial z$ from these blocks, holds by construction in the formalization.

Milestones

Proposition 4.2: for any permutation $p$ , $(A^{(p_1)}\odot\cdots\odot A^{(p_N)})^{\mathrm H}(A^{(p_1)}\odot\cdots\odot A^{(p_N)})=\ast_n A^{(n)\mathrm H}A^{(n)}$ .
Corollary 4.3: $(V^\sigma)^{\mathrm H}V^\sigma=W^\sigma$ .
The splitting $f=\frac12(f^{(1)}-f^{(2)}-\overline{f^{(2)}}+f^{(3)})$ with $f^{(1)}=\|A^{(n)}V^{\{n\}\mathrm T}\|^2$ , $f^{(2)}=\langle T_{(n)},A^{(n)}V^{\{n\}\mathrm T}\rangle$ , $f^{(3)}=\|T_{(n)}\|^2$ .
$\partial f^{(1)}/\partial A^{(n)}=\overline{A}^{(n)}W^{\{n\}}$ .
$\partial f^{(2)}/\partial A^{(n)}=\overline{T}_{(n)}V^{\{n\}}$ and $\partial\overline{f^{(2)}}/\partial A^{(n)}=\partial f^{(3)}/\partial A^{(n)}=0$ .
Proposition 4.1: $\operatorname{vec}(C^{(q)}E)^{\mathrm T}=\operatorname{vec}(C^{(q)})^{\mathrm T}(E\otimes\mathbb I)$ and the chain rule $\partial/\partial C^{(q)}=\partial/\partial A^{(P+q)}\cdot E^{\mathrm T}$ .

Significance

Theorem 4.4 gives the gradient information every first-order and quasi-Newton method for the CPD, the rank- $(L_r,L_r,1)$ BTD and their generalization needs. It replaces derivatives through the large Khatri–Rao product $V^{\{n\}}$ by small $R'\times R'$ Hadamard products of Gramians, and leaves one tensor–Khatri–Rao product per mode as the dominant cost. Table 4.1 of the paper specializes it to third-order CPDs and BTDs, and the same structure underlies the alternating least squares updates of §4.1.

The paper proves the result. As far as a search of the Prove2Me catalogue and Mathlib shows, it has not been machine-checked. Mathlib has the Kronecker product and Matrix.vec, but no Khatri–Rao product, tensor unfoldings or Wirtinger calculus on matrix-valued unknowns. A formal proof would supply a checked derivation of the gradient formula used in tensor software, together with reusable lemmas about Khatri–Rao products and Wirtinger derivatives of real quadratic forms.

Difficulty

Each step is elementary, but the bookkeeping is easy to get wrong. The cogradient of a real function is not a complex derivative. Conjugates appear exactly where the conventions put them: with $\partial/\partial\bar z$ instead of $\partial/\partial z$ , or with the inner product conjugated on the other argument, every overbar in (4.5) moves. The proof also differentiates with respect to $A^{(P+q)}$ , which is not an unknown. That step is justified only by treating the structured CPD as an unstructured one and pulling back through $A^{(P+q)}=C^{(q)}E$ with a chain rule for Wirtinger derivatives, which needs real differentiability of the outer function. Finally, the Khatri–Rao identity $V^{\mathrm H}V=W$ requires reindexing a product over a permuted list of modes into a product over all modes.

Formalization scope

Modes are Fin P ⊕ Fin Q. The paper's mode $p$ is Sum.inl (p-1) and its mode $P+q$ is Sum.inr (q-1). The $R'$ columns are Σ r : Fin R, Fin (L r) in lexicographic order, which is the order of (3.5), and all indices are 0-based. vec is column-major (Mathlib's Matrix.vec). The rows of $V^\sigma$ and the columns of $T_{(n)}$ are indexed by tuples of the remaining indices rather than by integers; both use the same order, so the products in (4.5) are unchanged. The residual is defined entrywise and $f_{\mathrm{BTD}}$ is a real number cast to $\mathbb C$ . The cogradient is defined coordinatewise from Mathlib's real deriv along the directions $e_\beta$ and $\mathrm i e_\beta$ . The functions differentiated in the goal are real polynomials in the real and imaginary parts, so deriv is a genuine derivative there; a junk value of $0$ would make (4.5) false, not vacuous. Milestones 3–5 are stated for the unstructured CPD, in which every mode, including $n>P$ , has a free factor matrix. Proposition 4.1's chain rule assumes the outer function is real-differentiable at the point. That is the only hypothesis in the mission.

The paper's qualifiers " $a_r^{(n)}$ nonzero" (3.1) and "rank- $L_r$ " (3.5) describe what a decomposition is, and §4 never uses them. They are not imposed: the statements hold for arbitrary complex factor matrices and tensors, and $P$ , $Q$ , $R$ , $L_r$ , $I_n$ may be $0$ . The goal must not be replaced by its (4.4) part alone, which holds by construction, nor by a version with $\partial/\partial\bar z$ or with the Hermitian transpose $A^{\mathrm H}$ in place of the entrywise conjugate $\overline A$ .

A complete development needs Khatri–Rao Gramian identities, derivatives of real-valued polynomial maps along real lines in $\mathbb C^n$ , and the Wirtinger chain rule for a $\mathbb C$ -linear inner map. All of these can be reused outside this mission. Contributions are welcome on any milestone, and on general Wirtinger-calculus lemmas (linearity, products, conjugation, chain rule).

Selected references

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

9 thms3 active usersReviewed

Completed

Algebraic Topology Combinatorics·Captain: mikedeng1

Isoperimetric Inequalities in Simplicial Complexes 2: The Mixing Lemma — for Disjoint A_0,…,A_d in a Complex with a Complete Skeleton, ||F(A_0,…,A_d)| − α|A_0|⋯|A_d|/n| ≤ ρ_α(|A_0|⋯|A_d|)^(d/(d+1))Research Paper

Motivation

For a $k$ -regular graph $G=(V,E)$ on $n$ vertices, the Expander Mixing Lemma (Alon–Chung 1988; see the survey of Hoory, Linial and Wigderson 2006) says that for any vertex sets $A,B$ , the number of edges between them is close to its expected value: $\bigl||E(A,B)|-k|A||B|/n\bigr|\le\rho\sqrt{|A||B|}$ , where $\rho$ is the largest absolute value of a nontrivial eigenvalue of $kI-\Delta^+$ . The deviation, called the discrepancy of $A$ and $B$ , measures how random-like the graph is. It is one of the basic tools of spectral graph theory and of the theory of expanders.

Higher-dimensional expansion asks the same questions for simplicial complexes, where the role of edges is played by $d$ -dimensional cells. Parzanchevski, Rosenthal and Tessler (Combinatorica 35, 2015) prove, for complexes with a complete skeleton, a Cheeger inequality and a Mixing Lemma: the number of $d$ -cells with one vertex in each of $d+1$ disjoint vertex sets is controlled by the spectrum of the upper Laplacian. The Mixing Lemma is the result of this mission. In the same paper it yields a lower bound on Gromov's geometric overlap (Gromov 2010) of complexes with a small spectral spread.

Setting

Let $V=\{0,1,\dots,n-1\}$ and $d\ge1$ . A $d$ -dimensional complex with a complete skeleton $X$ contains every set of at most $d$ vertices as a cell, together with a set $X^d$ of $d$ -cells, each a set of $d+1$ vertices. Cells are oriented by the increasing order of their vertices.

A $(d-1)$ -form is a real function on the $d$ -element subsets of $V$ ; the space $\Omega^{d-1}$ carries the inner product $\langle f,g\rangle=\sum_\sigma f(\sigma)g(\sigma)$ . Similarly $\Omega^{d-2}$ consists of functions on $(d-1)$ -subsets ( $\Omega^{-1}=\mathbb R^{\{\varnothing\}}$ when $d=1$ ) and $\Omega^d$ of functions on $d$ -cells. Writing $\sigma_i$ for the $i$ -th vertex of $\sigma$ , the co-boundary operators are $(\partial^*_j f)(\sigma)=\sum_{i}(-1)^i f(\sigma\setminus\sigma_i)$ (for $j=d$ only on $\sigma\in X^d$ ), and the boundary operators are $(\partial_j g)(\sigma)=\sum_{v\sim\sigma} g(v\sigma)$ , the sum over vertices $v\notin\sigma$ with $\{v\}\cup\sigma$ a cell, where $v\sigma$ is the oriented cell $[v,\sigma_0,\sigma_1,\dots]$ .

The upper, lower and full Laplacians on $\Omega^{d-1}$ are

\Delta^+=\partial_d\partial^*_d,\qquad \Delta^-=\partial^*_{d-1}\partial_{d-1},\qquad \Delta=\Delta^++\Delta^-.

The $(d-1)$ -cycles are $Z_{d-1}=\ker\partial_{d-1}$ , and the exact forms are $B^{d-1}=\operatorname{im}\partial^*_{d-1}$ ; they are orthogonal complements in $\Omega^{d-1}$ . Write $\mathbb P_{Z_{d-1}}$ and $\mathbb P_{B^{d-1}}$ for the orthogonal projections. For vertex sets $A_0,\dots,A_d$ , $F(A_0,\dots,A_d)$ is the set of $d$ -cells with exactly one vertex in each $A_i$ .

For $\alpha\in\mathbb R$ the operator $\alpha I-\Delta^+$ preserves $Z_{d-1}$ , and

\rho_\alpha=\max\bigl\{|\mu|\;:\;\mu\text{ an eigenvalue of }(\alpha I-\Delta^+)|_{Z_{d-1}}\bigr\}=\bigl\|(\alpha I-\Delta^+)|_{Z_{d-1}}\bigr\|.

Formalization targets

Goal: Theorem (1.4), the Mixing Lemma (p. 16)

For every $\alpha\in\mathbb R$ and any pairwise disjoint vertex sets $A_0,\dots,A_d$ (not necessarily a partition),

\left|\,|F(A_0,\dots,A_d)|-\frac{\alpha\cdot|A_0|\cdots|A_d|}{n}\right|\le\rho_\alpha\cdot\bigl(|A_0|\cdots|A_d|\bigr)^{\frac d{d+1}}.

The parameter $\alpha$ is free; the introduction's Theorem 1.4 (p. 4) is the case $\alpha=k$ , the average degree of a $(d-1)$ -cell, and is included as a companion item.

Milestones

The milestones follow the proof of §4.3 and the facts of §§2–3 that it uses:

the chain-complex identity $\partial_{d-1}\partial_d=0$ and its dual, so $B^{d-1}\subseteq\ker\Delta^+$ (p. 6), and $B^{d-1}=Z_{d-1}^\perp$ (p. 6);
Proposition 3.2: $\Delta^+_{\overline X}=nI-\Delta_X$ for the complement complex (3.4), and $\Delta^-=n\,\mathbb P_{B^{d-1}}$ (3.5);
for the signed indicator forms $\varphi=\delta_{A_0,A_1,\dots,A_{d-1}}$ and $\psi=\delta_{A_d,A_1,\dots,A_{d-1}}$ : the norm identity (4.5), the count $\langle\varphi,(D-\Delta^+)\psi\rangle=|F(A_0,\dots,A_d)|$ (4.6), its $\alpha$ -shift (4.7), the splitting (4.8), the main term (4.9), the spectral bound (4.10)–(4.11);
the asymmetric bound $\rho_\alpha\sqrt{|A_0||A_d|}\,|A_1|\cdots|A_{d-1}|$ and the geometric-mean step that symmetrizes it.

Significance

For $d=1$ the theorem is the Expander Mixing Lemma of graphs. For $d\ge2$ it shows that a complex whose upper Laplacian has its nontrivial spectrum concentrated near $\alpha$ distributes its $d$ -cells evenly across any $d+1$ disjoint vertex sets, with a bound that depends on the set sizes only through $(\prod|A_i|)^{d/(d+1)}$ . The paper uses it to bound the geometric overlap of such complexes from below (Corollary 1.6), and to show that random Linial–Meshulam complexes (Linial–Meshulam 2006) have small discrepancy.

The result is proved in the paper. To the knowledge of this mission, neither it nor the underlying signed simplicial Laplacians with their Hodge decomposition on a complete skeleton has been formalized. The formalization produces the boundary and co-boundary operators, the three Laplacians, the identity for the complement complex, and the projection formula for $\Delta^-$ , all of which are standard in the spectral theory of complexes and reusable well beyond this result.

Difficulty

Each step of the proof is a finite computation, but the steps are sign-sensitive. The count (4.6) relies on the orientation conventions: $\psi$ replaces only the first block of $\varphi$ , and the off-diagonal terms of $\Delta^+$ carry the signs that make $\varphi(\sigma)\psi(\sigma')=+1$ on neighbouring cells. Proposition 3.2 (1) and (3) are identities between explicit matrices indexed by $d$ -subsets that hold only because the skeleton is complete. The spectral step needs the orthogonal decomposition $\Omega^{d-1}=B^{d-1}\oplus Z_{d-1}$ , invariance of $Z_{d-1}$ under $\Delta^+$ , and the spectral theorem for the restriction. A direct transcription of the graph argument does not apply: the operators act on $(d-1)$ -forms rather than on functions on vertices, and the expected count $\alpha\prod|A_i|/n$ is not visible from $\Delta^+$ of $X$ alone.

Formalization scope

Vertices are Fin n. A complex is the structure Complex n d holding its $d$ -cells, so the complete skeleton is built in; forms are EuclideanSpace ℝ over the subtype of $k$ -element subsets of Fin n, oriented by the order of Fin n. All boundary and co-boundary operators are defined by their formulas, not as adjoints of one another. The standing assumption $d\ge1$ is added to every statement. The disjoint sets $A_0,\dots,A_d$ form an arbitrary pairwise-disjoint family, some possibly empty; no partition and no bound $n\ge d+1$ is assumed. The exponent $d/(d+1)$ is a real power of a nonnegative real.

$\rho_\alpha$ is not defined as a maximum or supremum: the goal is stated for every real $\rho$ that bounds $|\mu|$ for all eigenvalues $\mu$ of $\alpha I-\Delta^+$ on $Z_{d-1}$ , which is equivalent to the statement for $\rho_\alpha$ . Trivializing formalizations are ruled out by construction: forms cannot be supported outside $d$ -subsets (such a form would be a spurious cycle), an empty eigenvalue set cannot be read through a default sSup value, the boundary operators carry orientation signs, and disjoint families are not confused with partitions.

Contributions are welcome at every milestone, in particular a general library for signed boundary operators on finite complexes, the identity $\partial\partial=0$ , and the Hodge-type decomposition of forms, which are reusable for the Cheeger inequality of the companion mission and for other work on high-dimensional expanders.

Selected references

O. Parzanchevski, R. Rosenthal, R. J. Tessler, Isoperimetric inequalities in simplicial complexes, Combinatorica 35 (2015); arXiv:1207.0638v3 (2013). https://arxiv.org/abs/1207.0638 , https://doi.org/10.1007/s00493-014-3002-x
N. Alon, F. R. K. Chung, Explicit construction of linear sized tolerant networks, Discrete Mathematics 72 (1988). https://doi.org/10.1016/0012-365X(88)90189-6
S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bulletin of the AMS 43 (2006). https://doi.org/10.1090/S0273-0979-06-01126-8
N. Linial, R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006). https://doi.org/10.1007/s00493-006-0027-9
M. Gromov, Singularities, expanders and topology of maps. Part 2: From combinatorics to topology via algebraic isoperimetry, Geometric and Functional Analysis 20 (2010). https://doi.org/10.1007/s00039-010-0073-8

16 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Exploiting Symmetries in SDP-Relaxations for Polynomial Optimization 4: A One-Variable SDP Upper Bound for Minimizing a Power Sum, Exact When an m-Sparse Optimum ExistsResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6.7

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

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

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

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

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

Milestones

In attack order:

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

8 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Exploiting Symmetries in SDP-Relaxations for Polynomial Optimization 3: Hankel-Matrix SDP Lower Bounds for Minimizing a Power Sum Subject to Fixed Lower Power SumsResearch Paper

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6.6

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

(a)

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

Lean namespace SymPolyOpt.PowerSumLB. Conventions:

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

Disclosed changes relative to the page:

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

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

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

Selected references

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

6 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Phase Recovery, MaxCut and Complex Semidefinite Programming 1: For Injective A, Nonzero b and Solvable |Ax| = b, PhaseCutMod Is Tight Whenever PhaseLift IsResearch Paper

Motivation

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

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

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

Setting

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

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

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

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

The three programs are

\text{(PhaseLift)}\quad \min_{X\in\mathbf H_p} \operatorname{Tr}(X)\ \ \text{s.t.}\ \operatorname{Tr}(a_ia_i^*X) = b_i^2,\ i=1,\dots,n,\ X\succeq 0;

\text{(PhaseCut)}\quad \min_{U\in\mathbf H_n} \operatorname{Tr}(UM)\ \ \text{s.t.}\ \operatorname{diag}(U) = 1,\ U\succeq 0;

\text{(PhaseCutMod)}\quad \min_{U\in\mathbf H_n} \operatorname{Tr}(BU)\ \ \text{s.t.}\ \operatorname{Tr}(MU) = 0,\ \operatorname{diag}(U) = 1,\ U\succeq 0.

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

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

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

Formalization targets

Goal: Corollary 4.3 (p. 13)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

9 thms3 active usersReviewed

Machine Learning Numerical Analysis Probability+2·Captain: mikedeng1

An Introduction to Matrix Concentration Inequalities III: A Matrix Sampling Estimator Satisfies E‖R̄ₙ − B‖ ≤ √(2m₂(R)log(d₁ + d₂)/n) + 2L log(d₁ + d₂)/(3n)Textbook

Motivation

Matrix approximation replaces a large or complicated matrix with a random matrix that is easier to store or compute. Averaging independent realizations improves accuracy while retaining the structure of each realization. Examples in Tropp's monograph include sparse approximations and randomized matrix products. The practical question is how the number of samples, the size of one sample, and its second moment control the spectral norm error. Tropp, §6.2

The book proves a matrix Bernstein inequality in Theorem 6.1.1, then applies it to an empirical matrix average in Corollary 6.2.1. Theorem 6.1.1 is already posed as TroppMatrixConcentration.matrix_bernstein on Prove2Me and is currently Open. This mission records the application with its own hypotheses and constants. The capstone concerns the estimator that a reader would construct, rather than a sum of abstract centered summands. Tropp, §§6.1–6.2

Setting

Let $B$ be a fixed complex $d_1\times d_2$ matrix. A sample matrix $R$ has the same size, has expectation $B$ , and has spectral norm at most $L$ almost surely. The equality $\mathbb ER=B$ makes one sample an unbiased estimate of $B$ . The almost-sure bound limits the size of every sample except on a probability-zero set. The dimensions $d_1,d_2$ are positive integers, and $n$ is a positive sample count.

Take independent copies $R_1,\ldots,R_n$ with the distribution of $R$ . Their matrix sampling estimator is

\overline R_n=\frac1n\sum_{k=1}^nR_k.

For any rectangular matrix $A$ , $A^*$ denotes its conjugate transpose and $\|A\|$ its spectral norm. The per-sample second moment is

m_2(R)=\max\{\|\mathbb E(RR^*)\|,\|\mathbb E(R^*R)\|\}.

Both terms matter for a rectangular matrix: $RR^*$ and $R^*R$ act on different coordinate spaces. All expectations of matrices are entrywise expectations, represented by Bochner integrals in Lean. The almost-sure norm bound guarantees the moments used here are finite. Tropp, equations (6.2.4)–(6.2.6)

Formalization targets

Empirical matrix approximation

Corollary 6.2.1 gives an expectation estimate and a tail estimate for the same estimator. For every real $t\ge0$ ,

\mathbb E\|\overline R_n-B\|\le \sqrt{\frac{2m_2(R)\log(d_1+d_2)}{n}}+ \frac{2L\log(d_1+d_2)}{3n},

\mathbb P\{\|\overline R_n-B\|\ge t\}\le (d_1+d_2)\exp\left(\frac{-nt^2/2}{m_2(R)+2Lt/3}\right).

The goal includes both bounds. The expectation estimate controls average error; the tail estimate controls the chance of an error above a chosen threshold. The dimension enters only through $\log(d_1+d_2)$ in the expectation bound and the factor $d_1+d_2$ in the tail bound. These are the book's constants, including the factors $2$ and $3$ in the linear terms. Tropp, Corollary 6.2.1, p. 81

Supporting statements

The milestone list follows Corollary 6.1.2 for uncentered summands, the bound $\|n^{-1}(R_k-B)\|\le2L/n$ , and the variance estimate $v(\overline R_n-B)\le m_2(R)/n$ . Equation (6.2.7) is a companion: a stated lower bound on $n$ implies $\mathbb E\|\overline R_n-B\|\le2\varepsilon$ for $\varepsilon>0$ . Tropp, pp. 77, 82

Significance

The result turns a bound on one random matrix into a quantitative guarantee for an empirical approximation. It lets a user choose a sample count for a target error and evaluate both average error and failure probability. The same framework is instantiated later in the monograph for matrix sparsification and multiplication; those applications depend on controlling $L$ and $m_2(R)$ for their particular sampling laws. Tropp, §§6.2–6.4

This is a known mathematical result proved in the book. Its Lean statement is an open formalization target. The mission adds a reusable empirical-mean definition and application statements built on the already published matrix spectral norm and rectangular second-moment definitions. A proof of the general matrix Bernstein theorem remains separate; the mission can draw on it when that platform theorem is proved.

Difficulty

The estimator error is a centered sum, but the sampling assumptions are given for an uncentered random matrix $R$ . Bounding the centered summands changes the uniform bound from $L$ to $2L/n$ . The variance parameter must be related to the second moment of one uncentered sample, with the correct $1/n$ scaling. Dropping the common-distribution condition would leave no relation between the samples' second moments and $m_2(R)$ . Applying scalar concentration to entries would not directly give the stated spectral norm bound or its dimension dependence. Tropp, proof of Corollary 6.2.1, p. 82

Formalization scope

Matrices are Matrix (Fin d₁) (Fin d₂) ℂ. The spectral norm and rectSecondMoment are imported from tc's published TroppMatrixConcentration definitions. An arbitrary probability space carries a measurable reference matrix $R_0$ and a finite family $R_k$ ; iIndepFun expresses independence and IdentDistrib expresses equality in law with $R_0$ . The estimator is the finite sum scaled by $n^{-1}$ . No particular sampling scheme or deterministic choice of $R$ is fixed: the formal goal requires only the source's unbiasedness and boundedness conditions.

The Lean statements explicitly require $d_1,d_2\ge1$ , $n>0$ , measurability, and the almost-sure form of $\|R\|\le L$ . These make the logarithm and inverse sample count meaningful and make the random matrix laws well behaved. For the uncentered Bernstein corollary, integrability of each $S_k$ is explicit because a bounded deviation from an unspecified mean alone does not establish that the mean exists. The goal also asserts integrability of its error norm, preventing a Bochner integral from silently taking Lean's default value for a nonintegrable function. The bound on $R$ supplies that integrability. When the denominator in a tail formula is zero, the displayed total real division gives a loose bound at the degenerate case; the source's probabilistic claim remains valid.

Contributions that formalize the centered-summand calculation, the variance estimate, or the transfer from the general matrix Bernstein theorem are within scope. The imported matrix and probability definitions are reusable in other matrix concentration missions. The local empirical-mean definition is reusable whenever a matrix estimator averages finitely many random samples.

Selected references

Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, especially §§6.1–6.4.

7 thms3 active usersReviewed

Completed

Numerical Analysis Probability Random Matrix Theory·Captain: mikedeng1

An Introduction to Matrix Concentration Inequalities II: A Random Row-and-Column Submatrix Z = PBR Satisfies E‖Z‖² ≤ 3(p/d)(r/n)‖B‖² Plus Logarithmic Row, Column and Entry TermsTextbook

Motivation and context

Large matrices are often reduced by retaining only some rows or columns. The reduced matrix is cheaper to store and apply, but its spectral norm can be distorted by a single unusually large row, column, or entry. A useful estimate must show both the average effect of sampling and the cost of these local concentrations. In §5.2 of Tropp's monograph, matrix Chernoff inequalities give numerical estimates for independently sampled columns and for independently sampled rows and columns. The latter is the capstone of this mission.

The general matrix Chernoff inequality, Theorem 5.1.1, is already an Open goal in tc's Chapter 5 mission on Prove2Me. The intrinsic-dimension Chernoff inequality, Theorem 7.2.1, is likewise Open in tc's Chapter 7 mission. This mission concerns the application statements that those chapter missions have not posed: the numerical bound (5.2.2), its three displayed intermediate estimates, and companion consequences in §§5.1.1, 5.2.1 and 7.2.2. The motivation for choosing this target is that it connects a general concentration result to a concrete random matrix model; its terms can be read directly from a deterministic input matrix.

Setting

Fix a complex matrix $B\in\mathbb C^{d\times n}$ with $d,n\ge1$ . For each row $j$ , let $\delta_j$ equal one when that row is retained and zero otherwise. For each column $k$ , let $\xi_k$ have the analogous meaning. The whole family is independent, with $\delta_j\sim\operatorname{Bernoulli}(p/d)$ and $\xi_k\sim\operatorname{Bernoulli}(r/n)$ , where $0\le p\le d$ and $0\le r\le n$ . Thus $p$ and $r$ are the expected numbers of retained rows and columns. Put

P=\operatorname{diag}(\delta_1,\ldots,\delta_d),\qquad R=\operatorname{diag}(\xi_1,\ldots,\xi_n),\qquad Z=PBR.

The zeros remain in the matrix: $Z$ has the same dimensions as $B$ , but entries in discarded rows or columns vanish. Write $b_{j:}$ for row $j$ , $b_{:k}$ for column $k$ , and $b_{jk}$ for an entry. Their vector norms are Euclidean, while $\|B\|$ and $\|Z\|$ denote the spectral operator norm. The source uses $\mathbb E$ for expectation over the selections. Its maxima range over all rows, columns or entries of $B$ , so a highly uneven matrix is distinguished from one whose mass is spread evenly.

The first milestone is the streamlined upper matrix Chernoff expectation bound. For a finite independent family of positive semidefinite Hermitian matrices $X_k$ with eigenvalues at most $L$ , let $Y=\sum_kX_k$ and $\mu_{\max}=\lambda_{\max}(\mathbb EY)$ . The bound uses the book's numerical constant $1.72$ . The subsequent milestones specialize this setting to the row and column selectors above. A separate companion states the lower bound with $0.63$ and the two weakened tail inequalities of §5.1.1.

Formalization targets

The goal is the exact displayed estimate (5.2.2), with the book's rounded constants:

\begin{aligned} \mathbb E\|PBR\|^2\le{}&3\frac pd\frac rn\|B\|^2 +2\frac{p\log d}{d}\max_k\|b_{:k}\|^2\\ &+2\frac{r\log n}{n}\max_j\|b_{j:}\|^2 +(\log d)(\log n)\max_{j,k}|b_{jk}|^2. \end{aligned}

Its milestone chain is (5.1.8), followed by (5.2.3), (5.2.4), and (5.2.5). These are the claims the text places immediately before the final estimate. They bound, respectively, the first column-selection stage, the norm of the row-selected matrix, and the largest column norm after row selection. The companion (5.2.1) gives both the top and least squared singular-value bounds for column selection alone. The companion from §7.2.2 replaces $\log d$ by $\log(2\operatorname{srank}(B))$ , where $\operatorname{srank}(B)=\|B\|_F^2/\|B\|^2$ is stable rank.

Significance

The goal separates four sources of size in a sampled matrix. The first term scales the squared spectral norm by the expected row and column retention fractions. The remaining terms record concentrations in a column, a row, and an individual entry. Consequently, the estimate can be evaluated from $B$ and the two sampling rates without specifying a distribution for $B$ itself. It is an expectation bound, not a claim that every realized submatrix is close to $B$ .

The formal development would make the application layer of Tropp's Chapter 5 available alongside tc's general, currently Open matrix Chernoff theorem. A proof of that general theorem does not itself identify the random projectors, their joint independence, or the deterministic quantities on the right side of (5.2.2). The stable-rank companion also links the Chapter 7 notion of intrinsic dimension to a concrete rectangular matrix statistic. Both the chapter's general theorems and this mission's statements remain Open on the platform; none is being presented as already machine proved. Tropp, §§5.2 and 7.2.2 gives the mathematical results.

Difficulty

Sampling both rows and columns introduces two interacting random projectors. Merely applying a one-stage column estimate to $B$ leaves the row selection uncontrolled; merely applying a one-stage row estimate leaves the sampled column norms random. The two families must be independent of each other as well as independent internally. That distinction is substantial: separate independence claims for the row family and the column family do not imply independence between $P$ and $R$ . The final estimate must also retain the book's exact $3$ and $2$ coefficients rather than replacing the right side by an unspecified constant times a simpler expression.

Formalization scope

Matrices are Matrix (Fin d) (Fin n) ℂ, matching the book's general complex-matrix convention. The spectral norm, extreme eigenvalues, Borel measurable matrix space, and intrinsic dimension come from tc's published definitions, which this mission references. Random selectors are measurable real-valued functions on a probability space; their Bernoulli law specifies almost-sure values zero or one and the probability of one. The row and column selectors form one jointly independent family. Products with diagonal selector matrices define $PB$ , $BR$ and $PBR$ ; a deterministic diagonal or an unconstrained zero-one function would not be the sampled model.

Every sampling rate is within its Bernoulli domain. Nonzero dimensions keep the maxima over finite, inhabited sets and give the logarithms their intended arguments. Lean's Bochner integral otherwise returns zero on a nonintegrable function; each expectation inequality records integrability in its conclusion, which follows from measurable, bounded Bernoulli selectors and Tropp's standing regularity convention in §2.2.1. The maxima of column, row, and entry magnitudes are real finite suprema, equal to maxima for these finite nonempty index sets. The intrinsic-dimension identity assumes $p>0$ and $B\ne0$ for scale invariance; the final stable-rank bound itself includes zero sampling and the zero matrix.

The definitions of Bernoulli selection, random diagonal projections, sampled matrices, finite norm maxima and stable rank are reusable outside this mission. Contributions can address their structural identities, integrability, the four milestones, the goal, or the independent column-selection companions. The book's constants $1.72$ and $0.63$ are retained as decimals; $3$ and $2$ are the rounded coefficients printed in (5.2.2), as the text explains on p. 66.

Selected references

Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, §§2.1, 2.2, 5.1, 5.2, 7.2.
Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, DOI:10.1561/2200000048. The formalization cites the pinned arXiv version above for page and equation indices.

11 thms3 active usersReviewed

Completed

Combinatorics Probability Random Matrix Theory·Captain: mikedeng1

An Introduction to Matrix Concentration Inequalities I: A Matrix Gaussian Series Satisfies v(Z) ≤ E‖Z‖² ≤ 2v(Z)(1 + log(d₁ + d₂))Textbook

Motivation

Random matrices arise when observations, signs, or model coefficients fluctuate. Their spectral norm measures the largest amplification they can cause to a vector. A bound on that norm can turn entrywise randomness into a statement about the behavior of an entire linear operator. Tropp's chapter develops a common framework for Gaussian and Rademacher sums of fixed matrices, then applies it to Wigner matrices, rectangular Gaussian matrices, random signs, Toeplitz matrices, and a rounding scheme for a quadratic optimization relaxation (Tropp, Chapter 4). The applications show what the general estimate says when the matrices have concrete structure.

The chapter's general matrix-series theorem, Theorem 4.1.1, is already an open statement in tc's Prove2Me Chapter 4 mission. This mission targets the squared-norm comparison in §4.1.2 and the worked consequences that are not part of that existing goal. They are useful benchmarks because their dimensions, coefficients, and variance statistics are explicit. The existing platform status is a formalization status: Tropp proves these mathematical bounds in the cited book; the Chapter 4 theorem and the results proposed here do not yet have machine-checked proofs.

Setting

Fix positive integers $d_1,d_2$ and a finite family of complex $d_1\times d_2$ matrices $B_k$ . Let $\gamma_k$ be independent standard Gaussian real variables, each with mean zero and variance one. Their matrix Gaussian series is $Z=\sum_k\gamma_k B_k$ . For a complex matrix $M$ , write $M^*$ for its conjugate transpose and $\|M\|$ for its Euclidean operator norm. The matrix variance statistic is

v(Z)=\max\{\|\mathbb E(ZZ^*)\|,\ \|\mathbb E(Z^*Z)\|\}.

For this Gaussian series, the two expected products equal the corresponding sums of coefficient products, so $v(Z)$ can be computed from the fixed $B_k$ . This is the same statistic and norm as Theorem 4.1.1, equations (4.1.2)–(4.1.4) (Tropp, p. 42). Expectations are entrywise Bochner integrals for matrix-valued functions and ordinary integrals for real quantities.

A Rademacher variable takes values $-1$ and $1$ with equal probability. Some companion examples replace the Gaussian coefficients by independent Rademacher variables. For a Hermitian square matrix $Y$ , $\lambda_{\min}(Y)$ denotes its smallest real eigenvalue. In the signed-entry example, the relevant matrix statistic is the larger of the greatest squared row norm and the greatest squared column norm of a fixed matrix.

Formalization targets

Squared norm of a Gaussian series

The goal is the pair of inequalities in (4.1.7), together with explicit integrability of the random squared norm:

v(Z)\le\mathbb E\|Z\|^2\le2v(Z)\bigl(1+\log(d_1+d_2)\bigr).

The constants and the logarithm are exactly those printed on pp. 43–44. The left side identifies a necessary scale; the right side gives a dimension-dependent upper estimate. The two milestones are the Jensen lower-bound display and the tail-integration display in §4.1.2. The latter is stated for any measurable matrix with the chapter's tail bound and positive variance, because the displayed integration step itself uses only those properties. It retains the exact split-point expression and the factor $2$ .

Worked series

Companion statements record the minimum-eigenvalue consequences (4.6.4)–(4.6.5), the Wigner estimate (4.2.3), the rectangular Gaussian estimate (4.2.6), the randomly signed-entry estimate (4.3.3), the Toeplitz estimate (4.4.3), and the MaxQP rounding scale in §4.5. Their deterministic variance identities are part of the statements, rather than assumptions. In particular the Wigner bound keeps $\log(2d)$ and the Toeplitz bound keeps the exact coefficient sum $dI_d$ (Tropp, pp. 46–52).

Significance

The squared-norm comparison says that $v(Z)$ is the correct baseline for the size of a Gaussian series in mean square, while allowing a logarithmic penalty for matrix dimension. It also shows why an expectation estimate and a tail estimate answer different questions: the chapter discusses examples where a tail bound can be loose even when the expected norm is controlled (Tropp, pp. 44–45). The example statements make the abstract variance statistic usable for standard matrix ensembles and for signed matrices with prescribed entries.

A machine-checked development would connect the existing spectral and probability definitions to explicit examples, finite-sum variance identities, and integrability of Gaussian matrix norms. Those components can be reused in later sampling and numerical linear algebra missions. The general Chapter 4 matrix-series theorem remains an open platform target; these application statements are not claimed to be already formalized or proved there.

Difficulty

The central obstacle is moving from a tail estimate for $\|Z\|$ to a finite, sharp expectation for $\|Z\|^2$ . The tail estimate has a dimension factor, while the desired bound has its logarithm; an unspecialized bound at a single threshold does not provide the stated constant. At the modeling level, matrix variance uses expectations of matrix products, so it must coincide with the finite sums of coefficient squares for each example. A definition that silently returns zero for a nonintegrable Bochner integral would make the upper inequality misleading. The Gaussian law, measurability, and moment behavior therefore matter to the statement as well as to eventual proofs.

Formalization scope

Matrices use Matrix (Fin d₁) (Fin d₂) ℂ with $d_1,d_2\ge1$ and tc's spectralNorm and rectSecondMoment definitions. The probability space is arbitrary; coefficient functions are measurable and independent, and their pushforward laws are exactly standard Gaussian or Rademacher as the page requires. Families may be empty. Real random coefficients scale complex matrices. Integrability of $\|Z\|^2$ is a conclusion of the goal and tail-integration milestone, while the minimum-eigenvalue expectation companion likewise asserts integrability. The tail-integration milestone assumes $v(Z)>0$ because its displayed denominator divides by $v(Z)$ ; the Gaussian goal itself includes $v(Z)=0$ .

The Wigner coefficients are indexed by pairs $i<j$ ; rectangular and signed-entry coefficients by row-column pairs; Toeplitz coefficients by diagonals $-(d-1),\ldots,d-1$ . The Toeplitz index in Lean is shifted to Fin (2*d-1). Row and column maxima range over the nonempty finite row and column sets. The signed-entry theorem permits complex fixed entries and uses $|b_{ij}|^2$ ; the printed example starts with real entries. MaxQP uses the positive scale $\alpha=1/\sqrt{2\log(d_1+d_2)}$ and tc's positive-semidefinite order for the two relaxation constraints. None of the coefficient-square identities is supplied as a hypothesis; each is a conclusion to establish.

Context. The existing TroppMatrixConcentration.ch4_matrix_series formalizes Theorem 4.1.1 and is Open. Its Gaussian/Rademacher variance identity and norm/tail bounds provide the chapter context. The present goal specializes the same Gaussian model and asks for the separate second-moment result (4.1.7). Reusable contributions include finite-matrix identities, Gaussian moment integrability, and tail-integration lemmas. A valid proof must preserve the actual standard laws and independence, and cannot redefine $v(Z)$ as the expected squared norm.

Selected references

Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, Chapter 4, pp. 42–52.

8 thms3 active usersReviewed

Completed

Numerical Analysis Quantum Information·Captain: mikedeng1

Quantum Algorithm for Systems of Linear Equations with Exponentially Improved Dependence on Precision I: A Truncated Odd Chebyshev Series Is 2ε-Close to 1/x on [−1, −1/κ] ∪ [1/κ, 1]Research Paper

Motivation

The quantum linear systems problem asks, given a sparse Hermitian $N \times N$ matrix $A$ with condition number $\kappa$ and a procedure preparing a state $|b\rangle$ , to prepare a state close to $A^{-1}|b\rangle / \|A^{-1}|b\rangle\|$ . Harrow, Hassidim and Lloyd (2009) gave a quantum algorithm whose running time is polynomial in $\log N$ and $\kappa$ but grows like $1/\varepsilon$ in the target precision $\varepsilon$ , because it estimates eigenvalues by phase estimation. Childs, Kothari and Somma (arXiv:1511.02306, SIAM J. Comput. 46(6), 2017) reduced the precision dependence to $\mathrm{poly}\log(1/\varepsilon)$ , an exponential improvement.

The reduction has two parts. A quantum part implements a linear combination of unitaries applied to $A$ , and turns any function that is $\varepsilon$ -close to $1/x$ on the spectrum of $A$ into an approximate preparation of the solution state (Corollary 10 and Proposition 9 of the paper). An analytic part supplies such a function with small degree and small coefficient weight. The paper gives two analytic constructions: a Fourier expansion (Section 3) and an expansion in Chebyshev polynomials (Section 4). This mission formalizes the analytic core of the Chebyshev construction, the input to the paper's Theorem 4. The quantum algorithms and their query and gate counts are not formalized here.

Setting

For a real number $\kappa \ge 1$ (a condition number: the ratio of the largest to the smallest singular value), the domain is

D_\kappa := [-1, -1/\kappa] \cup [1/\kappa, 1].

A function $g$ is $\varepsilon$ -close to $h$ on a set $D \subseteq \mathbb R$ if $|g(x) - h(x)| \le \varepsilon$ for all $x \in D$ .

The Chebyshev polynomials of the first kind are $\mathcal T_0(x) = 1$ , $\mathcal T_1(x) = x$ and $\mathcal T_{n+1}(x) = 2x\mathcal T_n(x) - \mathcal T_{n-1}(x)$ ; those of the second kind $\mathcal U_n$ satisfy the same recursion with $\mathcal U_0 = 1$ , $\mathcal U_1 = 2x$ .

For natural numbers $b, j$ let

c_{b,j} := \frac{1}{2^{2b}} \sum_{i=j+1}^{b} \binom{2b}{b+i},

the probability of more than $b+j$ heads in $2b$ fair coin flips. The tamed inverse (74) is $f_b(x) = (1 - (1-x^2)^b)/x$ , and the odd Chebyshev series is

S_{b,n}(x) := 4 \sum_{j=0}^{n-1} (-1)^j c_{b,j}\, \mathcal T_{2j+1}(x).

In Lean these are Dκ, coeff b j, fTamed b, and chebSum b n in the namespace QuantumLinSys.Chebyshev; bOf κ ε and j0Of b ε are the parameters $b$ and $j_0$ below.

Formalization targets

Goal: Lemma 14 (p. 16)

With $b = \kappa^2 \log(\kappa/\varepsilon)$ and $j_0 = \sqrt{b\log(4b/\varepsilon)}$ , the truncated series

g(x) = 4\sum_{j=0}^{j_0} (-1)^j c_{b,j}\, \mathcal T_{2j+1}(x)

is $2\varepsilon$ -close to $1/x$ on $D_\kappa$ , for every $\kappa \ge 1$ and $\varepsilon > 0$ .

Milestones, in the order the proof uses them

Lemma 17 (p. 19). For integers $d \ge 1$ and $b \ge (\kappa d)^2\log(\kappa d/\varepsilon)$ , $f_b$ is $\varepsilon$ -close to $1/x$ on $D_{\kappa d}$ .
Lemma 18 (p. 19). On $[-1,1]$ , $f_b = S_{b,b}$ exactly:

\frac{1-(1-x^2)^b}{x} = 4\sum_{j=0}^{b-1}(-1)^j c_{b,j}\,\mathcal T_{2j+1}(x).

Display (89) (p. 21). $c_{b,j} \le e^{-j^2/b}$ .
Lemma 19 (p. 21). The series truncated at $j_0 = \sqrt{b\log(4b/\varepsilon)}$ is $\varepsilon$ -close to $f_b$ on $[-1,1]$ .

Two further statements of the same approach are included as companion theorems: Lemma 16 (p. 17), the closed form of the $n$ -th power of the $2\times 2$ rotation block in terms of $\mathcal T_n$ and $\mathcal U_{n-1}$ , and Proposition 9 (p. 9), the $4\varepsilon$ perturbation bound for normalized states.

Significance

Lemma 14 provides a polynomial of degree $O(\kappa\log(\kappa/\varepsilon))$ whose Chebyshev coefficients have total weight $O(\sqrt{b\log(b/\varepsilon)})$ , approximating $1/x$ uniformly on the region where a well-conditioned matrix has its eigenvalues. Applied to a Hermitian matrix through a quantum walk, whose powers implement $\mathcal T_n$ (Lemma 16), it gives the query complexity $O(d\kappa^2\log^2(d\kappa/\varepsilon))$ of Theorem 4. The same polynomial approximation of $1/x$ reappears in later work on quantum singular value transformation and matrix inversion.

All results of this mission are proved in the paper. None of them is machine-checked in Mathlib or on the platform, as far as a search found: Mathlib has the Chebyshev polynomials and the identity $\mathcal T_n(\cos\theta) = \cos n\theta$ , but no Chebyshev expansion of a rational function, no binomial tail bound in this form, and no approximation theorem for $1/x$ . The formalization produces a checked uniform approximation of $1/x$ with explicit, non-asymptotic parameters.

Difficulty

The exact identity (Lemma 18) has no slack: every coefficient, sign and summation bound of (77) must be right for all $b$ , and an off-by-one in the inner sum or in the Chebyshev index makes it false. Mathlib's Chebyshev library offers evaluation facts but no expansion of a given polynomial in the Chebyshev basis. The bound (89) is a Chernoff–Hoeffding tail bound for a symmetric binomial distribution, which must be stated for sums of binomial coefficients rather than for random variables. The goal then needs both approximation errors at the page's specific parameters, including the corner cases in which $\log(\kappa/\varepsilon)$ or $\log(4b/\varepsilon)$ is negative.

Formalization scope

All functions are real functions of one real variable. Chebyshev polynomials are Mathlib's Polynomial.Chebyshev.T ℝ and Polynomial.Chebyshev.U ℝ, indexed by integers. The sum $\sum_{j=0}^{n-1}$ is over Finset.range n, so the series of (55)/(88) truncated at $j_0$ is chebSum b (j₀ + 1) and the full series (77) is chebSum b b.

The formalization commits to the following conventions, each disclosed in the item it affects.

$\kappa \ge 1$ on every statement that mentions $D_\kappa$ , and $d \ge 1$ in Lemma 17. Below these values the domain is empty or contains $0$ .
$\varepsilon > 0$ . No upper bound on $\varepsilon$ is imposed in this mission.
The paper's real $b = \kappa^2\log(\kappa/\varepsilon)$ is rounded up to a natural number in the goal, and the truncation index $j_0$ is rounded down, the sum running over $j = 0,\dots,\lfloor j_0\rfloor$ .
In Lemmas 17–19 $b$ is a natural number. The page's "integer" exponent cannot be negative without making $(1-x^2)^b$ singular.
At $x = 0$ , $f_b(0)$ is Lean's $0/0 = 0$ , which is the value of its continuous extension. Lemma 18 is therefore stated on all of $[-1,1]$ .
Proposition 9 is stated for continuous linear operators on $\mathbb C^N$ , with $\|C^{-1}\| \le 1$ given as a two-sided inverse of norm at most $1$ , and for unit vectors $\psi$ .

A trivializing reading is ruled out: the goal fixes the page's $b$ , $j_0$ and constant $2\varepsilon$ , so neither an arbitrarily large truncation nor a weaker constant satisfies it, and the domain $D_\kappa$ excludes the origin, where Lean's $1/0 = 0$ would make closeness to $1/x$ meaningless.

Useful infrastructure, reusable beyond this mission: Chebyshev expansions of polynomials on $[-1,1]$ , binomial tail bounds, and uniform approximation of $1/x$ . Contributions of general lemmas of this kind are welcome.

Selected references

A. M. Childs, R. Kothari and R. D. Somma, Quantum algorithm for systems of linear equations with exponentially improved dependence on precision, SIAM J. Comput. 46(6), 2017; arXiv:1511.02306v2. https://arxiv.org/abs/1511.02306
A. W. Harrow, A. Hassidim and S. Lloyd, Quantum algorithm for linear systems of equations, Phys. Rev. Lett. 103, 150502, 2009. https://arxiv.org/abs/0811.3171
D. W. Berry, A. M. Childs and R. Kothari, Hamiltonian simulation with nearly optimal dependence on all parameters, FOCS 2015. https://arxiv.org/abs/1501.01715
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

6 thms3 active usersReviewed

Completed

Control Theory Dynamical Systems·Captain: mikedeng1

Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems 1: States Reached from 0 Stay in Im P and Ker Q Gives Zero Output, for Gramians P, Q ≥ 0 of (3.6)Research Paper

Motivation

Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions $P$ and $Q$ of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.

Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.

Setting

Fix $n, m, p \ge 0$ and real matrices $A, N_1,\dots,N_m\in\mathbb R^{n\times n}$ , $B\in\mathbb R^{n\times m}$ , $C\in\mathbb R^{p\times n}$ . The bilinear control system (3.1)–(3.2) is

\dot x = Ax + \sum_{j=1}^m N_j x\,u_j + Bu,\qquad y = Cx,

with state $x(t)\in\mathbb R^n$ , input $u(t) = [u_1(t),\dots,u_m(t)]^T\in\mathbb R^m$ and output $y(t)\in\mathbb R^p$ . The homogeneous system (3.5) drops the term $Bu$ : $\dot x = Ax + \sum_j N_j x\,u_j$ , $y = Cx$ . The same $m$ indexes the bilinear terms and the columns of $B$ . Write $x(t, x_0, u)$ for a solution with input $u$ and initial state $x(0) = x_0$ , and $y(t,x_0,u) = Cx(t,x_0,u)$ .

An admissible input is a function $u:[0,\infty)\to\mathbb R^m$ that is integrable on every interval $[0,T]$ . A solution with $x(0) = x_0$ is a continuous $x:[0,\infty)\to\mathbb R^n$ satisfying

x(t) = x_0 + \int_0^t \Big(Ax(s) + \sum_{j=1}^m u_j(s)N_jx(s) + Bu(s)\Big)\,ds\qquad (t\ge 0).

The generalized Lyapunov equations (3.6) are

AP + PA^T + \sum_{j=1}^m N_jPN_j^T = -BB^T,\qquad A^TQ + QA + \sum_{j=1}^m N_j^TQN_j = -C^TC .

A solution $P$ of the first is a controllability Gramian and a solution $Q$ of the second an observability Gramian. " $P\ge 0$ " means $P$ is symmetric nonnegative definite; $\mathrm{Im}\,P$ and $\mathrm{Ker}\,P$ are its image and kernel.

Formalization targets

Goal: Theorem 3.1 (p. 695)

(a) If $P\ge 0$ solves the first equation of (3.6), then for every admissible input $u$

x(t,0,u)\in\mathrm{Im}\,P\qquad\text{for all } t\ge 0 .

(b) If $Q\ge 0$ solves the second equation of (3.6) and $x_0\in\mathrm{Ker}\,Q$ , then for the homogeneous system (3.5) and every admissible input $u$

y(t,x_0,u) = Cx(t,x_0,u) = 0\qquad\text{for all } t\ge 0 .

Milestones (the steps of the paper's proof, pp. 695–696)

$N_j^T\,\mathrm{Ker}\,P\subset\mathrm{Ker}\,P\subset\mathrm{Ker}\,B^T$ .
$A^T\,\mathrm{Ker}\,P\subset\mathrm{Ker}\,P$ .
$\mathrm{Im}\,P$ is invariant under the vector field of (3.1): $z\in\mathrm{Im}\,P$ implies $Az + \sum_j w_jN_jz + Bw\in\mathrm{Im}\,P$ for every $w\in\mathbb R^m$ .
$N_j\,\mathrm{Ker}\,Q\subset\mathrm{Ker}\,Q\subset\mathrm{Ker}\,C$ and $A\,\mathrm{Ker}\,Q\subset\mathrm{Ker}\,Q$ .
$\mathrm{Ker}\,Q$ is invariant under the vector field of (3.5).

Significance

The result. Part (a) says that a state outside $\mathrm{Im}\,P$ cannot be reached from the origin by any input, so its controllability energy $E_c$ is infinite; part (b) says that a state in $\mathrm{Ker}\,Q$ is indistinguishable from the origin at the output, so its observability energy $E_o$ is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to $\mathrm{Im}\,P$ and projected along $\mathrm{Ker}\,Q$ without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of $A$ nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field $z\mapsto Az + \sum_j w_jN_jz + Bw$ is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.

Difficulty

The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix $M$ , $v^TMv = 0$ forces $Mv = 0$ , applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence " $\dot x(t)\in\mathrm{Im}\,P$ whenever $x(t)\in\mathrm{Im}\,P$ , so $\mathrm{Im}\,P$ is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so $x$ is merely absolutely continuous and $\dot x$ exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of $x(t)$ orthogonal to the subspace.

Formalization scope

The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices $j = 1,\dots,m$ as Fin m. $\mathrm{Im}\,P$ and $\mathrm{Ker}\,P$ are LinearMap.range and LinearMap.ker of Matrix.toLin' P; " $P\ge 0$ " is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every $[0,T]$ (this contains $L^2[0,\infty[$ , the input space of the paper's energy functionals). A solution is a function continuous on $[0,\infty)$ whose integrand is integrable on every $[0,t]$ and which satisfies the integral equation for all $t\ge 0$ ; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.

Two reading decisions are fixed. First, part (b) is stated for every admissible input $u$ , not only for $u = 0$ as printed in the theorem: the paper's proof concludes " $x(t,x_0,u)\in\mathrm{Ker}\,Q$ for all $t\ge0$ , implying $y(t,x_0,u) = 0$ ", and the theorem's clause "i.e., $E_o(x_0) = 0$ " (with $E_o$ a maximum over inputs) needs this form. The $\forall u$ statement contains the printed one. Second, the clauses "i.e., $E_c(x_0) = \infty$ " and "i.e., $E_o(x_0) = 0$ ", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.

The statements must not be trivialized: assuming $P$ positive definite makes (a) empty ( $\mathrm{Im}\,P = \mathbb R^n$ ), assuming $A$ stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring $C^1$ trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for $A = -I_2$ , $N_1 = 0$ , $B = e_1$ , the matrix $P = \mathrm{diag}(1/2, 0)$ is a nonnegative definite solution of (3.6) with $e_2\notin\mathrm{Im}\,P$ .

A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.

Selected references

P. Benner, T. Damm, Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems, SIAM J. Control Optim. 49(2), 686–711, 2011. https://doi.org/10.1137/09075041X
S. A. Al-Baiyat, M. Bettayeb, A new model reduction scheme for k-power bilinear systems, Proceedings of the 32nd IEEE Conference on Decision and Control, San Antonio, 1993, pp. 22–27 (reference [1] of Benner–Damm).
W. S. Gray, J. Mesko, Energy functions and algebraic Gramians for bilinear systems, Preprints of the 4th IFAC Nonlinear Control Systems Design Symposium, Enschede, 1998, pp. 103–108 (reference [25] of Benner–Damm).
B. C. Moore, Principal component analysis in linear systems: Controllability, observability, and model reduction, IEEE Trans. Automat. Control 26(1), 17–32, 1981. https://doi.org/10.1109/TAC.1981.1102568

8 thms3 active usersReviewed

Completed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Generalising the Scattered Property of Subspaces 1: An h-Scattered 𝔽_q-Subspace of V(r, qⁿ) Either Defines a Subgeometry or Has Dimension at Most rn/(h + 1)Research Paper

Motivation

Let $V$ be an $r$ -dimensional vector space over the finite field $\mathbb F_{q^n}$ . Viewed over the subfield $\mathbb F_q$ , $V$ has dimension $rn$ , and its one-dimensional $\mathbb F_{q^n}$ -subspaces form the Desarguesian spread. An $\mathbb F_q$ -subspace $U$ of $V$ is scattered if it meets every element of this spread in an $\mathbb F_q$ -subspace of dimension at most one. Scattered subspaces define scattered $\mathbb F_q$ -linear sets in $\mathrm{PG}(r-1,q^n)$ . Through these linear sets they are connected to projective two-weight codes, strongly regular graphs and maximum rank distance (MRD) codes. In 2000 Blokhuis and Lavrauw proved that a scattered subspace has dimension at most $rn/2$ , and a sequence of papers showed that this bound is attained whenever $2 \mid rn$ .

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2; Combinatorica 41, 2021) replace the one-dimensional spread elements by all $h$ -dimensional $\mathbb F_{q^n}$ -subspaces. This gives a hierarchy of conditions, the $h$ -scattered subspaces, that refines the scattered case. For $h = r-1$ and dimension $n$ these subspaces had already been identified with $\mathbb F_{q^n}$ -linear MRD codes by Sheekey and Van de Voorde. This mission formalizes the paper's main theorem, the dimension bound for $h$ -scattered subspaces.

Timeline.

2000: Blokhuis and Lavrauw, Scattered spaces with respect to a spread in PG(n, q), prove $\dim_{\mathbb F_q} U \le rn/2$ for scattered $U$ (the case $h = 1$ ).
2000–2018: Ball–Blokhuis–Lavrauw (2000), Blokhuis–Lavrauw (2000), Csajbók–Marino–Polverino–Zullo (2017) and Bartoli–Giulietti–Marino–Polverino (2018) together show that scattered subspaces of dimension $rn/2$ exist whenever $rn$ is even.
2020: Sheekey and Van de Voorde study subspaces scattered with respect to hyperplanes ( $h = r-1$ ) and relate them to MRD codes.
2019–2021: Csajbók, Marino, Polverino and Zullo introduce $h$ -scattered subspaces and prove the bound $rn/(h+1)$ for every $h$ (Theorem 2.3).

Setting

Let $\mathbb F_q \subseteq \mathbb F_{q^n}$ be finite fields, so $n = \dim_{\mathbb F_q}\mathbb F_{q^n}$ , and let $V$ be a vector space over $\mathbb F_{q^n}$ of dimension $r$ . Every $\mathbb F_{q^n}$ -subspace of $V$ is also an $\mathbb F_q$ -subspace. For an $\mathbb F_q$ -subspace $U$ of $V$ , $\langle U\rangle_{\mathbb F_{q^n}}$ denotes its $\mathbb F_{q^n}$ -span.

Definition 1.1. Let $0 < h \le r-1$ . An $\mathbb F_q$ -subspace $U$ of $V$ is $h$ -scattered if $\langle U\rangle_{\mathbb F_{q^n}} = V$ and every $h$ -dimensional $\mathbb F_{q^n}$ -subspace $S$ of $V$ satisfies $\dim_{\mathbb F_q}(S\cap U) \le h$ . In Lean this is HScattered.Bound.IsHScattered F K h U, with F $=\mathbb F_q$ , K $=\mathbb F_{q^n}$ , and $r$ = Module.finrank K V.

An $\mathbb F_q$ -subspace $U$ defines a subgeometry of $\mathrm{PG}(V,\mathbb F_{q^n})$ if some $\mathbb F_q$ -basis of $U$ is also an $\mathbb F_{q^n}$ -basis of $V$ (HScattered.Construction.DefinesSubgeometry F K U, a definition shared with the other missions of this series). In coordinates, $U$ is then $\mathbb F_q^{\,r}$ inside $\mathbb F_{q^n}^{\,r}$ .

A rank distance code of $\mathbb F_q^{n\times m}$ , $n \le m$ , is a set $\mathcal C$ of $\mathbb F_q$ -linear maps from an $m$ -dimensional to an $n$ -dimensional $\mathbb F_q$ -space, with distance $d(f,g) = \operatorname{rk}(f-g)$ .

Formalization targets

Goal: Theorem 2.3

If $U$ is an $h$ -scattered $\mathbb F_q$ -subspace of $V$ , then either $\dim_{\mathbb F_q}U = r$ , $U$ defines a subgeometry and $U$ is $(r-1)$ -scattered, or

\dim_{\mathbb F_q} U \le \frac{rn}{h+1}.

The disjunction is inclusive. The statement holds for every $h$ in the range $0 < h \le r-1$ , including $h = 1$ .

Milestones

Proposition 2.1. For $h > 1$ , an $h$ -scattered subspace is $i$ -scattered for every $0 < i < h$ .
Lemma 2.2. If $r \ge 2$ and $r \le i \le n$ , then $V$ contains an $(r-1)$ -scattered $\mathbb F_q$ -subspace of dimension $i$ .
Result 4.6 (Delsarte). A rank distance code of $\mathbb F_q^{n\times m}$ , $n\le m$ , with minimum distance $d$ has $|\mathcal C| \le q^{m(n-d+1)}$ .

Significance

The result. Theorem 2.3 is the upper end of the theory of $h$ -scattered subspaces. It shows that the bound $rn/(h+1)$ decreases with $h$ : a stronger intersection condition forces a smaller subspace. Every subspace reaching the bound is a maximum $h$ -scattered subspace. The rest of the paper builds on such subspaces. Its constructions show the bound is sharp when $h+1 \mid r$ . Its intersection numbers with hyperplanes lie in $[rn/(h+1)-n,\ rn/(h+1)-n+h]$ . Its Delsarte-type duality sends maximum $h$ -scattered subspaces to maximum $(n-h-2)$ -scattered ones. Each of these statements presupposes the bound. For $h = r-1$ , the bound $\dim U \le n$ is the geometric counterpart of the Singleton bound for MRD codes.

Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization would provide a Lean model of $h$ -scattered subspaces over a field tower and a rank-metric Singleton bound, and the bound itself as a reusable lemma for the companion missions on constructions, hyperplane intersections and duality. The case $h = 1$ is attributed in the paper to Blokhuis–Lavrauw and is not reproved there, so a complete formal proof must also supply that case.

Difficulty

The obvious approach is to count. Every $h$ -dimensional $\mathbb F_{q^n}$ -subspace meets $U$ in at most $q^h$ vectors. But these subspaces overlap heavily, and a double count of incidences between vectors of $U$ and $h$ -dimensional subspaces does not produce a bound of the form $rn/(h+1)$ . The $h$ -scattered condition must be used on subspaces of every dimension $t < h$ at once, which is the content of Proposition 2.1. The argument for $h = 1$ does not carry over directly either: the paper treats $h = r-1$ , $1 < h < r-1$ with $n \ge h+1$ , and $n < h+1$ as separate cases. The case $h = r-1$ rests on a coding-theoretic input (Result 4.6), and the middle case needs auxiliary subspaces whose existence (Lemma 2.2) holds only when $n \ge h+1$ .

Formalization scope

Field tower. $\mathbb F_q$ and $\mathbb F_{q^n}$ are finite fields F, K with [Algebra F K]. $V$ is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]). The parameters are $q$ = Fintype.card F, $n$ = Module.finrank F K and $r$ = Module.finrank K V.
Subspaces. $\mathbb F_q$ -subspaces are Submodule F V and $\mathbb F_{q^n}$ -subspaces are Submodule K V. The intersection $S\cap U$ is S.restrictScalars F ⊓ U.
The definition. The range $0 < h < r$ and the spanning condition $\langle U\rangle_{\mathbb F_{q^n}} = V$ are clauses of IsHScattered.
No division. $rn/(h+1)$ never appears with division: " $\dim U \le rn/(h+1)$ " is $(h+1)\dim U \le rn$ in $\mathbb N$ .
Result 4.6. The code is a Finset of linear maps. The minimum distance $d$ enters as a lower bound on all pairwise rank distances, with $1 \le d \le n$ .
Lemma 2.2. It carries $r \ge 2$ , which Definition 1.1 forces for $(r-1)$ -scattered subspaces.

Ruling out trivial readings. Without the range $h < r$ , every spanning subspace would be " $h$ -scattered" for $h \ge r$ , and $U = V$ of dimension $rn$ would refute the goal. Without the spanning condition, $U = 0$ would satisfy the bound vacuously. Both conditions are part of the definition, and the goal is the inclusive disjunction for every $h$ -scattered $U$ .

Cited inputs. Result 4.6 is Delsarte's theorem [13], numbered in this paper and posed here with sorry. The case $h = 1$ of the goal is the Blokhuis–Lavrauw bound [4], which the paper cites without proof and says can be obtained by adapting its argument (Zullo's thesis [30]). It is not an item: a complete proof of the goal must cover it.

Infrastructure. A proof needs: dimension arithmetic for restriction of scalars in a tower; the rank–nullity theorem for $\mathbb F_q$ -linear maps; the count of roots of a $q$ -polynomial $\sum_j a_j x^{q^j}$ , for Lemma 2.2; and a rank-metric Singleton bound. The Singleton bound and Lemma 2.2 are reusable beyond this mission. Contributions are welcome on any milestone, on the $h = 1$ case, and on the reduction for $n < h+1$ .

Selected references

B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, arXiv:1906.10590v2 (2020); Combinatorica 41 (2021). https://arxiv.org/abs/1906.10590v2
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81 (2000) 231–243. https://doi.org/10.1023/A:1005283806897
P. Delsarte, Bilinear forms over a finite field, with applications to coding theory, J. Combin. Theory Ser. A 25 (1978) 226–241. https://doi.org/10.1016/0097-3165(78)90015-8
J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets, and their duality, Designs, Codes and Cryptography 88 (2020) 655–675. https://doi.org/10.1007/s10623-019-00703-z

6 thms3 active usersReviewed

Complexity Theory Graph Theory Theoretical Computer Science·Captain: mikedeng1

Most Tensor Problems Are NP-Hard 2: Graph 3-Colorability Reduces to Tensor Bilinear Feasibility over the Reals and over the Complex NumbersResearch Paper

Motivation

A matrix $A \in \mathbb C^{n\times n}$ is singular exactly when the pair of linear systems $\mathbf x^\top A = 0$ , $A\mathbf y = 0$ has a solution with both $\mathbf x$ and $\mathbf y$ nonzero, and this is decided in polynomial time by Gaussian elimination. The natural analogue for a 3-tensor replaces the two linear systems by three families of bilinear equations, one for each way of contracting the tensor against two vectors. For tensors whose dimensions satisfy the Gelfand–Kapranov–Zelevinsky condition, solvability of that system is equivalent to the vanishing of the hyperdeterminant, and for any tensor it is equivalent to $0$ being a singular value in the sense of Lim (2005). The same system appears in multiview geometry (Cohen and Tomasi 1997).

C. J. Hillar and L.-H. Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013; arXiv:0911.1393), show that, unlike the matrix case, this feasibility question is NP-hard over $\mathbb R$ and over $\mathbb C$ (their Theorem 3.7). The proof is a reduction from graph 3-colorability through the polynomial color encoding of a graph, an idea the authors trace to Bayer's thesis (1982) and to Lovász (1994) and De Loera (1995). This mission formalizes that reduction and its consequence for tensor singular values (Theorem 6.2).

Setting

A 3-tensor over a field $F$ is an array $\mathcal A = [\![a_{ijk}]\!] \in F^{l\times m\times n}$ . Its slices are the matrices $A_i(j,k) = B_j(i,k) = C_k(i,j) = a_{ijk}$ , all read off the same array.

Tensor bilinear feasibility (Problem 3.1) asks, for a rational tensor $\mathcal A \in \mathbb Q^{l\times m\times n}$ and $F = \mathbb R$ or $\mathbb C$ , whether the system (9)

\mathbf v^\top A_i\mathbf w = 0\ (i \le l),\qquad \mathbf u^\top B_j \mathbf w = 0\ (j \le m),\qquad \mathbf u^\top C_k \mathbf v = 0\ (k \le n)

has a solution $\mathbf u \in F^l$ , $\mathbf v\in F^m$ , $\mathbf w \in F^n$ with each of the three vectors nonzero. In Lean this is TBF A.

The color encoding $C_G$ of a graph $G = (V,E)$ on $v$ vertices (Definition 2.9) is the set of $4v$ quadratics in $x_1,\dots,x_v,y_1,\dots,y_v,z$ :

x_iy_i - z^2,\quad y_iz - x_i^2,\quad x_iz - y_i^2,\quad \sum_{j:\{i,j\}\in E}(x_i^2 + x_ix_j + x_j^2),\qquad i = 1,\dots,v .

The tensor $\mathcal A_G \in \mathbb Z^{l\times m\times n}$ of the proof of Theorem 3.7 has $m = n = 2v+1$ and $l = v(2v+5)$ slices: $v(2v+1)$ slices whose bilinear forms are the $2\times 2$ minors of the matrix $[\mathbf v\ \mathbf w]$ , then $3v + v$ slices whose bilinear forms restrict, on $\mathbf w = \mathbf v$ , to the polynomials of $C_G$ (Lean: AG G).

The tensor $\mathcal B$ of Lemma 3.6 doubles a real tensor $\mathcal A$ into $\mathbb R^{2l\times 2m\times 2n}$ through the slices $B_i = \left[\begin{smallmatrix} A_i & 0 \\ 0 & -A_i\end{smallmatrix}\right]$ , $B_{l+i} = \left[\begin{smallmatrix} 0 & A_i \\ A_i & 0\end{smallmatrix}\right]$ (Lean: doubling A).

An $\ell^2$ -singular value $\sigma$ of $\mathcal A$ (Definition 6.1) admits nonzero $\mathbf u,\mathbf v,\mathbf w$ with $\sum_{j,k}a_{ijk}v_jw_k = \sigma u_i$ and the two analogous equations; an $\ell^3$ -singular value has $\sigma u_i^2$ , $\sigma v_j^2$ , $\sigma w_k^2$ on the right. At $\sigma = 0$ both reduce to (9).

Formalization targets

Goal: Theorem 3.7

\textsf{3-COLORABILITY} \le_p \textsf{TBF}_{\mathbb R} \quad\text{and}\quad \textsf{3-COLORABILITY} \le_p \textsf{TBF}_{\mathbb C},

polynomial-time many-one reductions between languages of binary codes. NP-hardness of tensor bilinear feasibility then follows from the NP-completeness of 3-colorability (Karp 1972), which is cited and not part of the statement.

Milestones, in the order the proof uses them

Lemma 2.10. $C_G$ has a nonzero complex zero iff $G$ is 3-colorable.
The minors (proof of Theorem 3.7). For nonzero $\mathbf v, \mathbf w \in \mathbb C^N$ , all $2\times2$ minors of $[\mathbf v\ \mathbf w]$ vanish iff $\mathbf v = c\mathbf w$ for some $c \in \mathbb C$ .
Correctness over $\mathbb C$ (proof of Theorem 3.7). For $v \ge 1$ , $\mathrm{TBF}_{\mathbb C}(\mathcal A_G) \iff G$ is 3-colorable.
Lemma 3.6. $\mathrm{TBF}_{\mathbb R}(\mathcal B) \iff \mathrm{TBF}_{\mathbb C}(\mathcal A)$ for real $\mathcal A$ .
Theorem 6.2 (further result). 3-colorability reduces to deciding whether $0$ is an $\ell^2$ -singular value, and whether it is an $\ell^3$ -singular value, over $\mathbb R$ and over $\mathbb C$ .

Significance

Theorem 3.7 is the hub of the paper's bilinear results: Section 6 derives from it the NP-hardness of deciding whether $0$ is a tensor singular value (Theorem 6.2), and the triple bilinear problem (Theorem 3.8) is handled by the same techniques. It separates tensors from matrices in a precise sense: the matrix analogue of (9) is decided by a determinant, while the tensor version encodes a classical NP-complete problem. It does not settle the hardness of the hyperdeterminant, since the dimensions $l = v(2v+5)$ , $m = n = 2v+1$ of $\mathcal A_G$ violate the GKZ condition; the paper leaves that as a conjecture.

The result is proved in the paper; none of it is formalized on Prove2Me or, to our knowledge, elsewhere. A complete development produces a machine-checked polynomial-time reduction in Cook's Turing-machine model between two concrete algebraic problems, the color-encoding lemma for 3-colorability (reusable by any reduction that goes through polynomial systems, including Theorems 1.3 and 2.6 of the same paper), and the realification of bilinear systems.

Difficulty

The algebra of the reduction is short; two places need care. First, the bilinear system does not see $C_G$ directly: (9) involves two independent vectors $\mathbf v, \mathbf w$ , and the reduction recovers the quadratic system only because the minors force $\mathbf v = c\mathbf w$ , which requires both vectors to be nonzero. Second, the converse direction must produce a nonzero $\mathbf u$ satisfying the second and third families, a homogeneous linear system of $4v+2$ equations in $l = v(2v+5)$ unknowns; this works only when $l > 4v+2$ , which fails for the empty graph, so the reduction has to treat $v = 0$ separately.

The goal also asks for polynomial-time computability in a Turing-machine model: decoding a graph code, rejecting malformed words, and writing the binary code of $\mathcal A_G$ (or of its doubling over $\mathbb R$ ). This bookkeeping, not the algebra, is the bulk of a complete proof.

Formalization scope

Tensors are functions I → J → K → F over finite index types, 0-based: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). Problem 3.1 requires $\mathbf u$ , $\mathbf v$ , $\mathbf w$ each nonzero, not merely $(\mathbf u, \mathbf v, \mathbf w) \neq 0$ , and the three equation families come from one tensor.
The doubled tensor of Lemma 3.6 is indexed by I ⊕ I, J ⊕ J, K ⊕ K, with Sum.inr i standing for the paper's index $l+i$ . Lemma 3.6 is stated for this explicit $\mathcal B$ ; a bare existential would be witnessed by any tensor with the right truth value. Only the equivalence of existence is stated, not the paper's "one-to-one" correspondence (which pairs $\mathbf u' = (\mathbf p,\mathbf q)$ with the conjugate-type vector $\mathbf p - i\mathbf q$ ).
The paper does not print the matrices of the last $4v$ slices of $\mathcal A_G$ . The mission fixes the bilinearizations $x_i\hat y_i - z\hat z$ , $y_i\hat z - x_i\hat x_i$ , $x_i\hat z - y_i\hat y_i$ and $\sum_{j\sim i}(x_i\hat x_i + x_i\hat x_j + x_j\hat x_j)$ ; each restricts to the printed polynomial on $\mathbf w = \mathbf v$ .
"Nontrivial zero" in the minors claim is read as both $\mathbf v$ and $\mathbf w$ nonzero; the correctness milestone over $\mathbb C$ assumes $v \geq 1$ , since for $v = 0$ the printed tensor has no slices and its system (9) is infeasible.
"Polynomially reducible" is formalized as Cook–Karp many-one reducibility (CookPvsNP.PolyReducible), which the paper's proof constructs and which implies the paper's oracle notion of §1.4. "NP-hard" in Theorem 6.2 is rendered the same way, and "( $\ell^2$ or $\ell^3$ )" as the claim for each notion. Rational inputs are coded as numerator and denominator in binary; tensors as $l, m, n$ and then their entries in lexicographic order.
The singular-value equations (20)–(21) are taken literally over $\mathbb C$ , without conjugates and without normalization; only $\sigma = 0$ is used, where they are scale-free.
NP-completeness of 3-colorability is cited, not formalized; no statement mentions P, NP-membership, or hyperdeterminants.
A trivializing formalization is ruled out: the goal is the polynomial-time reduction, not the bare equivalence of yes-instances, and the reduction must handle every input word.

The mission reuses the published definitions CookPvsNP_defs (Turing machines, polynomial-time computability, many-one reducibility) and ProjSchedTW.Complexity.Encoding (the binary alphabet and number codes), and Mathlib's SimpleGraph.Colorable. Contributions welcome: the algebraic milestones (Lemma 2.10, the minors, Lemma 3.6) are independent and self-contained; a library of polynomial-time computable list and arithmetic operations on BSym codes would serve both this goal and Theorem 6.2.

Selected references

C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Art. 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393)
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP, 2005. https://arxiv.org/abs/math/0607648
I. M. Gelfand, M. M. Kapranov, A. V. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkhäuser, 1994. https://doi.org/10.1007/978-0-8176-4771-1
S. A. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

14 thms3 active usersReviewed

Complexity Theory Graph Theory Theoretical Computer Science·Captain: mikedeng1

Most Tensor Problems Are NP-Hard 1: Graph 3-Colorability Reduces to Deciding Whether 0 Is an Eigenvalue of a Rational 3-Tensor over the RealsResearch Paper

Motivation

Eigenvalues of matrices are computable in polynomial time to any accuracy, and numerical linear algebra rests on that fact. Higher-order tensors appear in statistics (moment and cumulant tensors), signal processing, quantum information and polynomial optimization, and several notions of tensor eigenvalue were proposed for them, independently by Lim and by Qi in 2005 (Lim 2005; Qi 2005). Hillar and Lim (J. ACM 60(6), 2013, Art. 45; arXiv:0911.1393) showed that most of the natural tensor analogues of tractable matrix problems are NP-hard. Their first example, Theorem 1.3, concerns the simplest one: deciding whether a given number is an eigenvalue of a 3-tensor.

This mission formalizes that theorem together with the lemmas its proof uses. The reduction starts from graph 3-colorability, and its intermediate step, quadratic feasibility (Theorem 2.6), is reused throughout the paper: the bilinear, singular value and triple-bilinear results all go through the same color encoding.

Setting

A 3-tensor over a field $F$ is an array $\mathcal A=[\![a_{ijk}]\!]\in F^{n\times n\times n}$ . A scalar $\lambda\in F$ is an eigenvalue of $\mathcal A$ (eq. (3) of the paper) if there is a nonzero $\mathbf x\in F^n$ with

\sum_{i,j=1}^{n}a_{ijk}\,x_ix_j=\lambda x_k,\qquad k=1,\dots,n.

The sum is over the first two indices. For $\lambda=0$ the condition is invariant under scaling of $\mathbf x$ , so no normalization enters.

Problem 1.2 (tensor $\lambda$ -eigenvalue) fixes $F\in\{\mathbb R,\mathbb C\}$ and $\lambda\in\mathbb Q$ , and asks, for a rational tensor $\mathcal A\in\mathbb Q^{n\times n\times n}$ , whether $\lambda$ is an eigenvalue of $\mathcal A$ with an eigenvector in $F^n$ .

Problem 2.2 (quadratic feasibility) asks, for rational matrices $A_1,\dots,A_m\in\mathbb Q^{n\times n}$ , whether the system $\mathbf x^\top A_i\mathbf x=0$ ( $i=1,\dots,m$ ) has a nonzero solution $\mathbf x\in F^n$ .

A proper 3-coloring of a simple graph $G=(V,E)$ assigns one of three colors to each vertex so that adjacent vertices receive different colors.

The color encoding $C_G$ of a graph on vertices $1,\dots,v$ (Definition 2.9) is the family of $4v$ quadratics in $x_1,\dots,x_v,y_1,\dots,y_v,z$ :

x_iy_i-z^2,\quad y_iz-x_i^2,\quad x_iz-y_i^2,\quad \sum_{j:\{i,j\}\in E}(x_i^2+x_ix_j+x_j^2),\qquad i=1,\dots,v.

Lemma 2.7 replaces a complex quadratic system by a real one of twice the size, and Lemma 2.8 pads a real system to a square one. Applied to $C_G$ , they give $N$ real quadratics $\mathbf x^\top B_k\mathbf x$ in $N$ unknowns. The tensor $T_G$ with $a_{ijk}=(B_k)_{ij}$ is the output of the reduction.

Formalization targets

Goal: Theorem 1.3

\textsf{3-COL}\ \le_p\ \textsf{TENSOR-0-EIG}_{\mathbb R}.

Graph 3-colorability is polynomial-time many-one reducible to the language of binary codes of rational tensors having $0$ as a real eigenvalue.

Milestones, in the order the proof uses them

Lemma 2.10. $C_G$ has a nonzero complex solution if and only if $G$ is 3-colorable.
Lemma 2.7. The $2m$ real equations with matrices $\begin{bmatrix}A_i&0\\0&-A_i\end{bmatrix}$ and $\begin{bmatrix}0&A_i\\A_i&0\end{bmatrix}$ have a nonzero real solution iff $\{\mathbf z^\top A_i\mathbf z=0\}$ has a nonzero complex solution.
Lemma 2.8. Padding to $r\ge m+1$ equations in $s\ge n$ unknowns preserves real feasibility.
Theorem 2.6. $\textsf{3-COL}\le_p$ quadratic feasibility over $\mathbb R$ and over $\mathbb C$ .
Proof of Theorem 1.3, first step. $0$ is a real eigenvalue of $\mathcal A$ iff the square system $\mathbf x^\top A_k\mathbf x=0$ , $A_k(i,j)=a_{ijk}$ , has a nonzero real solution.
Proof of Theorem 1.3, the construction. $G$ is 3-colorable iff $0$ is a real eigenvalue of $T_G$ .

Significance

The result. Theorem 1.3 shows that deciding whether $0$ is an eigenvalue of a rational 3-tensor over $\mathbb R$ is NP-hard, in contrast to the matrix case. Because the instance is a single rational tensor with small integer entries, the hardness does not come from numerical precision: it is a property of the exact problem. The same encoding underlies the paper's hardness of approximating an eigenvector (Theorem 1.5) and its remarks on counting eigenvectors (Corollary 1.16).

Formalizing it. The result is proved in the paper, but no part of it is machine-checked. The mission adds three things. It gives a precise language-level statement of what "polynomially reducible" means for this problem. It gives a checked equivalence between 3-colorability and the eigenvalue condition for the explicit tensor $T_G$ . And it gives reusable statements about homogeneous quadratic systems (realification and padding), which the bilinear and singular value missions of this series also need.

Difficulty

The algebraic core is Lemma 2.10, and its reverse direction is where a first attempt fails. The fourth family of $C_G$ does not say that each term $x_i^2+x_ix_j+x_j^2$ vanishes; it says only that their sum over the neighbours of $i$ vanishes, over $\mathbb C$ , where nonzero terms can cancel. A common zero yields a coloring only after the first three families have pinned down each coordinate, and the case $z=0$ must be excluded separately.

Lemma 2.7 needs care because the matrices $A_i$ are not assumed symmetric: the imaginary part of $\mathbf z^\top A\mathbf z$ is $\mathbf u^\top A\mathbf v+\mathbf v^\top A\mathbf u$ , not $2\mathbf u^\top A\mathbf v$ . Lemma 2.8 uses that $\mathbb R$ is formally real; it fails over $\mathbb C$ .

At the language level, the reduction must be exhibited as a Turing machine computation on binary codes in polynomial time. That is bookkeeping, but it is the part the paper does not write down.

Formalization scope

Tensors and vectors. Tensors are arrays Fin n → Fin n → Fin n → F, vectors Fin n → F, and indices are 0-based. The eigenvalue condition is eq. (3) verbatim, without normalization; for $\lambda=0$ none is needed. Rational data are cast into $\mathbb R$ or $\mathbb C$ .
Quadratic polynomials. A homogeneous quadratic is a (not necessarily symmetric) rational matrix $M$ , read as $\mathbf x^\top M\mathbf x$ , and the monomial $x_ax_b$ is the matrix unit $E_{ab}$ . A vertex without neighbours contributes the zero polynomial to $C_G$ .
Choices in the construction. The square size is $N=8v+2$ . It meets Lemma 2.8's bounds $r\ge 8v+1$ and $s\ge 4v+2$ for every $v\ge 0$ ; Example 1.4's count differs and is not used.
Reducibility. "Polynomially reducible" is Cook's polynomial-time many-one reducibility (CookPvsNP.PolyReducible, published definition CookPvsNP_defs). The paper's reduction maps one graph to one tensor, and a many-one reduction implies the oracle notion of its §1.4.
Binary codes. Instances are coded over the alphabet BSym with the binary codes of the published definition ProjSchedTW.Complexity.Encoding. A graph is $\nu$ followed by its adjacency matrix. A rational is its numerator then its denominator. A tensor is $n$ followed by its entries in lexicographic order. The target language contains all rational tensors, not only integral ones.
Not formalized. NP-completeness of 3-colorability (Karp 1972) is cited, not formalized, and the goal states only the reduction. Approximation (Theorem 1.5), counting (Corollary 1.16) and the solution count of Example 1.4 are out of scope.
Trivializations ruled out. Every feasibility statement requires a nonzero solution, since the zero vector solves every homogeneous system. The goal includes polynomial-time computability of the reduction, not just the existence of an equivalence-preserving map, which would be trivial. The milestones concern the paper's explicit $C_G$ and $T_G$ , not an arbitrary tensor.

Contributions are welcome in four places:

proofs of the milestones;
a polynomial-time Turing machine computing $G\mapsto T_G$ on codes;
general lemmas on homogeneous quadratic systems over formally real fields;
a composition (transitivity) lemma for CookPvsNP.PolyReducible.

Selected references

C. J. Hillar and 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)
L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 2005, pp. 129–132. https://doi.org/10.1109/CAMAP.2005.1574201
L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40(6), 2005, pp. 1302–1324. https://doi.org/10.1016/j.jsc.2005.05.007
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, pp. 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problem description, 2000. https://www.claymath.org/millennium/p-vs-np/

11 thms3 active usersReviewed

Analysis Probability Random Matrix Theory·Captain: mikedeng1

User-Friendly Tail Bounds for Sums of Random Matrices V: The Matrix Azuma Inequality for Adapted Sequences with Semidefinite Bounds on the Squared DifferencesResearch Paper

Motivation

Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.

Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.

Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.

Setting

All matrices are $d\times d$ with complex entries, $d\ge 1$ . A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. $A$ , $\lambda_{\max}(A)$ is its largest eigenvalue and $\|A\|$ its spectral norm. Functions of s.a. matrices are defined spectrally: if $A=Q\Lambda Q^*$ then $e^{A}=Qe^{\Lambda}Q^*$ , and $\log$ is defined the same way on positive-definite matrices. $A\preceq B$ is the semidefinite order: $B-A$ is positive semidefinite.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $\mathcal F_0\subset\mathcal F_1\subset\cdots\subset\mathcal F$ , and write $\mathbb E_k[\,\cdot\,]=\mathbb E[\,\cdot\mid\mathcal F_k]$ . The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence $X_1,\dots,X_n$ of random matrices is adapted when each $X_k$ is $\mathcal F_k$ -measurable. A matrix martingale is an adapted sequence of s.a. matrices $Y_k$ with $\mathbb E\|Y_k\|<\infty$ and $\mathbb E_{k-1}Y_k=Y_{k-1}$ ; its difference sequence $X_k=Y_k-Y_{k-1}$ satisfies $\mathbb E_{k-1}X_k=0$ .

The hypotheses of the main theorem are: $X_1,\dots,X_n$ is an adapted sequence of random s.a. matrices, and $A_1,\dots,A_n$ is a fixed (non-random) sequence of s.a. matrices, with

\mathbb E_{k-1}X_k = 0 \qquad\text{and}\qquad X_k^2\preceq A_k^2\ \text{ almost surely.}

The variance parameter is $\sigma^2 := \big\|\sum_k A_k^2\big\|$ .

Formalization targets

Goal: Theorem 7.1 (Matrix Azuma), p. 27

For all $t\ge 0$ ,

\mathbb P\Big\{\lambda_{\max}\Big(\sum_{k}X_k\Big)\ge t\Big\}\le d\cdot e^{-t^2/8\sigma^2}.

Milestones

In the order they are used:

Display (2.6), Golden–Thompson: $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ for s.a. $A,H$ .
Proposition 3.1, the Laplace transform method: $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}$ .
Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E e^{X})$ .
Lemma 4.3, Rademacher half: $\mathbb E e^{\varepsilon\theta A}\preceq e^{\theta^2A^2/2}$ .
Lemma 7.6 (Symmetrization): $\mathbb E\operatorname{tr}e^{H+X}\le\mathbb E\operatorname{tr}e^{H+2\varepsilon X}$ when $\mathbb EX=0$ and $\varepsilon$ is an independent Rademacher variable.
Lemma 7.7 (Azuma cgf): $\log\mathbb E[e^{2\varepsilon\theta X}\mid X]\preceq2\theta^2A^2$ when $X^2\preceq A^2$ .
Display (7.5): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(2\theta^2\sum_kA_k^2)$ under the hypotheses of the goal.

Further statements

Corollary 7.2 is the martingale form, $\mathbb P\{\lambda_{\max}(Y_n-\mathbb EY_n)\ge t\}\le d\,e^{-t^2/8\sigma^2}$ . Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, $\mathbb P\{\lambda_{\max}(H(z)-\mathbb EH(z))\ge t\}\le d\,e^{-t^2/8\sigma^2}$ for a matrix-valued function $H$ of independent variables whose changes in one coordinate $k$ have squares bounded by $A_k^2$ .

Significance

The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor $d$ , and a variance parameter equal to the norm of the sum $\sum_kA_k^2$ rather than the sum of the norms $\sum_k\|A_k\|^2$ . In the commuting case the two coincide; in general the first can be smaller by a factor of up to $n$ . The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).

Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.

Difficulty

The scalar proof of Azuma's inequality multiplies conditional moment generating functions, $\mathbb E e^{\theta\sum X_k}=\mathbb E\big[e^{\theta\sum_{k<n}X_k}\,\mathbb E_{n-1}e^{\theta X_n}\big]$ , and bounds each factor. For matrices this fails: $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, and $\operatorname{tr}e^{A+B+C}\le\operatorname{tr}(e^Ae^Be^C)$ is false, so the Golden–Thompson inequality cannot be iterated over $n$ terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis $X_k^2\preceq A_k^2$ bounds squares, not the matrices themselves; it does not give $X_k\preceq A_k$ , so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and $\preceq$ is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. $\lambda_{\max}$ is the supremum of the real spectrum, which is why $d\ge1$ is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by $k=1,\dots,n$ , so $\mathcal F_{k-1}$ is never truncated. The bound $X_k^2\preceq A_k^2$ is required almost surely. The bounds $A_k$ are deterministic matrices. The infimum over $\theta>0$ in Proposition 3.1 is posed as the bound for each $\theta>0$ at which the expectation is finite.

The hypotheses must not be made vacuous. Integrability of each $X_k$ is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is $0$ and the centring hypothesis would say nothing. The $X_k$ are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.

Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given $X$ is replaced by the expectation over $\varepsilon$ at each fixed value $x$ with $x^2\preceq A^2$ ; by independence these agree. Corollary 7.2 adds the hypothesis that $Y_0$ is almost surely constant, without which $Y_n-\mathbb EY_n\neq\sum_kX_k$ .

A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.

Selected references

J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited version arXiv:1004.4389v7 (2011). https://arxiv.org/abs/1004.4389v7
R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
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
J. A. Tropp, Freedman's inequality for matrix martingales, Electron. Commun. Probab. 16 (2011) 262–270. https://arxiv.org/abs/1101.3039
R. I. Oliveira, Concentration of the adjacency matrix and of the Laplacian in random graphs with independent edges, arXiv:0911.0600 (2010). https://arxiv.org/abs/0911.0600
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer (1998) 195–248. https://doi.org/10.1007/978-3-662-12788-9_6
R. Bhatia, Matrix Analysis, Springer GTM 169 (1997), Sec. IX.3. https://doi.org/10.1007/978-1-4612-0653-8
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

10 thms3 active usersReviewed

Missions

Geometric Deep Learning III: An n × n Matrix Commutes with the Cyclic Shift S if and only if It Is Circulant, So Convolution Is Shift EquivarianceTextbook

Why convolution, and why the shift

Setting

Formalization targets

Goal: commuting with the shift characterises circulant matrices

Milestones, in attack order

Companion: the Convolution Theorem

Significance

Difficulty

Formalization scope

Selected references

Commutant Structure of U⊗(n−1) ⊗ U* Transformations: The Operator Basis v^{ab}_{ij}(α) Is a Linear Combination of Partially Transposed Permutation Operators, and ConverselyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9

Milestones

Significance

Difficulty

Formalization scope

Selected references

On a Family of a Linear Maps from Mₙ(ℂ) to Mₙ²(ℂ): Φ[α, β] on M₃(ℂ) Is 2-Positive and Not Completely Positive Exactly When β ≤ −0.2 and α Lies in an Explicit IntervalResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Lectures on Modern Convex Optimization V: Semidefinite Representability of Symmetric Functions of EigenvaluesTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 4.2.1 (p. 151)

Milestones, in attack order

A further level

Significance

Difficulty

Formalization scope

Selected references

Improvements in Quantum SDP-Solving with Applications 1: A Unitary Preparing a Purification of a Subnormalized Density Operator ϱ Gives an Exact (1, w+a+1, 0)-Block-Encoding of ϱResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Improvements in Quantum SDP-Solving with Applications 2: A Two-Outcome Measurement Implemented With Bias ε Gives a (1, a+1, ε)-Block-Encoding of Its POVM Element MResearch Paper

Motivation

Setting

Formalization targets

Goal (§4.1, p. 25)

Milestones (all p. 25, in the order of the derivation)

Significance

Difficulty

Formalization scope

Selected references

Quadratic Matrix Inequalities with Applications to Data-Based Control IV: Noisy Data Are Informative for Quadratic Stabilization iff an LMI in (P, L, β) Is FeasibleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 2: Chains to the Rows of Sum ≥ 1 of a Super-Stochastic F Give ρ(F) < 1 under Condition (2.5)Research Paper

Why spectral bounds for super-stochastic matrices

Setting

Formalization targets

Goal: Theorem 2.6 (p. 9)

Milestones (the steps of the proof on p. 9)

Companion results

Significance

Difficulty

Formalization scope

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 1: Chains to the Unit Rows of a Sub-Stochastic F Give ρ(F) ≤ (1 − (1 − α₁)α₂^|C|)^(1/(|C|+1)) < 1Research Paper