Linear algebra · Prove2Me

Completed

Control Theory Dynamical Systems·Captain: mikedeng1

Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems 2: An Explicit Bilinear System Whose Field x ↦ P̃(x)⁻¹x Is Not a Gradient, So (3.8) FailsResearch Paper

Motivation

Balanced truncation reduces a large control system to a small one by discarding the states that are both hard to reach and hard to observe. For linear systems "hard to reach" is measured exactly by the controllability Gramian $P$ : the minimal input energy needed to steer the system from $0$ to $x_0$ is $x_0^T P^{-1} x_0$ . For bilinear systems, in which the input also multiplies the state, no such exact formula is known, and several papers have tried to describe the nonlinear controllability energy functional $E_c$ through state-dependent Gramians.

Gray and Mesko ([25] in the paper, 1998) and Condon and Ivanov ([11], 2005) stated that, for $x \neq 0$ with $\|x\|$ sufficiently small, the gradient of $E_c$ is given by a state-dependent Gramian $\tilde P(x)$ of the linearization, $\nabla E_c(x) = \tilde P(x)^{-1}x$ , and derived from this comparison inequalities between $E_c$ and the algebraic Gramian. Benner and Damm (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X) observed that this formula needs an integrability condition that is not automatic, and gave an explicit two-dimensional system for which it fails (Example 3.3, pp. 697–698). This mission formalizes that counterexample.

Setting

A bilinear control system with state $x(t) \in \mathbb R^n$ and input $u(t) \in \mathbb R^m$ is

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

with real matrices $A, N_1, \dots, N_m \in \mathbb R^{n\times n}$ and $B \in \mathbb R^{n \times m}$ ; write $b_j$ for the $j$ -th column of $B$ . The system is locally controllable if the pair $(A, B)$ is controllable, that is, the Kalman matrix $[B, AB, \dots, A^{n-1}B]$ has rank $n$ .

Linearizing the system at a state $x$ and the input $u = 0$ gives a linear system whose input matrix has columns $N_j x + b_j$ . Its controllability Gramian $\tilde P(x)$ is the solution of the Lyapunov equation

A \tilde P(x) + \tilde P(x) A^T = -\sum_{j=1}^m (N_j x + b_j)(N_j x + b_j)^T. \tag{3.9}

When $A$ is stable, (3.9) has exactly one solution for every $x$ , and it is symmetric. The claim under test is

\nabla E_c(x) = \tilde P(x)^{-1} x \qquad \text{for } x \neq 0,\ \|x\| \text{ sufficiently small.} \tag{3.8}

A vector field $F$ on an open set is integrable (a gradient field) if $F = \nabla E$ for some real function $E$ .

Example 3.3 is the single-input system ( $n = 2$ , $m = 1$ ) with

A = \begin{bmatrix} -1 & 0 \\ 0 & -2 \end{bmatrix}, \qquad N = \nu \begin{bmatrix} 0 & 1 \\ 1 & 0 \end{bmatrix}, \qquad b = \begin{bmatrix} 1 \\ 1 \end{bmatrix},

and a real parameter $\nu$ . In Lean these are exA, exN ν and exb (with exB the $2\times 1$ matrix $[b]$ ), equation (3.9) is IsLinGramian, and controllability is IsControllable.

Formalization targets

Goal: Example 3.3

For every $\nu \neq 0$ , with $\tilde P(x)$ solving (3.9) for every $x \in \mathbb R^2$ : the pair $(A, b)$ is controllable, and for every $\varepsilon > 0$ there is no $E : \mathbb R^2 \to \mathbb R$ with

\nabla E(x) = \tilde P(x)^{-1}x \qquad \text{for all } 0 < \|x\| < \varepsilon .

The goal refutes every potential $E$ , not only $E_c$ , so it does not depend on how $E_c$ is defined; it is exactly the statement that the field is not integrable on any punctured neighbourhood of the origin, which is how (3.8) is claimed.

Milestones, in the order the example uses them

Local controllability: $(A, b)$ is controllable.
The derivative of $F(x) = \tilde P(x)^{-1}x$ (general $n$ , $m$ ): where $\tilde P(x)$ is invertible,

F'(x)h = \tilde P(x)^{-1}h - \tilde P(x)^{-1}\tilde P'_x(h)\tilde P(x)^{-1}x, \qquad A\tilde P'_x(h) + \tilde P'_x(h)A^T = -\sum_{j}\big(N_j h (N_j x + b_j)^T + (N_j x + b_j)h^TN_j^T\big).

The explicit Gramian at $x = \xi(1,1)^T$ , $1 + \nu\xi \neq 0$ :

\tilde P(x) = (1+\nu\xi)^2\begin{bmatrix} 1/2 & 1/3 \\ 1/3 & 1/4\end{bmatrix}, \qquad \tilde P(x)^{-1} = \frac{6}{(1+\nu\xi)^2}\begin{bmatrix} 3 & -4 \\ -4 & 6\end{bmatrix}.

The non-symmetric Jacobian at $x = \xi(1,1)^T$ , $\nu\xi \neq 0$ , $1+\nu\xi \neq 0$ :

F'(x) = \tilde P(x)^{-1} + \frac{12\nu\xi}{(1+\nu\xi)^3}\begin{bmatrix} 2 & -1 \\ -4 & 2\end{bmatrix}, \quad \text{not symmetric.}

Significance

The result. The example shows that the state-dependent Gramian $\tilde P(x)$ of the linearization does not, in general, describe the controllability energy of a bilinear system through (3.8), even for a locally controllable system and arbitrarily close to the origin. As a consequence, the inequalities $E_c(x_0) > x_0^TP^{-1}x_0$ and $E_o(x_0) < x_0^TQx_0$ derived in [25, 11] from (3.8) lose their justification, and the comparison of $E_c$ with the algebraic Gramian requires the different argument the paper develops in its later sections. The example is a minimal one: two states, one input, one coupling parameter.

Formalizing it. The counterexample is proved in the paper by a hand computation through Kronecker products, and that computation contains a sign slip (see below); a machine-checked version settles the claim independently of it. The result is proved in the paper and, to our knowledge, has not been formalized anywhere. The general derivative formula (milestone 2) is reusable for any parametric Lyapunov equation.

Difficulty

The obvious route is to compute the Jacobian of $F$ at one point and observe that it is not symmetric. Two steps of this route need care. First, $\tilde P(x)$ is defined only implicitly, through (3.9) at every point, so its differentiability in $x$ , and that of its inverse, must be derived from the invertibility of the Lyapunov operator $X \mapsto AX + XA^T$ and of $\tilde P(x)$ near the point. Second, passing from "the Jacobian of $F$ is not symmetric" to " $F$ is not a gradient" requires the symmetry of second derivatives of a function that is only assumed differentiable with gradient $F$ on a punctured ball; the regularity of $E$ is inherited from that of $F$ , not assumed. The goal is also not a statement about a single point: it must hold for every radius $\varepsilon$ , so the asymmetry must be exhibited at points arbitrarily close to the origin, where it is of order $\nu\xi$ .

Formalization scope

Scalars are real; states are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the paper's indices $j = 1, \dots, m$ are Fin m. In the goal the plane is EuclideanSpace ℝ (Fin 2) and the potential is required to satisfy HasGradientAt at each point of the punctured ball $0 < \|x\| < \varepsilon$ , with no further regularity.
$\tilde P$ enters as an arbitrary function satisfying (3.9) at every point. For the example data (3.9) has exactly one solution at every $x$ , so this is the paper's "defined by (3.9)", and the hypothesis is satisfiable.
Added hypothesis $\nu \neq 0$ . The paper says $\nu$ is "irrelevant for the computation", but its asymmetry term is proportional to $\nu\xi$ ; at $\nu = 0$ the Gramian is constant and the field is a gradient.
Repaired sign. The equation for $\tilde P'_x(h)$ on p. 697 is printed without parentheses after the minus sign, and the Kronecker formula for $\operatorname{vec}\tilde P'_x(h)$ drops the minus sign of (3.9). Milestone 2 places the minus sign on both terms. The matrix $\frac{12\nu\xi}{(1+\nu\xi)^3}\left[\begin{smallmatrix} 2 & -1 \\ -4 & 2\end{smallmatrix}\right]$ of the paper is, with the sign restored, the matrix of $h \mapsto -\tilde P^{-1}\tilde P'_x(h)\tilde P^{-1}x$ ; milestone 4 therefore states $F'(x) = \tilde P(x)^{-1}$ plus this matrix. The non-symmetry conclusion is unchanged.
Matrix inverses are Mathlib's Matrix.inv, which returns $0$ at singular matrices; $\tilde P(x)$ is invertible near the origin, and milestones 2–4 assume invertibility (or $1 + \nu\xi \neq 0$ ) where they use it.
The observability half of (3.8), $\nabla E_o(x) = \tilde Q(x)x$ , which the paper says "can be argued similarly" without a proof, is not part of the mission.
A trivializing formalization is ruled out: $\tilde P$ is pinned by (3.9) at every point (a free $\tilde P$ would make the claim meaningless), and non-integrability is stated as the non-existence of a potential, not as the non-symmetry of some matrix.

Contributions welcome: proofs of the four milestones, in particular the smooth dependence of the solution of a Lyapunov equation on its right-hand side (milestone 2), which is general and reusable.

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
W. S. Gray, J. Mesko, Energy functions and algebraic Gramians for bilinear systems, Proc. 4th IFAC Nonlinear Control Systems Design Symposium, Enschede, 1998, pp. 103–108.
M. Condon, R. Ivanov, Nonlinear systems — algebraic Gramians and model reduction, COMPEL 24, 202–219, 2005.
E. I. Verriest, Time variant balancing and nonlinear balanced realizations, in Model Order Reduction: Theory, Research Aspects and Applications, Mathematics in Industry 13, Springer, 2008, pp. 203–222.

7 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Baumgarten 2018: How to (Un-) Quantum Mechanics — Phase-Space AlgebraResearch Paper

Motivation

C. Baumgarten's essay How to (Un-) Quantum Mechanics (arXiv:1810.06981, v2 2025) argues that much of the mathematical formalism usually presented as specifically "quantum" — Heisenberg's equation of motion, commutators, eigenvalue problems, the real Pauli and Dirac algebras — already follows from classical linear Hamiltonian mechanics on an abstract phase space. The physical and philosophical claims of the paper are outside the scope of a formalization, but its argument rests on a compact chain of linear-algebra facts stated in Sections IV–VI (pp. 13–20). This mission formalizes exactly that chain, so that the mathematical part of the argument can be checked independently of its interpretation.

Setting

Fix a number $n \ge 0$ of degrees of freedom. A phase-space vector is $\psi = (q_1,p_1,\dots,q_n,p_n)^T \in \mathbb R^{2n}$ . The symplectic unit matrix is the Kronecker product

\gamma_0 = \mathbf 1_n \otimes \eta_0, \qquad \eta_0 = \begin{pmatrix}0 & 1\\ -1 & 0\end{pmatrix}.

A real $2n\times 2n$ matrix is Hamiltonian if it equals $\gamma_0 A$ with $A$ symmetric, skew-Hamiltonian if it equals $\gamma_0 B$ with $B$ skew-symmetric, and symplectic if $M\gamma_0M^T = \gamma_0$ .

Linear Hamiltonian motion is $\dot\psi = H\psi$ with $H$ Hamiltonian (the paper's Eq. 35, coming from the quadratic Hamiltonian $\tfrac12\psi^TA\psi$ ). A matrix of second moments $\Sigma(\tau)$ (in the paper an average $\langle\psi\psi^T\rangle$ ) then evolves by

\dot\Sigma = H\Sigma + \Sigma H^T \qquad\text{(Eq. 40)},

and the autocorrelation matrix is $S = \Sigma\gamma_0^T$ .

Target

The goal theorem combines the conclusions drawn on pp. 16–17: for $H$ Hamiltonian and $\Sigma$ a symmetric solution of Eq. (40), the autocorrelation matrix satisfies, for every time $\tau$ ,

\chi_{S(\tau)} = \chi_{S(0)} \qquad\text{and}\qquad \operatorname{Tr}\big(S(\tau)^{2k+1}\big) = 0 \ \ (k \in \mathbb N),

where $\chi$ is the characteristic polynomial: "the eigenvalues are constants of motion" (after Eq. 51) together with Eq. (48).

The milestones follow the paper's own steps, in order:

pairing $\pm\lambda$ of eigenvalues of skew-symmetric matrices, and a vanishing eigenvalue in odd size (p. 13);
conservation of $H$ under $\dot\psi = J\nabla H$ with $J$ skew (Eqs. 26–28);
identities of $\gamma_0$ and the transpose rules for (skew-)Hamiltonian matrices (Eqs. 33, 36, 54);
$\exp(H\tau)\psi_0$ solves $\dot\psi = H\psi$ (Eq. 49);
Heisenberg's equation $\dot S = [H,S]$ for second moments (Eq. 42);
the Lax invariants $\operatorname{Tr}(S^k)$ (Eq. 47) and tracelessness of odd powers (Eq. 48);
symplecticity of $\exp(H\tau)$ and $S(\tau) = M(\tau)S(0)M(-\tau)$ (Eqs. 50–51);
the dimension counts $n(2n+1)$ and $n(2n-1)$ (Eqs. 55–56) and the (anti-)commutator table (Eq. 57);
the matrix Euler formulas for the real Pauli matrices (Eq. 66).

Significance

The result itself. Each statement is classical linear algebra or linear ODE theory; the paper uses them to argue that Heisenberg's equation and the spectral description of observables arise from second moments of a classical Hamiltonian ensemble. A checked version separates what is a theorem from what is interpretation, and pins down the hypotheses (for example, that only symmetry of $A$ is needed for Eq. 48, not positive definiteness).

Formalizing it. None of these statements is new mathematics; the work is to formalize them in the paper's notation ( $\gamma_0 = \mathbf 1_n\otimes\eta_0$ , entrywise matrix derivatives, the matrix exponential) so that they can be reused for later parts of the paper, such as the real Dirac algebra of Sec. VII–VIII.

Difficulty

Most milestones are short calculations. The two steps needing real infrastructure are (i) the uniqueness of solutions of the linear matrix ODE $\dot S = [H,S]$ , needed to identify $S(\tau)$ with $\exp(H\tau)S(0)\exp(-H\tau)$ , and (ii) the dimension counts, which require an explicit basis or an isomorphism with symmetric/skew-symmetric matrices. Going through the Lax invariants alone gives only the traces of powers of $S$ , and recovering the characteristic polynomial from them needs Newton's identities; the similarity form of Eq. (51) gives the conservation of the characteristic polynomial directly.

Formalization scope

Everything is over $\mathbb R$ . Matrices are indexed by pairs $(i,b)$ , $i<n$ , $b\in\{0,1\}$ , so that $\gamma_0$ is literally a Kronecker product; $n = 0$ is allowed. Time derivatives of matrix-valued functions are entrywise HasDerivAt; $\exp$ is Mathlib's power-series NormedSpace.exp. A Hamiltonian matrix is $\gamma_0A$ with $A$ symmetric (no definiteness); $\Sigma$ is any symmetric solution of Eq. (40) — positivity is not assumed because it is not used. Eigenvalues of real skew-symmetric matrices are taken over $\mathbb C$ . "Number of linearly independent elements" is the dimension of the real span. No statement is vacuous: all hypotheses are satisfied, for example, by $H = \gamma_0$ and $\Sigma \equiv \mathbf 1$ .

All statements share the definition file UnQM_phase_space and the namespace UnQuantumMechanics.

Selected references

C. Baumgarten, How to (Un-) Quantum Mechanics, arXiv:1810.06981v2 [physics.gen-ph], 2025. https://arxiv.org/abs/1810.06981
P. D. Lax, Integrals of nonlinear equations of evolution and solitary waves, Comm. Pure Appl. Math. 21 (1968), 467–490. https://doi.org/10.1002/cpa.3160210503

18 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Davidson–Nardi–Nir 2008 (Leptogenesis), Eq. (5.10): upper bound on the flavoured CP asymmetry in N1 decaysResearch Paper

Motivation

Leptogenesis is a class of scenarios in which the baryon asymmetry of the Universe is produced from a lepton asymmetry generated in the out-of-equilibrium decays of heavy singlet neutrinos $N_k$ , which also give the light neutrinos their small masses through the type I seesaw (Fukugita–Yanagida 1986). The review of Davidson, Nardi and Nir (Phys. Rep. 466 (2008) 105) collects the standard results of the field. One of its central quantitative facts is an upper bound on the CP asymmetry in the decays of the lightest singlet $N_1$ , in terms of $M_1$ and the light-neutrino masses. This bound is the origin of the familiar lower bound $M_1\gtrsim10^9\,$ GeV for thermal leptogenesis with hierarchical singlets (Eq. (5.12) of the review).

Timeline. Casas and Ibarra introduced the orthogonal-matrix parametrization of the seesaw in 2001 (hep-ph/0103065). Davidson and Ibarra derived the bound $|\varepsilon|\le 3M_1(m_3-m_1)/(16\pi v^2)$ on the total asymmetry in 2002 (hep-ph/0202239); Hamaguchi, Murayama and Yanagida gave a related bound (hep-ph/0109030). Once flavour effects were recognised (around 2006), attention moved to the flavoured asymmetries $\varepsilon_{\alpha\alpha}$ , whose bound (Eq. (5.10) of the review) is the goal of this mission.

Setting

There are three lepton flavours $\alpha$ and three singlets $N_k$ with Majorana masses $M_k>0$ . We work in the mass basis of the charged leptons and of the $N_k$ . The Yukawa matrix $\lambda$ is an arbitrary complex $3\times3$ matrix, and $v=v_u>0$ is the Higgs vev. The light-neutrino mass matrix (Eq. (2.5)) is

[m]_{\alpha\beta}=\sum_k\lambda_{\alpha k}M_k^{-1}\lambda_{\beta k}v^2 ,

a complex symmetric matrix. It is diagonalized as $m=U^*D_mU^\dagger$ with $U$ unitary and $D_m=\operatorname{diag}(m_1,m_2,m_3)$ , $m_i\ge0$ (Eq. (2.6)). The largest and smallest light masses are $m_{\max}$ and $m_{\min}$ . The Casas–Ibarra matrix is $R=D_m^{-1/2}U^T\lambda D_M^{-1/2}v$ (Eq. (2.11)).

At tree level $N_1$ decays into $\phi\ell_\alpha$ and $\bar\phi\bar\ell_\alpha$ with partial rate $\Gamma_{\alpha\alpha}=|\lambda_{\alpha1}|^2M_1/(8\pi)$ and total rate $\Gamma_D=[\lambda^\dagger\lambda]_{11}M_1/(8\pi)$ (Eq. (4.5)). So the branching fractions satisfy $B_{\phi\ell_\alpha}+B_{\bar\phi\bar\ell_\alpha}=\Gamma_{\alpha\alpha}/\Gamma_D$ . For hierarchical singlets the flavoured CP asymmetry is (Eq. (5.9))

\varepsilon_{\alpha\alpha}=\frac{3M_1}{16\pi v^2[\lambda^\dagger\lambda]_{11}}\operatorname{Im}\{[\lambda]_{\alpha1}[m^*\lambda]_{\alpha1}\}.

Formalization targets

Goal — Eq. (5.10)

|\varepsilon_{\alpha\alpha}|\le\frac{3M_1m_{\max}}{16\pi v^2}\sqrt{B_{\phi\ell_\alpha}+B_{\bar\phi\bar\ell_\alpha}}\qquad\text{for every flavour }\alpha.

Milestones

Eq. (2.6): the matrix $m$ admits a diagonalization $m=U^*D_mU^\dagger$ with $U$ unitary and $m_i\ge0$ .
Eq. (2.11): for $m_i>0$ , $R$ is complex orthogonal, $R^TR=RR^T=1$ .
Sec. 5.2: $|m\cdot x^*|\le m_{\max}|x|$ for all $x\in\mathbb C^3$ .
Sec. 5.2 / Eq. (5.17): the total asymmetry bound $|\sum_\alpha\varepsilon_{\alpha\alpha}|\le 3M_1(m_{\max}-m_{\min})/(16\pi v^2)$ .

Significance

Eq. (5.10) is the input to the lower bounds on $M_1$ and on the reheat temperature for hierarchical thermal leptogenesis (Eq. (5.12), Sec. 9.4.3), and it shows that flavoured asymmetries are not suppressed for degenerate light neutrinos, unlike the total one (Eq. (5.17)). These are established results. The work here is to formalize them: to state the seesaw quantities precisely and machine-check the linear-algebra steps (Takagi factorization, complex orthogonality, operator-norm bounds) that the physics literature takes for granted. To the captain's knowledge none of these statements has a machine-checked proof.

Difficulty

The goal reduces to an operator-norm estimate for the complex symmetric matrix $m$ . That estimate needs the diagonalization $m=U^*D_mU^\dagger$ , which is a Takagi (Autonne–Takagi) factorization, not a unitary eigen-decomposition: $m$ is symmetric, not Hermitian. The obvious move, applying the spectral theorem to $m$ , fails because $m$ is in general not normal. The milestone-1 existence statement therefore needs its own argument, for example through the Hermitian matrix $m^\dagger m$ . The total-asymmetry bound (milestone 4) needs a finer argument than the triangle inequality to produce the difference $m_{\max}-m_{\min}$ rather than $m_{\max}$ .

Formalization scope

Everything is $3\times3$ over $\mathbb C$ with index set $\{0,1,2\}$ (Fin 3); the singlet " $N_1$ " is index $0$ .
$m_{\max}$ and $m_{\min}$ are ⨆ i, masses i and ⨅ i, masses i over the three diagonal entries. No ordering of the $m_i$ is imposed.
The diagonalization is a hypothesis IsLightMassDiagonalization m U masses (unitary $U$ , $m_i\ge0$ , $m=\overline U\,\mathrm{diag}(m_i)\,U^\dagger$ ). It is always satisfiable by milestone 1, so it is not vacuous.
$\varepsilon_{\alpha\alpha}$ is the explicit hierarchical-limit expression (5.9), with $[\lambda^\dagger\lambda]_{11}$ written as $\sum_\beta|\lambda_{\beta1}|^2$ . The physical approximation $M_{2,3}\gg M_1$ is built into this formula and is not a hypothesis. The branching sum is the tree-level ratio $\Gamma_{\alpha\alpha}/\Gamma_D$ .
Division by zero returns $0$ in Lean. This only matters when the first column of $\lambda$ vanishes, where both sides of the goal are $0$ .
Needed infrastructure: Takagi factorization of complex symmetric matrices (reusable beyond this mission), and elementary Euclidean-norm estimates on $\mathbb C^3$ .

Selected references

S. Davidson, E. Nardi, Y. Nir, Leptogenesis, Physics Reports 466 (2008) 105–177. https://doi.org/10.1016/j.physrep.2008.06.002 · https://arxiv.org/abs/0802.2962
J. A. Casas, A. Ibarra, Oscillating neutrinos and μ → e γ, Nucl. Phys. B 618 (2001) 171. https://arxiv.org/abs/hep-ph/0103065
S. Davidson, A. Ibarra, A lower bound on the right-handed neutrino mass from leptogenesis, Phys. Lett. B 535 (2002) 25. https://arxiv.org/abs/hep-ph/0202239
M. Fukugita, T. Yanagida, Baryogenesis without grand unification, Phys. Lett. B 174 (1986) 45. https://doi.org/10.1016/0370-2693(86)91126-3

6 thms2 active usersReviewed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Generalising the Scattered Property of Subspaces 5: For h ≥ 2, Two h-Scattered Linear Sets Are PΓL(r, qⁿ)-Equivalent iff Their Subspaces Are ΓL(r, qⁿ)-EquivalentResearch Paper

Motivation

Linear sets are point sets of a finite projective space defined by a subspace over a subfield. They appear throughout finite geometry, for instance in the study of semifields and, through the correspondence studied by Sheekey and Van de Voorde (arXiv:1806.05929), maximum rank distance (MRD) codes; see Polverino's survey (doi:10.1016/j.disc.2009.04.007). In these applications one needs to decide when two linear sets are the same up to a collineation, which can be difficult (Csajbók–Zanella, arXiv:1501.03441; Csajbók–Marino–Polverino, arXiv:1607.06962). The natural candidate answer, "when their defining subspaces are in the same orbit of the semilinear group", is only a sufficient condition: on the projective line $\mathrm{PG}(1,q^n)$ there are maximum scattered subspaces in different $\Gamma\mathrm L(2,q^n)$ -orbits defining equivalent linear sets (the two papers just cited).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590, Combinatorica 41 (2021)) introduced $h$ -scattered subspaces, a generalisation of scattered subspaces, and showed in their §4 that for $h \ge 2$ the sufficient condition is also necessary. This mission formalizes that result, Theorem 4.5.

Setting

Let $\mathbb F_q \subseteq \mathbb F_{q^n}$ be finite fields and let $V$ be an $r$ -dimensional vector space over $\mathbb F_{q^n}$ ; it is also a vector space over $\mathbb F_q$ . The projective space $\mathrm{PG}(V,\mathbb F_{q^n}) = \mathrm{PG}(r-1,q^n)$ has as points the one-dimensional $\mathbb F_{q^n}$ -subspaces $\langle u\rangle_{\mathbb F_{q^n}}$ , $u \ne 0$ .

For an $\mathbb F_q$ -subspace $U$ of $V$ , the $\mathbb F_q$ -linear set of $U$ is

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

of rank $\dim_{\mathbb F_q} U$ .

For $0 < h \le r-1$ , the subspace $U$ is $h$ -scattered (Definition 1.1) 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$ . The linear set $L_U$ of an $h$ -scattered $U$ is called $h$ -scattered (Definition 4.1); for $h = 2$ it is scattered with respect to lines.

The group $\Gamma\mathrm L(r,q^n)$ consists of the bijective additive maps $f$ of $V$ that are semilinear: $f(av) = a^\sigma f(v)$ for some field automorphism $\sigma$ of $\mathbb F_{q^n}$ . Each $f$ induces a collineation $\varphi_f$ of $\mathrm{PG}(V,\mathbb F_{q^n})$ , $\langle u\rangle \mapsto \langle f(u)\rangle$ , and these collineations form $\mathrm P\Gamma\mathrm L(r,q^n)$ . Two linear sets are $\mathrm P\Gamma\mathrm L$ -equivalent if $\varphi_f(L_U) = L_W$ for some $f$ ; two subspaces are $\Gamma\mathrm L$ -equivalent if $f(U) = W$ for some $f$ .

Formalization targets

Goal: Theorem 4.5 (p. 14)

For $h \ge 2$ and $h$ -scattered $\mathbb F_q$ -subspaces $U$ , $W$ of $V(r,q^n)$ ,

L_U \sim_{\mathrm P\Gamma\mathrm L(r,q^n)} L_W \iff U \sim_{\Gamma\mathrm L(r,q^n)} W .

Milestones (in the order of the proof)

Proposition 2.1 (p. 3): an $h$ -scattered subspace is $i$ -scattered for every $0 < i < h$ .
Proposition 4.2 (p. 13, quoted from Bonoli–Polverino [5]): on a projective line $\mathrm{PG}(1,q^n)$ , (1) a linear set with $q+1$ points has rank $2$ ; (2) two subspaces defining the same linear set of size $q+1$ and sharing a nonzero vector coincide.
Proposition 4.3 (p. 13): if $U$ is $2$ -scattered and $L_W = L_U$ , then $\dim_{\mathbb F_q} W = \dim_{\mathbb F_q} U$ .
Lemma 4.4 (p. 13): if $U$ is $2$ -scattered and $L_U = L_W$ , then $U = \lambda W$ for some $\lambda\in\mathbb F_{q^n}^*$ .

Significance

The result. Theorem 4.5 says that, for $h\ge2$ , an $h$ -scattered linear set remembers its defining subspace up to a scalar and up to the semilinear group. The equivalence problem for such linear sets, a geometric question about point sets, becomes the equivalence problem for subspaces, which is algebraic and can be attacked with linearized polynomials. Through the correspondence of Sheekey and Van de Voorde between maximum $(r-1)$ -scattered subspaces and MRD codes, the paper derives from it (Theorem 4.10, not part of this mission) that two $\mathbb F_q$ -linear MRD codes with minimum distance $n-r+1$ , $r>2$ , and left idealiser isomorphic to $\mathbb F_{q^n}$ are equivalent if and only if their associated linear sets in $\mathrm{PG}(r-1,q^n)$ are $\mathrm P\Gamma\mathrm L$ -equivalent. Lemma 4.4 and Proposition 4.3 are of independent use: they say that the rank and, up to scalars, the subspace of any linear set scattered with respect to lines are invariants of the point set.

The formalization. The theorem is proved in the paper; no part of it, nor any statement about linear sets over a field extension, is machine-checked in Mathlib. The mission produces a formal model of linear sets, of the semilinear group and of its induced collineations that later finite-geometry missions can reuse, together with formal proofs of the four milestones. Proposition 4.2 is quoted from [5] without proof in the paper, so formalizing it means formalizing Bonoli and Polverino's argument.

Difficulty

The "if" direction is a direct computation, $L_{U^f} = L_U^{\varphi_f}$ . The obvious approach to the converse, reconstructing $U$ from $L_U$ point by point, fails because a point $\langle u\rangle$ of $L_U$ determines $U\cap\langle u\rangle$ only up to a scalar of $\mathbb F_{q^n}^*$ , and these scalars can a priori differ from point to point. Without the condition $h \ge 2$ they really do differ: for $h = 1$ the theorem is false. The step that needs $h\ge2$ is the rigidity of the intersections of $U$ with two-dimensional $\mathbb F_{q^n}$ -subspaces, which is where the quoted result on linear sets of size $q+1$ on a projective line enters. Proposition 4.2 itself is a counting statement about point weights on $\mathrm{PG}(1,q^n)$ and is not available in any library.

Formalization scope

$\mathbb F_q$ and $\mathbb F_{q^n}$ are arbitrary finite fields F, K with [Algebra F K]; $q$ is Fintype.card F. $V$ is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]), and $r$ is Module.finrank K V.
IsHScattered F K h U includes the range $0 < h < r$ and the spanning condition $\langle U\rangle_{\mathbb F_{q^n}} = V$ , as in Definition 1.1. With $h\ge2$ this forces $r\ge3$ .
A point is the K-submodule K ∙ u; linearSet F K U is a Set (Submodule K V) and $|L_U|$ is its Set.ncard.
$\Gamma\mathrm L$ is the set of f : V ≃+ V for which some σ : K ≃+* K gives f (a • v) = σ a • f v. The collineation $\varphi_f$ sends a subspace $P$ to Submodule.span K (f '' P). The image $U^f$ is the set f '' U, and $\lambda W$ is (λ • ·) '' W with $\lambda\ne0$ .
Two trivializing readings are excluded. Restricting to linear maps (GL, PGL) would prove a different, weaker statement; taking $\mathrm{P}\Gamma\mathrm{L}$ -equivalence to mean "some bijection of points maps $L_U$ to $L_W$ " would make the "only if" direction false. Both equivalences quantify over the full semilinear group, and the collineation is the one induced by the same $f$ .
Proposition 4.2 is a result the paper numbers but quotes from [5] (Bonoli–Polverino, $\mathbb F_q$ -linear blocking sets in $\mathrm{PG}(2,q^4)$ ). It is a milestone with its own proof obligation and is not assumed. The two parts are separate items.
Proposition 2.1's "for any $i < h$ " is read as $0 < i < h$ , the range on which Definition 1.1 defines $i$ -scattered.

Welcome contributions: the general theory of linear sets (point weights, $|L_U| \le (q^k-1)/(q-1)$ with equality iff $U$ is scattered), the fact that a semilinear map of $V$ maps $\mathbb F_q$ -subspaces to $\mathbb F_q$ -subspaces, and the counting argument behind Proposition 4.2. These are reusable for every linear-set mission.

Selected references

B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, Combinatorica 41 (2021); arXiv:1906.10590v2 (2020). https://arxiv.org/abs/1906.10590
G. Bonoli, O. Polverino, $\mathbb F_q$ -linear blocking sets in $\mathrm{PG}(2,q^4)$ , Innov. Incidence Geom. 2 (2005), 35–56. https://doi.org/10.2140/iig.2005.2.35
B. Csajbók, G. Marino, O. Polverino, Classes and equivalence of linear sets in $\mathrm{PG}(1,q^n)$ , J. Combin. Theory Ser. A 157 (2018), 402–426. https://arxiv.org/abs/1607.06962
B. Csajbók, C. Zanella, On the equivalence of linear sets, Des. Codes Cryptogr. 81 (2016), 269–281. https://arxiv.org/abs/1501.03441
O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2009.04.007
J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://arxiv.org/abs/1806.05929

9 thms2 active usersReviewed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Generalising the Scattered Property of Subspaces 4: For n ≥ h + 3, the Delsarte Dual of a Maximum h-Scattered Subspace of Dimension rn/(h + 1) Is Maximum (n − h − 2)-ScatteredResearch Paper

Motivation

Scattered subspaces are a central object of finite geometry. An $\mathbb F_q$ -subspace $U$ of an $\mathbb F_{q^n}$ -vector space is scattered when every one-dimensional $\mathbb F_{q^n}$ -subspace meets it in $\mathbb F_q$ -dimension at most one. They give the largest scattered linear sets of projective spaces, and through them constructions of two-intersection sets, two-weight codes, strongly regular graphs and, most prominently, maximum rank distance (MRD) codes. Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2) generalise the notion to $h$ -scattered subspaces, which meet every $h$ -dimensional $\mathbb F_{q^n}$ -subspace in $\mathbb F_q$ -dimension at most $h$ , prove the dimension bound $rn/(h+1)$ , and ask when it is attained.

When $h+1$ divides $r$ , direct sums of known examples reach the bound (Theorem 2.6 of the paper). For other values of $r$ the paper introduces a duality, the Delsarte dual, which turns a maximum $h$ -scattered subspace of one space into a maximum $(n-h-2)$ -scattered subspace of a space of another dimension. The name comes from Delsarte's duality on MRD codes, which the paper shows corresponds to it (Theorem 4.12). This mission is about that duality: Theorem 3.3 of the paper.

Setting

Let $\mathbb F_q\subseteq\mathbb F_{q^n}$ be finite fields, with $n=\dim_{\mathbb F_q}\mathbb F_{q^n}$ . Write $V(r,q^n)$ for an $r$ -dimensional $\mathbb F_{q^n}$ -vector space; it is also an $\mathbb F_q$ -space of dimension $rn$ .

Definition 1.1. For $0<h\le r-1$ , an $\mathbb F_q$ -subspace $U$ of $V=V(r,q^n)$ 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$ . It is maximum $h$ -scattered if no $h$ -scattered subspace of $V$ has larger $\mathbb F_q$ -dimension. The paper's Theorem 2.3 shows that an $h$ -scattered subspace either has dimension $r$ and defines a subgeometry, or has dimension at most $rn/(h+1)$ .

The setting of §3. Let $\mathbb V$ be a $k$ -dimensional $\mathbb F_{q^n}$ -vector space, written as a direct sum $\mathbb V=\Lambda\oplus\Gamma$ of $\mathbb F_{q^n}$ -subspaces with $\dim\Lambda=r$ and $\dim\Gamma=k-r$ . Let $W$ be a $k$ -dimensional $\mathbb F_q$ -subspace of $\mathbb V$ with $\langle W\rangle_{\mathbb F_{q^n}}=\mathbb V$ and $W\cap\Gamma=\{0\}$ , and put

U=\langle W,\Gamma\rangle_{\mathbb F_q}\cap\Lambda ,

an $\mathbb F_q$ -subspace of $\Lambda$ . Every $k$ -dimensional $\mathbb F_q$ -subspace of $\Lambda$ with $k>r$ arises in this way (Lunardon and Polverino, cited as [21, Theorems 1, 2] in the paper). Let $\beta:\mathbb V\times\mathbb V\to\mathbb F_{q^n}$ be a non-degenerate reflexive sesquilinear form with companion automorphism $\sigma$ (linear in the first argument, $\beta(v,aw)=a^\sigma\beta(v,w)$ ) which takes values in $\mathbb F_q$ on $W\times W$ ; equivalently, $\beta$ extends a non-degenerate reflexive form $\beta':W\times W\to\mathbb F_q$ . Write $\Gamma^\perp=\{v:\beta(v,g)=0\ \forall g\in\Gamma\}$ , an $r$ -dimensional subspace. The Delsarte dual of $U$ (Definition 3.2) is the $\mathbb F_q$ -subspace

\bar U=W+\Gamma^\perp=\{w+\Gamma^\perp:w\in W\}\subseteq\mathbb V/\Gamma^\perp ,

a subspace of a $(k-r)$ -dimensional $\mathbb F_{q^n}$ -space.

Formalization targets

Goal: Theorem 3.3

Suppose $U$ is a maximum $h$ -scattered $\mathbb F_q$ -subspace of $\Lambda=V(r,q^n)$ of dimension $k=rn/(h+1)$ , and $n\ge h+3$ . Then

\bar U \text{ is a maximum } (n-h-2)\text{-scattered } \mathbb F_q\text{-subspace of } \mathbb V/\Gamma^\perp=V\!\left(\tfrac{rn}{h+1}-r,\ q^n\right),\qquad \dim_{\mathbb F_q}\bar U=k .

The statement holds for every admissible choice of the embedding and of $\beta$ .

Milestones

Theorem 2.7 (p. 8): a maximum $h$ -scattered subspace of dimension $rn/(h+1)$ meets every hyperplane $H$ in dimension between $rn/(h+1)-n$ and $rn/(h+1)-n+h$ .
The identity $(S^*)^\perp=(S^{\perp'})^*$ (p. 9) for $\mathbb F_q$ -subspaces $S$ of $W$ , where $S^*=\langle S\rangle_{\mathbb F_{q^n}}$ and $\perp'$ is orthogonality for $\beta'$ .
Proposition 3.1 (p. 9): if $k>r$ and every hyperplane $M$ of $\Lambda$ satisfies $\dim_{\mathbb F_q}(M\cap U)<k-1$ (condition $(\diamond)$ ), then $\dim_{\mathbb F_q}\bar U=k$ .
Theorem 2.3 (p. 4): the dimension bound $rn/(h+1)$ for $h$ -scattered subspaces.

Significance

The result. Theorem 3.3 converts a maximum $h$ -scattered subspace of $V(r,q^n)$ of dimension $rn/(h+1)$ into a maximum $(n-h-2)$ -scattered subspace of $V(rn/(h+1)-r,q^n)$ . For $h=r-1$ it was known through MRD codes; the paper proves it for every $h$ . Its consequences in the paper are Corollaries 3.4 and 3.5 and Theorem 3.6: when $n\ge4$ is even and $r\ge3$ is odd, maximum $(n-3)$ -scattered subspaces of $V(r(n-2)/2,q^n)$ exist which the direct sum construction of Theorem 2.6 cannot produce, because $n-2$ does not divide $r(n-2)/2$ . Theorem 3.3 is also the geometric counterpart of Delsarte duality of MRD codes (Theorem 4.12 of the paper).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formalization would provide a reusable treatment of sesquilinear forms whose restriction to an $\mathbb F_q$ -form is controlled, of orthogonal complements across the field extension $\mathbb F_q\subseteq\mathbb F_{q^n}$ , and of the passage between $\Lambda$ , $\mathbb V/\Gamma$ and $\mathbb V/\Gamma^\perp$ . Theorems 2.3 and 2.7 are also the goals of companion missions in this series; here they enter as milestones.

Difficulty

The definition of $\bar U$ is easy; the content is in two dimension statements. First, $W+\Gamma^\perp$ must not collapse: $W\cap\Gamma^\perp=\{0\}$ is not automatic and depends on the hyperplane condition $(\diamond)$ on $U$ , which in turn needs the upper bound of Theorem 2.7, whose proof in the paper is a long counting argument with Gaussian binomials (Section 5). Second, the scattered property must be transported through the duality: a large intersection of $\bar U$ with an $(n-h-2)$ -dimensional subspace of $\mathbb V/\Gamma^\perp$ must be converted into a large intersection of $U$ with a hyperplane of $\Lambda$ . This conversion runs through three different spaces and two different orthogonalities, $\perp$ over $\mathbb F_{q^n}$ and $\perp'$ over $\mathbb F_q$ , and the identification $(S^*)^\perp=(S^{\perp'})^*$ between them requires that $W$ have an $\mathbb F_q$ -basis which is an $\mathbb F_{q^n}$ -basis of $\mathbb V$ . Maximality is a further step that uses the bound of Theorem 2.3 in $\mathbb V/\Gamma^\perp$ .

Formalization scope

$\mathbb F_q$ and $\mathbb F_{q^n}$ are finite fields F, K with Algebra F K; $\mathbb V$ is a finite-dimensional K-module with a compatible F-structure (IsScalarTower F K 𝕍). The setting of §3 is a structure DelsarteSetting F K 𝕍 holding $\Lambda,\Gamma$ (complementary), $W$ (with $\dim_{\mathbb F_q}W=\dim_{\mathbb F_{q^n}}\mathbb V$ , spanning, $W\cap\Gamma=0$ ), $\sigma:\mathbb F_{q^n}\simeq\mathbb F_{q^n}$ and $\beta:\mathbb V\to_{\mathbb F_{q^n}}\mathbb V\to_{\sigma}\mathbb F_{q^n}$ with non-degeneracy, reflexivity and $\beta(W,W)\subseteq\mathbb F_q$ . The embedding of $\Lambda$ into $\mathbb V$ is data, not a theorem; its existence is cited by the paper and is not an item. The paper's $\beta'$ is the restriction of $\beta$ to $W$ .

Conventions pinned:

$U$ is an F-subspace of the type ↥Λ, and "h-scattered in $\Lambda$ " is Definition 1.1 with ambient space $\Lambda$ , including $0<h<r$ and $\langle U\rangle_{\mathbb F_{q^n}}=\Lambda$ . The dual is (n − h − 2)-scattered in the quotient 𝕍 ⧸ Γ^⊥, whose dimension is $k-r$ .
Every $rn/(h+1)$ is multiplied out: $(h+1)\dim U=rn$ . Hyperplanes are subspaces with $\dim+1=\dim$ of the ambient space; $\dim<k-1$ is written $\dim+1<k$ . The only natural-number subtraction is the index $n-h-2$ , exact because $n\ge h+3$ .
The paper's $k>r$ is a hypothesis of Proposition 3.1, as on the page, and is derived (not assumed) in Theorem 3.3.

The form must be non-degenerate and $\mathbb F_q$ -valued on $W$ : with $\beta=0$ one would get $\Gamma^\perp=\mathbb V$ and a zero quotient, and without $\beta(W,W)\subseteq\mathbb F_q$ the subspace $W+\Gamma^\perp$ is not the paper's Delsarte dual; both conditions are fields of the setting and may not be dropped.

Cited inputs: none of the milestones is proved elsewhere; Theorems 2.3 and 2.7 duplicate the goals of companion missions 1 and 3 and may be closed by importing their proofs once published. Contributions welcome: the sesquilinear-form infrastructure (dimension of orthogonal complements, the extension of $\beta'$ from $W$ to $\mathbb V$ ), Proposition 3.1, and the transport argument of Theorem 3.3.

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
G. Lunardon, O. Polverino, Translation ovoids of orthogonal polar spaces, Forum Math. 16 (2004), 663–669 (the embedding used in §3).
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243 (the case h = 1 of the bound).
P. Delsarte, Bilinear forms over a finite field, with applications to coding theory, J. Combin. Theory Ser. A 25 (1978), 226–241 (Delsarte duality of rank-metric codes).

8 thms2 active usersReviewed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Generalising the Scattered Property of Subspaces 2: If h + 1 Divides r and n ≥ h + 1, Maximum h-Scattered 𝔽_q-Subspaces of V(r, qⁿ) of Dimension rn/(h + 1) ExistResearch Paper

Motivation

A scattered subspace is an $\mathbb F_q$ -subspace $U$ of an $\mathbb F_{q^n}$ -vector space $V$ that meets every one-dimensional $\mathbb F_{q^n}$ -subspace of $V$ in an $\mathbb F_q$ -subspace of dimension at most one. Scattered subspaces produce scattered linear sets in projective spaces over finite fields, and through them two-intersection sets, two-weight codes, translation caps and maximum rank distance (MRD) codes. Blokhuis and Lavrauw (Geom. Dedicata 2000) proved that a scattered subspace of $V(r,q^n)$ has dimension at most $rn/2$ , and constructions of that dimension are known whenever $rn$ is even (see Bartoli, Giulietti, Marino, Polverino 2018 and the references there).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) replace "one-dimensional" by " $h$ -dimensional". The resulting $h$ -scattered subspaces interpolate between scattered subspaces ( $h=1$ ) and subspaces meeting every hyperplane in small dimension ( $h=r-1$ ), which Sheekey and Van de Voorde (Des. Codes Cryptogr. 2020) showed to be equivalent to MRD codes with an idealiser isomorphic to $\mathbb F_{q^n}$ . For the new notion the paper proves an upper bound on the dimension (Theorem 2.3) and shows that the bound is attained when $h+1$ divides $r$ (Theorem 2.6). This mission is the attainment half.

Setting

Let $\mathbb F_q\subseteq\mathbb F_{q^n}$ be finite fields, so $n=[\mathbb F_{q^n}:\mathbb F_q]$ , and let $V=V(r,q^n)$ be an $r$ -dimensional $\mathbb F_{q^n}$ -vector space with $r\ge1$ . Every $\mathbb F_{q^n}$ -space is also an $\mathbb F_q$ -space of dimension $rn$ . For an integer $h$ with $0<h\le r-1$ , an $\mathbb F_q$ -subspace $U\le V$ is $h$ -scattered (Definition 1.1) if

$U$ spans $V$ over $\mathbb F_{q^n}$ , $\langle U\rangle_{\mathbb F_{q^n}}=V$ , and
$\dim_{\mathbb F_q}(S\cap U)\le h$ for every $h$ -dimensional $\mathbb F_{q^n}$ -subspace $S$ of $V$ .

An $h$ -scattered subspace of largest possible $\mathbb F_q$ -dimension is maximum $h$ -scattered. Theorem 2.3 of the paper says that an $h$ -scattered $U$ either has dimension $r$ and defines a subgeometry (an $\mathbb F_q$ -basis of $U$ is an $\mathbb F_{q^n}$ -basis of $V$ ), or satisfies

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

Two building blocks appear in the statements. If $V=V_1\oplus\dots\oplus V_t$ with $V_i=V(r_i,q^n)$ and $U_i\le V_i$ are $\mathbb F_q$ -subspaces, then $U=U_1\oplus\dots\oplus U_t$ is the direct sum of the $U_i$ . For $r\le n$ the Gabidulin-type subspace of $\mathbb F_{q^n}^{\,r}$ is

G_r=\{(x,x^{q},x^{q^2},\dots,x^{q^{r-1}}) : x\in\mathbb F_{q^n}\},

the image of an $\mathbb F_q$ -linear map, since $x\mapsto x^{q^j}$ fixes $\mathbb F_q$ .

Formalization targets

Goal: Theorem 2.6 (p. 7)

If $h\ge1$ , $h+1$ divides $r$ and $n\ge h+1$ , then $V(r,q^n)$ contains an $\mathbb F_q$ -subspace $U$ that is maximum $h$ -scattered and satisfies

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

Milestones, in the order the paper uses them

Proposition 2.1 (p. 3): for $h>1$ , every $h$ -scattered subspace is $i$ -scattered for all $0<i<h$ .
Theorem 2.3 (p. 4): the dichotomy above, subgeometry or bound (1).
Theorem 2.4 (p. 6): if $U_i$ is $h_i$ -scattered in $V_i$ , then $U_1\oplus\dots\oplus U_t$ is $\min_i h_i$ -scattered in $V_1\oplus\dots\oplus V_t$ .
Theorem 2.4, second sentence (p. 6): if every $U_i$ is $h$ -scattered with $\dim_{\mathbb F_q}U_i=r_in/(h+1)$ , then the direct sum is $h$ -scattered of dimension $rn/(h+1)$ .
Example 2.5 (p. 7): for $2\le r\le n$ , $G_r$ is maximum $(r-1)$ -scattered of dimension $n$ .

Significance

Together with Theorem 2.3, the goal settles the largest dimension of an $h$ -scattered subspace of $V(r,q^n)$ whenever $h+1\mid r$ and $n\ge h+1$ : it is exactly $rn/(h+1)$ . The subspaces it produces are the input of the paper's Delsarte duality (Theorem 3.3), which turns maximum $h$ -scattered subspaces of $V(r,q^n)$ reaching bound (1) into maximum $(n-h-2)$ -scattered subspaces of $V(rn/(h+1)-r,q^n)$ and so gives constructions also when $h+1\nmid r$ . The direct-sum theorem is also of independent use: it extends the direct-sum construction for scattered linear sets of Bartoli, Giulietti, Marino and Polverino to every $h$ , and Example 2.5 gives the subspace counterpart of Gabidulin codes.

All results in this mission are proved in the paper. To our knowledge none of them has a machine-checked proof; no formal library contains scattered subspaces, linear sets or Gabidulin-type subspaces. The remaining work is formalizing the paper's arguments: the counting of roots of linearized polynomials behind Example 2.5, the Grassmann-formula and quotient-space argument of Theorem 2.4, and the bound (1) of Theorem 2.3, which the companion mission on the dimension bound states as its goal.

Difficulty

The construction itself is short; the work lies in the three ingredients. The obvious approach to Theorem 2.4 fails: an $h$ -dimensional $\mathbb F_{q^n}$ -subspace $W$ of $V_1\oplus V_2$ need not be the sum of its intersections with $V_1$ and $V_2$ , so the intersection $W\cap U$ cannot be bounded summand by summand. Example 2.5 needs that a nonzero $q$ -polynomial $\sum_{j<r}a_jx^{q^j}$ has at most $q^{r-1}$ roots in $\mathbb F_{q^n}$ , and the root set is an $\mathbb F_q$ -subspace. Maximality is not a property of a single subspace: it quantifies over every $h$ -scattered subspace of $V$ and so needs the full upper bound of Theorem 2.3, including the case $n<h+1$ handled there by Proposition 2.1.

Formalization scope

$\mathbb F_q$ is a finite field F, $\mathbb F_{q^n}$ a finite field K with Algebra F K, so $q=$ Fintype.card F and $n=$ Module.finrank F K. $V$ is a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V), and $r=$ Module.finrank K V. An $\mathbb F_q$ -subspace is a Submodule F V; its intersection with an $\mathbb F_{q^n}$ -subspace S is S.restrictScalars F ⊓ U.

Conventions the statements commit to:

The range $0<h<r$ and the spanning condition are part of IsHScattered; without the range every spanning subspace would be $h$ -scattered for $h\ge r$ .
Every quotient $rn/(h+1)$ is multiplied out, as $(h+1)\dim_{\mathbb F_q}U=rn$ or $\le rn$ ; no natural-number division is used.
The direct sum in Theorem 2.4 is external: $V=\prod_{i<t}V_i$ ((i : Fin t) → V i) and $U=$ Submodule.pi Set.univ U. The minimum $h=\min_i h_i$ is given by $h\le h_i$ for all $i$ and $h=h_i$ for some $i$ . The second part of Theorem 2.4 assumes $t\ge1$ .
Example 2.5 is stated on Fin r → K, with $G_r$ the range of the F-linear map $x\mapsto(x^{q^j})_{j<r}$ , and assumes $r\ge2$ so that $(r-1)$ -scattered is within Definition 1.1's range.
The goal assumes $r\ge1$ : $h+1$ divides $0$ , but the zero space has no $h$ -scattered subspace. The upper end $h<r$ follows from $h+1\mid r$ .
"Defines a subgeometry" in Theorem 2.3 is: some subset of $U$ spans $U$ over $\mathbb F_q$ and is an $\mathbb F_{q^n}$ -basis of $V$ .

The goal is not satisfied by a small subspace: both the dimension equality $(h+1)\dim_{\mathbb F_q}U=rn$ and maximality among all $h$ -scattered subspaces of $V$ are part of its conclusion.

Results the paper cites without a number (the Blokhuis–Lavrauw bound for $h=1$ , the direct-sum theorem for scattered linear sets) are not items. Theorem 2.3 is restated here because the maximality in Theorem 2.6 rests on it; it duplicates the goal of the companion mission. Useful infrastructure beyond this mission: roots of linearized polynomials over finite fields, dimension formulas for subspaces under restriction of scalars, and direct sums of $h$ -scattered subspaces. Contributions on any milestone are welcome, and the goal can be closed from the milestones alone.

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.10590, https://doi.org/10.1007/s00493-020-4347-y
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, Combinatorica 38 (2018), 255–278. https://doi.org/10.1007/s00493-016-3531-6
J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets, and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://doi.org/10.1007/s10623-019-00703-z

10 thms2 active usersReviewed

Completed

Algebra Combinatorics Discrete Geometry·Captain: mikedeng1

Generalising the Scattered Property of Subspaces 3: A Maximum h-Scattered Subspace of Dimension rn/(h + 1) Meets Every Hyperplane in Dimension Between rn/(h + 1) − n and rn/(h + 1) − n + hResearch Paper

Motivation

Scattered subspaces are a central object of finite geometry. An $\mathbb F_q$ -subspace $U$ of an $r$ -dimensional vector space over $\mathbb F_{q^n}$ defines an $\mathbb F_q$ -linear set of the projective space $\mathrm{PG}(r-1,q^n)$ , and when $U$ is scattered this linear set has the largest possible number of points for its rank. Maximum scattered subspaces give rise to maximum rank distance (MRD) codes, to translation caps, and to two-intersection sets and the associated two-weight codes and strongly regular graphs (Polverino 2010; Sheekey–Van de Voorde 2020).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) generalised the notion to $h$ -scattered subspaces, which meet every $h$ -dimensional $\mathbb F_{q^n}$ -subspace in dimension at most $h$ , and proved that such a subspace has dimension at most $rn/(h+1)$ unless it defines a subgeometry. This mission concerns the extremal case: subspaces attaining $rn/(h+1)$ , and the way they meet hyperplanes.

Timeline.

2000: Blokhuis and Lavrauw (Geom. Dedicata 81, Theorem 4.2) prove the case $h=1$ : a scattered subspace of dimension $rn/2$ meets each hyperplane in dimension $rn/2-n$ or $rn/2-n+1$ , and they count the hyperplanes of each kind.
2020: Csajbók, Marino, Polverino and Zullo prove the general statement (Theorem 2.7) by a double count and $q$ -series identities, and use it to build maximum $h$ -scattered subspaces by Delsarte duality.
Later work by Zini and Zullo (Scattered subspaces and related codes, reference [29] of the paper) determines the number of hyperplanes of each intersection dimension for every $h$ ; the case $h=2$ is in Napolitano–Zullo.

Setting

Let $\mathbb F_q\subseteq\mathbb F_{q^n}$ be finite fields, $n = [\mathbb F_{q^n}:\mathbb F_q]$ , and let $V = V(r,q^n)$ be an $r$ -dimensional vector space over $\mathbb F_{q^n}$ , viewed also as an $rn$ -dimensional vector space over $\mathbb F_q$ . A hyperplane of $V$ is an $(r-1)$ -dimensional $\mathbb F_{q^n}$ -subspace.

Fix an integer $h$ with $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$ satisfies $\dim_{\mathbb F_q}(S\cap U)\le h$ . It is maximum $h$ -scattered if no $h$ -scattered subspace of $V$ has larger $\mathbb F_q$ -dimension.

Put $s=h+1$ and suppose $s\mid rn$ . For an $\mathbb F_q$ -subspace $U$ of dimension $rn/s$ , let $h_i$ be the number of hyperplanes $W$ with $\dim_{\mathbb F_q}(W\cap U)=i$ . The proof works with the Gaussian binomial coefficients $\left[{n\atop k}\right]_q$ , the $q$ -Pochhammer symbols $(a;q)_k=(1-a)(1-aq)\cdots(1-aq^{k-1})$ , the elementary symmetric values $\sigma_{k,l}$ of $1,q,\dots,q^k$ , and the sums

\alpha_k=\sum_i h_i(q^n-1)q^{ki},\qquad \beta_k=\sum_i h_i(q^n-1)\prod_{j=0}^{k-1}(q^i-q^j),

A=\sum_i h_i(q^n-1)\prod_{l=0}^{s-1}\bigl(q^i-q^{\,n(r-s)/s+l}\bigr).

Formalization targets

Goal: Theorem 2.7

If $U$ is a maximum $h$ -scattered $\mathbb F_q$ -subspace of $V(r,q^n)$ of dimension $rn/(h+1)$ , then for every hyperplane $W$ of $V$

\frac{rn}{h+1}-n\;\le\;\dim_{\mathbb F_q}(U\cap W)\;\le\;\frac{rn}{h+1}-n+h.

Milestones, in the order of the proof (§5, pp. 20–24)

$h_i=0$ for $i<rn/s-n$ (the lower bound), and (23): $\sum_i h_i(q^n-1)=q^{rn}-1$ .
Lemma 5.7: for $0\le k\le s-1$ ,

\sum_i h_i(q^n-1)\prod_{j=0}^{k}(q^i-q^j)=\prod_{j=0}^{k}(q^{rn/s}-q^j)\,(q^{(r-k-1)n}-1).

The $q$ -series tools: Lemma 5.5 ( $\sigma_{k,l}=q^{l(l-1)/2}\left[{k+1\atop l}\right]_q$ ), Carlitz's inversion (Theorem 5.6), the $q$ -binomial theorem (Theorem 5.2) and its specialisation (Corollary 5.3).
(24): $\alpha_k=\sum_{j\le k}\left[{k\atop j}\right]_q\beta_j$ . Identity (25), which expresses $A$ through $\alpha_0,\dots,\alpha_s$ , is included as a supporting item rather than a milestone.
Propositions 5.8 and 5.9: two triple sums $a_s$ , $b_s$ both equal $q^{nr}(-1)^s(q^{-n};q)_s$ .
$A=0$ , which forces $h_i=0$ for $i>n(r-s)/s+s-1$ .

Significance

The result. Theorem 2.7 says that a maximum $h$ -scattered subspace of dimension $rn/(h+1)$ has only $h+1$ possible intersection dimensions with hyperplanes. Its linear set therefore meets hyperplanes in few sizes, which links these subspaces to sets of few intersection numbers and to codes with few weights. Inside the paper, the upper bound is the input to §3: it shows that the Delsarte dual of a maximum $h$ -scattered subspace of dimension $rn/(h+1)$ is maximum $(n-h-2)$ -scattered (Theorem 3.3). That theorem in turn gives maximum $h$ -scattered subspaces when $h+1$ does not divide $r$ .

Formalizing it. The theorem is proved in the paper, but no machine-checked version exists. Beyond the geometry, the mission produces a library of finite $q$ -series facts: Gaussian binomials as rational functions of $q$ , the $q$ -binomial theorem in both forms, Carlitz's inversion formula, and the elementary symmetric evaluation $\sigma_{k,l}$ . Some of these are proved on the platform in a different Mathlib environment, but they are not available in this one. Counting statements about subspaces over finite fields (hyperplanes through a subspace, ordered independent tuples) are also needed and are reusable.

Difficulty

The lower bound is a dimension count. The upper bound is not: the obvious approach bounds $\dim(U\cap W)$ from the scattered property alone, but the $h$ -scattered condition controls intersections with $h$ -dimensional subspaces, and hyperplanes have dimension $r-1$ , which is far larger. No pointwise argument is known; the paper determines the distribution $(h_i)$ only through its first $s+1$ moments, given by a double count, and then shows that a specific nonnegative combination of the $h_i$ vanishes. The moment identities hold only for $k\le s-1$ (Lemma 5.7 needs each $k+1\le h+1$ independent vectors of $U$ to stay independent over $\mathbb F_{q^n}$ ), and closing the argument requires exact evaluation of a triple $q$ -series with signed Gaussian binomials and quadratic exponents.

Formalization scope

$\mathbb F_q$ is a finite field F, $\mathbb F_{q^n}$ a finite field K with [Algebra F K], and $V$ a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V). We take $r=$ finrank K V, $n=$ finrank F K and $q=$ Fintype.card F.
The range $0<h<r$ and the spanning condition are part of IsHScattered.
"Dimension $rn/(h+1)$ " is the equation $(h+1)\dim_{\mathbb F_q}U = rn$ . Both bounds of Theorem 2.7 are stated with $n$ moved to the other side: $\dim U\le\dim(U\cap W)+n\le\dim U+h$ . A version written with natural-number subtraction would make the lower bound vacuous whenever $rn/(h+1)<n$ , and dropping the dimension hypothesis would make the upper bound false. Both trivialisations are ruled out.
Gaussian binomials are defined by the product formula (15) for real $q$ and vanish for $k>n$ . The $q$ -identities are stated for real $q>1$ , which covers every prime power. Carlitz's formula is stated for complex sequences.
Every fraction in an exponent is an exact quotient: $rn/s$ is passed as $m$ with $sm=nr$ , and halves $l(l-1)/2$ are binomial coefficients $\binom l2$ . Possibly negative exponents use integer powers.
The milestones of §5 carry the full $h$ -scattered hypothesis, spanning included. The printed setting of §5.2 omits spanning, but Lemma 5.7 uses Proposition 2.1, which needs it.
Cited inputs stated as milestones: Lemma 5.5 ([6]), Theorem 5.2 ([15]) and Theorem 5.6 ([7]). Identity (18) is used inside proofs and is not an item.

Proofs of any milestone, of standard counting facts for subspaces of finite vector spaces, and of the $q$ -series lemmas are welcome.

Selected references

B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, Combinatorica 41 (2021). arXiv:1906.10590v2. https://arxiv.org/abs/1906.10590v2
A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2009.04.007
J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets, and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://doi.org/10.1007/s10623-019-00703-z
G. Gasper, M. Rahman, Basic Hypergeometric Series, 2nd ed., Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511526251
L. Carlitz, Some inverse relations, Duke Math. J. 40 (1973), 893–901. https://doi.org/10.1215/S0012-7094-73-04083-0
V. Napolitano, F. Zullo, Codes with few weights arising from linear sets, arXiv:2002.07241. https://arxiv.org/abs/2002.07241
P. J. Cameron, Notes on Counting: An Introduction to Enumerative Combinatorics, Cambridge University Press, 2017. https://doi.org/10.1017/9781108277457

18 thms2 active usersReviewed

Probability Random Matrix Theory Statistics·Captain: mikedeng1

User-Friendly Tail Bounds for Sums of Random Matrices IV: The Matrix Bennett and Bernstein Inequalities for Independent Zero-Mean Random Matrices with Bounded Largest EigenvalueResearch Paper

Motivation

The scalar Bernstein and Bennett inequalities bound the upper tail of a sum of independent, zero-mean random variables that are bounded above: the tail is governed by the total variance at moderate deviations and by the uniform bound in the far tail. Many questions in randomized numerical linear algebra, matrix completion, covariance estimation, graph sparsification and statistical learning reduce to the same question for a sum of independent random matrices, where the quantity of interest is the largest eigenvalue or the spectral norm of the sum rather than a scalar.

Ahlswede and Winter (2002) introduced a matrix Laplace transform method based on the Golden–Thompson inequality. Oliveira (2010) and Gross (2011) proved matrix Bernstein-type bounds with this method. Tropp (arXiv:1004.4389, Found. Comput. Math. 12 (2012)) replaced the Golden–Thompson step with Lieb's concavity theorem, obtaining a master tail bound for independent sums (Theorem 3.6) from which matrix Bennett and Bernstein inequalities follow with the variance parameter $\|\sum_k \mathbb E X_k^2\|$ , the natural analogue of the scalar variance. This mission formalizes §6 of that paper.

Timeline:

1924–1962, Bernstein and Bennett: scalar inequalities for bounded and subexponential sums.
2002, Ahlswede–Winter: the matrix Laplace transform method, via Golden–Thompson.
2010, Oliveira; Gross: matrix Bernstein-type bounds by the Ahlswede–Winter method.
2010–2012, Tropp: master tail bound via Lieb's theorem; matrix Bennett and Bernstein inequalities (Theorems 6.1, 6.2) with variance parameter $\|\sum_k\mathbb E X_k^2\|$ .

Setting

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

A random matrix is a measurable map $X:\Omega\to\mathbb C^{d\times d}$ on a probability space $(\Omega,\mathcal F,\mathbb P)$ ; its expectation $\mathbb E X$ is taken entrywise. A finite sequence $X_1,\dots,X_n$ of random self-adjoint matrices is independent if the maps are mutually independent.

The setting of the goal: $X_1,\dots,X_n$ are independent random self-adjoint matrices with

\mathbb E X_k=0\qquad\text{and}\qquad \lambda_{\max}(X_k)\le R\ \text{almost surely},

and the total variance is $\sigma^2:=\big\|\sum_k \mathbb E(X_k^2)\big\|$ . Bennett's function is $h(u):=(1+u)\log(1+u)-u$ for $u\ge0$ .

Formalization targets

Goal: Theorem 6.1 (matrix Bernstein, bounded case)

For every $t\ge0$ , the following chain holds:

\mathbb P\Big\{\lambda_{\max}\Big(\sum_k X_k\Big)\ge t\Big\}\le d\cdot\exp\Big(-\frac{\sigma^2}{R^2}\,h\Big(\frac{Rt}{\sigma^2}\Big)\Big)\le d\cdot\exp\Big(\frac{-t^2/2}{\sigma^2+Rt/3}\Big),

and the last term is at most $d\,e^{-3t^2/8\sigma^2}$ for $t\le\sigma^2/R$ and at most $d\,e^{-3t/8R}$ for $t\ge\sigma^2/R$ . The first inequality is the matrix Bennett inequality, the second the matrix Bernstein inequality, and the case split the split Bernstein inequality.

Milestones, in attack order

Theorem 3.6, the master tail bound $\mathbb P\{\lambda_{\max}(\sum_k X_k)\ge t\}\le e^{-\theta t}\operatorname{tr}\exp(\sum_k\log\mathbb E e^{\theta X_k})$ for $\theta>0$ .
Corollary 3.7: a semidefinite bound $\mathbb E e^{\theta X_k}\preccurlyeq e^{g(\theta)A_k}$ gives $\mathbb P\{\lambda_{\max}(\sum_k X_k)\ge t\}\le d\,e^{-\theta t+g(\theta)\lambda_{\max}(\sum_k A_k)}$ .
Lemma 6.7: if $\mathbb E X=0$ and $\lambda_{\max}(X)\le1$ , then $\mathbb E e^{\theta X}\preccurlyeq\exp\big((e^\theta-\theta-1)\,\mathbb E X^2\big)$ for $\theta>0$ .
Theorem 6.1(i), the matrix Bennett inequality on its own.
The numerical bound $h(u)\ge\dfrac{u^2/2}{1+u/3}$ for $u\ge0$ , from the proof of Theorem 6.1.

Further items

Lemma 6.8 (the matrix mgf bound $\mathbb E e^{\theta X}\preccurlyeq\exp(\frac{\theta^2}{2(1-\theta)}A^2)$ under $\mathbb E X^p\preccurlyeq\frac{p!}{2}A^2$ ) and Theorem 6.2 (matrix Bernstein, subexponential case: $\mathbb P\{\lambda_{\max}(\sum_k X_k)\ge t\}\le d\exp(\frac{-t^2/2}{\sigma^2+Rt})$ , split as $d\,e^{-t^2/4\sigma^2}$ and $d\,e^{-t/4R}$ ) are included as further theorems.

Significance

Matrix Bernstein is the most used inequality of the paper: it bounds the spectral norm of a sum of independent bounded random matrices with only a logarithmic dimensional factor, and it is the standard tool behind sampling bounds for matrix completion, randomized low-rank approximation, spectral sparsification, covariance estimation and the analysis of random features. Theorem 6.1 assumes only an upper bound on the largest eigenvalue of each summand, so it applies to summands with unbounded smallest eigenvalues; applied to $\{X_k\}$ and $\{-X_k\}$ separately it controls both tails.

The results are proved in the paper. As far as the local catalog shows, no machine-checked proof of the matrix Bennett or Bernstein inequality for complex Hermitian matrices exists; the platform has a matrix Bernstein statement for real symmetric matrices in a different form (Wainwright, Theorem 6.17), still open, and scalar Bennett and Bernstein inequalities. Formalizing Theorem 6.1 produces a reusable matrix concentration inequality together with its two ingredients, the matrix mgf bound of Lemma 6.7 and the scalar inequality relating Bennett's and Bernstein's exponents.

Difficulty

The scalar argument multiplies moment generating functions of independent summands. For matrices, $e^{A+B}\ne e^Ae^B$ unless $A$ and $B$ commute, so $\mathbb E\,\operatorname{tr} e^{\theta\sum_k X_k}$ does not factor; the master bound of Theorem 3.6 rests on Lieb's concavity theorem for $A\mapsto\operatorname{tr}\exp(H+\log A)$ , which is not in Mathlib. The mgf bound of Lemma 6.7 needs a semidefinite comparison between functions of a random matrix, the transfer rule $f\le g$ on the spectrum $\Rightarrow f(A)\preccurlyeq g(A)$ , and the operator monotonicity of the logarithm. The remaining steps (optimizing over $\theta$ , the inequality between $h$ and the Bernstein exponent) are real analysis.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; $\lambda_{\max}$ is the supremum of the real spectrum; $\|\cdot\|$ is the operator norm on $\ell_2^d$ ; $e^A$ and $\log A$ are Mathlib's continuous functional calculus cfc; the semidefinite order is Mathlib's MatrixOrder; expectation is entrywise. A random matrix is a measurable map, each $X_k$ is Hermitian at every $\omega$ , independence is iIndepFun, and the measure is a probability measure. The bound $\lambda_{\max}(X_k)\le R$ is assumed almost surely; no lower bound on the eigenvalues is assumed. The paper's standing regularity (§2.2) is made explicit as integrability of the entries of $X_k$ and $X_k^2$ (and of $e^{\theta X_k}$ where its expectation is taken). The infimum over $\theta>0$ in Theorem 3.6 and Corollary 3.7 is stated for every admissible $\theta>0$ .

The printed formulas divide by $R$ and $\sigma^2$ , so $0<R$ and $0<\sigma^2$ are hypotheses of Theorems 6.1 and 6.2; with Lean's convention $x/0=0$ , the case $\sigma^2=0$ would turn the Bennett bound into the trivial value $d$ , so the statement is not allowed to degenerate there. The chain is a conjunction of the probability bound and the inequalities between consecutive bounds, so the weaker reading "the probability is below each bound" does not satisfy it.

A complete development needs the matrix Laplace transform method, Lieb's theorem (or a substitute), operator monotonicity of the logarithm, the transfer rule for the functional calculus, and the scalar inequality $h(u)\ge(u^2/2)/(1+u/3)$ . The first four are reusable for every matrix concentration inequality of this paper and beyond. Contributions to any milestone are welcome.

Selected references

J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7, 2011; Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
R. Ahlswede 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
D. Gross, Recovering low-rank matrices from few coefficients in any basis, IEEE Trans. Inform. Theory 57 (2011) 1548–1566. https://arxiv.org/abs/0910.1879
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
G. Lugosi, Concentration-of-measure inequalities, lecture notes, 2009 (Theorems 5 and 6, scalar Bennett and Bernstein). https://www.econ.upf.edu/~lugosi/anu.pdf

9 thms2 active usersReviewed

Completed

Algebra Complexity Theory Theoretical Computer Science·Captain: mikedeng1

Most Tensor Problems Are NP-Hard 4: A Rational 2×2×2 Tensor Has Smaller Rank over the Reals Than over the RationalsResearch Paper

Motivation

The rank of a matrix does not depend on the field in which its entries are read: a rational matrix has the same rank over $\mathbb Q$ , $\mathbb R$ and $\mathbb C$ , because rank is computed by Gaussian elimination, which never leaves the field of the entries. For 3-tensors, arrays $\mathcal A = [\![a_{ijk}]\!]$ with three indices, this fails. Tensor rank governs the complexity of bilinear maps (the exponent of matrix multiplication is a statement about the rank of one tensor), the uniqueness of the CANDECOMP/PARAFAC decompositions used in psychometrics and signal processing, and the identifiability of latent-variable models. In each application the field matters: algorithms are run over $\mathbb R$ or $\mathbb C$ , while complexity results are often proved over $\mathbb Q$ or finite fields.

Håstad (1990) proved that deciding $\operatorname{rank}(\mathcal A) \le r$ is NP-complete over finite fields and NP-hard over $\mathbb Q$ . De Silva and Lim (2008) gave real tensors whose rank over $\mathbb C$ is strictly smaller than their rank over $\mathbb R$ . Hillar and Lim (2013, Theorem 1.14) showed that the same phenomenon already occurs between $\mathbb Q$ and $\mathbb R$ , for a $2\times2\times2$ tensor with integer entries, so that Håstad's result over $\mathbb Q$ does not by itself say anything about rank over $\mathbb R$ .

Setting

Let $E$ be a field. The outer product of $\mathbf x \in E^l$ , $\mathbf y \in E^m$ , $\mathbf z \in E^n$ is the tensor $\mathbf x\otimes\mathbf y\otimes\mathbf z \in E^{l\times m\times n}$ with entries $x_iy_jz_k$ . The rank of $\mathcal A$ over $E$ is

\operatorname{rank}_E(\mathcal A) = \min\Big\{ r : \mathcal A = \sum_{s=1}^{r} \lambda_s\,\mathbf x_s\otimes\mathbf y_s\otimes\mathbf z_s,\ \ \lambda_s\in E,\ \mathbf x_s\in E^l,\ \mathbf y_s\in E^m,\ \mathbf z_s\in E^n\Big\}.

If $\mathcal A$ has entries in a subfield $F \subseteq E$ , both $\operatorname{rank}_F(\mathcal A)$ and $\operatorname{rank}_E(\mathcal A)$ are defined, and $\operatorname{rank}_E(\mathcal A) \le \operatorname{rank}_F(\mathcal A)$ .

The paper's example uses $\mathbf x = [1,0]^\top$ , $\mathbf y = [0,1]^\top$ and

\mathcal A = 2\,\mathbf x\otimes\mathbf x\otimes\mathbf x - 4\,\mathbf y\otimes\mathbf y\otimes\mathbf x + 4\,\mathbf y\otimes\mathbf x\otimes\mathbf y - 4\,\mathbf x\otimes\mathbf y\otimes\mathbf y \in \mathbb Q^{2\times2\times2}.

A decomposition $\mathcal A = \mathbf u_1\otimes\mathbf u_2\otimes\mathbf u_3 + \mathbf v_1\otimes\mathbf v_2\otimes\mathbf v_3$ with $\mathbf u_i = [a_i,b_i]^\top$ , $\mathbf v_i = [c_i,d_i]^\top$ is equivalent to the eight cubic equations (30) in the twelve unknowns $a_1,\dots,d_3$ , one for each entry of $\mathcal A$ .

In Lean, outer x y z and rankOver E A implement the two definitions, tensorA is $\mathcal A$ , and System30 is (30).

Formalization targets

Goal: Theorem 1.14

\exists\, \mathcal A \in \mathbb Q^{2\times2\times2}:\quad \operatorname{rank}_{\mathbb R}(\mathcal A) < \operatorname{rank}_{\mathbb Q}(\mathcal A).

Milestones (proof of Theorem 1.14, p. 0:26)

With $\mathbf z = \mathbf x + \sqrt2\,\mathbf y$ and $\bar{\mathbf z} = \mathbf x - \sqrt2\,\mathbf y$ :

\bar{\mathbf z}\otimes\mathbf z\otimes\bar{\mathbf z} + \mathbf z\otimes\bar{\mathbf z}\otimes\mathbf z = \mathcal A,\qquad\text{so } \operatorname{rank}_{\mathbb R}(\mathcal A)\le 2.

A tensor of rank at most 2 over a field is a sum of two outer products, and for $\mathcal A$ the identity (29) $\mathcal A = \mathbf u_1\otimes\mathbf u_2\otimes\mathbf u_3 + \mathbf v_1\otimes\mathbf v_2\otimes\mathbf v_3$ holds exactly when the coordinates of $\mathbf u_i, \mathbf v_i$ satisfy (30).
Every solution of (30) in a field of characteristic zero satisfies $2c_2^2 - d_2^2 = 0$ and $c_1d_2d_3 + 2 = 0$ .
Lemma 8.1: (30) has no rational solution.
$\operatorname{rank}_{\mathbb Q}(\mathcal A) > 2$ .

Significance

The theorem shows that tensor rank, unlike matrix rank, is not invariant under field extension even between $\mathbb Q$ and $\mathbb R$ , and even for the smallest nontrivial format $2\times2\times2$ . Its consequence for complexity is that a hardness result for rank over $\mathbb Q$ cannot be transferred to $\mathbb R$ by reading the same instance in a larger field; the paper accordingly re-examines Håstad's construction to obtain hardness over $\mathbb R$ and $\mathbb C$ (Theorem 8.2), which is outside this mission.

The result is proved in the paper, with the decisive algebraic step delegated to a computer-algebra computation (Appendix). A machine-checked proof replaces that computation by a certificate verified in Lean, and it settles a printed error: one of the two consequences of (30) in the proof of Lemma 8.1 is printed with the wrong sign (see Formalization scope). No formalization of array tensor rank over a field, or of its field dependence, is known to exist in Mathlib or on this platform.

Difficulty

The upper bound is an identity among explicit $2\times2\times2$ arrays. The lower bound is the substance: one must show that the cubic system (30), which has real solutions, has no rational one. Since (30) is solvable over $\mathbb R$ , no argument by signs, inequalities or real geometry can work; the obstruction is arithmetic, coming from the irrationality of $\sqrt2$ . The step that fails in a naive attempt is the elimination: eliminating ten of the twelve unknowns from eight cubic equations by hand is impractical. A second, smaller difficulty is the reduction from " $\operatorname{rank}_{\mathbb Q}(\mathcal A) \le 2$ " to two terms of the special form (29), which requires absorbing the scalars and padding a decomposition with fewer than two terms.

Formalization scope

Tensors are functions Fin l → Fin m → Fin n → E, with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). Vectors are Fin n → E.
rankOver E A is the sInf over $\mathbb N$ of the lengths $r$ of decompositions $\sum_s \lambda_s\, \mathbf x_s\otimes\mathbf y_s\otimes\mathbf z_s$ . The set is nonempty (one term per entry), so this is the paper's minimum. Zero summands are allowed; this gives the same minimum as the paper's sum of nonzero rank-1 tensors.
$\operatorname{rank}_{\mathbb R}$ of a rational tensor is rankOver ℝ of its entrywise cast to $\mathbb R$ ; $\operatorname{rank}_{\mathbb Q}$ is rankOver ℚ, whose witnesses are rational. A formalization in which both ranks range over real witnesses would make the theorem false.
The goal is the printed existential. It is not a loophole: the milestones concern the paper's explicit tensor.
Readings of loose phrases: "Suppose not and that there exist $\mathbf u_i, \mathbf v_i$ with (29). Identity (29) gives eight equations found in (30)" is split into a general statement (rank at most 2 over any field means a sum of two outer products) and the equivalence of (29) with (30) over every field of characteristic zero (milestone 2); both are stated in a generality in which their hypotheses can hold, because for $\mathcal A$ over $\mathbb Q$ they cannot. "Polynomial consequences of (30)" is read as "holds at every solution of (30) in every field of characteristic zero" (milestone 3); over $\mathbb Q$ alone the statement would be vacuous, since (30) has no rational solution.
Corrected error. The paper prints the second consequence as $c_1d_2d_3 - 2 = 0$ . It is false: the real solution from milestone 1 has $c_1d_2d_3 = -2$ . The milestone states $c_1d_2d_3 + 2 = 0$ (checked by a Gröbner basis computation over $\mathbb Q$ ), which serves the paper's argument equally. The Appendix certificates $G_k$ , $H_k$ (p. 0:34) are not used in any statement.
Out of scope: Theorem 1.15/8.2 (Håstad's construction over $\mathbb R$ and $\mathbb C$ ) and the conjectures of §13.

Needed infrastructure: finite sums of arrays, Real.sqrt and irrational_sqrt_two, and an ideal-membership certificate for milestone 3. The array rank rankOver is reusable for any statement about tensor rank over a field. The platform's mme_tensor_rank (restriction-based rank of a TensorObj over a single field, from the matrix-multiplication exponent series) is a different object and is not reused. Proofs of any milestone, and alternative certificates for Lemma 8.1, are welcome.

Selected references

C. J. Hillar and L.-H. Lim, Most tensor problems are NP-hard, J. ACM 60(6), Art. 45, 2013. https://doi.org/10.1145/2512329 (arXiv: https://arxiv.org/abs/0911.1393)
J. Håstad, Tensor rank is NP-complete, J. Algorithms 11(4), 644–654, 1990. https://doi.org/10.1016/0196-6774(90)90014-6
V. de Silva and L.-H. Lim, Tensor rank and the ill-posedness of the best low-rank approximation problem, SIAM J. Matrix Anal. Appl. 30(3), 1084–1127, 2008. https://doi.org/10.1137/06066518X
F. L. Hitchcock, The expression of a tensor or a polyadic as a sum of products, J. Math. Phys. 6, 164–189, 1927. https://doi.org/10.1002/sapm192761164

8 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

A Primal-Dual Interior-Point Algorithm for Nonsymmetric Exponential-Cone Optimization 2: Rank-One Recursions Factor Y₀(Y₀ᵀS₀)⁻¹Y₀ᵀ = VVᵀ and S₀(Y₀ᵀS₀)⁻¹S₀ᵀ = UUᵀResearch Paper

Motivation

Quasi-Newton methods replace the Hessian of an objective by a matrix $H \succ 0$ that is updated from observed pairs of steps and gradient changes. The secant equation $HS = Y$ asks the new matrix to map the observed steps $S$ to the observed changes $Y$ . The best-known update is BFGS, which for $p$ simultaneous pairs $S, Y \in \mathbb{R}^{n\times p}$ reads

H_{\mathrm{BFGS}} := Y(Y^TS)^{-1}Y^T + H - HS(S^THS)^{-1}S^TH .

Schnabel (Quasi-Newton methods using multiple secant equations, technical report, University of Colorado at Boulder, 1983, reference [25] of the paper) studied such multiple-secant updates; one of his results is that a positive definite $H$ with $HS = Y$ exists exactly when $Y^TS \succ 0$ .

Dahl and Andersen (Math. Program. 194:341–370, 2022) use multiple-secant BFGS updates to build primal-dual scaling matrices for an interior-point algorithm on the nonsymmetric exponential cone, following Tunçel (Found. Comput. Math. 1:229–254, 2001) and Myklebust and Tunçel (arXiv:1411.2129). In their setting $p = 2$ , and they need the update in factored, low-rank form. Their Theorem 2 supplies it: the term $Y(Y^TS)^{-1}Y^T$ , and its counterpart $S(Y^TS)^{-1}S^T$ for the inverse update, are computed by $p$ rank-one steps. These steps resemble single-secant quasi-Newton updates, and no inverse is formed. This mission formalizes Theorem 2 and the steps of its proof.

Setting

Let $n, p \ge 0$ and $Y_0, S_0 \in \mathbb{R}^{n\times p}$ . Write $e_k$ for the $k$ -th unit vector of $\mathbb{R}^p$ and $\langle a, b\rangle = a^Tb$ for the inner product of $\mathbb{R}^n$ , so that $\langle Ye_k, Se_k\rangle = (Y^TS)_{kk}$ . The hypothesis of the theorem is

Y_0^TS_0 \succ 0,

meaning that the $p\times p$ matrix $Y_0^TS_0$ is symmetric and positive definite.

For $k = 1, \dots, p$ the recursions (25)–(26) are

v_k := \frac{Y_{k-1}e_k}{\langle Y_{k-1}e_k, S_{k-1}e_k\rangle^{1/2}}, \qquad Y_k := Y_{k-1} - v_kv_k^TS_{k-1},

u_k := \frac{S_{k-1}e_k}{\langle Y_{k-1}e_k, S_{k-1}e_k\rangle^{1/2}}, \qquad S_k := S_{k-1} - u_ku_k^TY_{k-1}.

Both updates of step $k$ use the previous pair $(Y_{k-1}, S_{k-1})$ . Collect the vectors into $V := (v_1 \cdots v_p)$ and $U := (u_1 \cdots u_p) \in \mathbb{R}^{n\times p}$ .

The proof uses two more objects. The first is the $p\times p$ matrix

L := \left(\frac{Y_0^TS_0e_1}{\langle Y_0e_1, S_0e_1\rangle^{1/2}}, \cdots, \frac{Y_{p-1}^TS_{p-1}e_p}{\langle Y_{p-1}e_p, S_{p-1}e_p\rangle^{1/2}}\right).

The second is $\Psi_k$ , the principal submatrix formed by the last $p-k$ rows and columns of $Y_k^TS_k$ . In Lean these are ExpConeIPM.Secant.Ys, Ss, d, V, U, L and Ψ, all in one definition item.

Formalization targets

Goal: Theorem 2 (pp. 357–358)

Y_0(Y_0^TS_0)^{-1}Y_0^T = VV^T, \qquad S_0(Y_0^TS_0)^{-1}S_0^T = UU^T .

Milestones (the steps of the proof, pp. 358–359)

(27). For $k = 1, \dots, p$ ,

Y_k^TS_k = Y_{k-1}^TS_{k-1} - \frac{(Y_{k-1}^TS_{k-1}e_k)(Y_{k-1}^TS_{k-1}e_k)^T}{\langle Y_{k-1}e_k, S_{k-1}e_k\rangle}.

Well-definedness. For $k = 0, \dots, p-1$ , $\Psi_k \succ 0$ , and in particular $\langle Y_ke_{k+1}, S_ke_{k+1}\rangle > 0$ .
Sparsity. $Y_je_k = S_je_k = 0$ for $1 \le k \le j \le p$ .
Cholesky factorization (28). $LL^T = Y_0^TS_0$ .
The $V$ -identity. $LV^T = Y_0^T$ .

The first identity of the goal follows from milestones 4 and 5. The paper says the second "follows similarly". The analogous identity $LU^T = S_0^T$ is not displayed in the paper, so it is not a milestone.

Significance

The result. Theorem 2 expresses the multiple-secant part of the BFGS update (23), and of its inverse, as a sum of $p$ rank-one terms $v_kv_k^T$ and $u_ku_k^T$ . Each term comes from a recursion that touches one column at a time. On pp. 359–360 Dahl and Andersen apply it twice with $p = 2$ . This gives the BFGS scaling of their exponential-cone algorithm as an explicit rank-3 update of $\mu F''(x)$ , which is how the algorithm implemented in MOSEK computes its scaling matrices (§6, p. 361 of the paper). The argument is a Cholesky factorization of $Y_0^TS_0$ carried out implicitly on the factors $Y_0$ and $S_0$ .

Formalizing it. The theorem is proved in the paper, in under a page. Its proof leaves two steps implicit. The first is that the symmetry of every $Y_k^TS_k$ , which (27) and the step to $LV^T = Y_0^T$ use, propagates from $Y_0^TS_0$ . The second is the second identity, which the paper does not prove. A machine-checked proof records both. To our knowledge no proof assistant has a formal treatment of multiple-secant updates. The recursion also gives a reusable statement: a column-by-column Schur-complement process on a product $Y^TS$ produces its Cholesky factor.

Difficulty

The obvious route expands $VV^T$ directly and compares it with $Y_0(Y_0^TS_0)^{-1}Y_0^T$ . This leads nowhere, because $v_k$ depends on all earlier steps through $Y_{k-1}$ and $S_{k-1}$ . The step that carries the proof is an invariant over the recursion. The trailing blocks $\Psi_k$ of $Y_k^TS_k$ must stay symmetric positive definite, and the leading columns of $Y_k$ and $S_k$ must stay zero. Both must be maintained together through a pair of coupled updates, in which $S_k$ is updated with the old $Y_{k-1}$ . A second difficulty is bookkeeping: the paper's 1-based columns, the step count $k$ , and the trailing block of size $p-k$ shift relative to each other.

The hypothesis needs care. If $Y_0^TS_0$ is only assumed to satisfy $x^TY_0^TS_0x > 0$ for $x \ne 0$ , without symmetry, the identities are false in general. A $5\times 3$ instance whose symmetric part is positive definite, with a small antisymmetric part, violates the first identity by $0.44$ in the largest entry.

Formalization scope

Everything is real matrix algebra over Matrix (Fin n) (Fin p) ℝ, with arbitrary $n, p$ (including $p = 0$ , where both sides are zero). The formalization commits to the following conventions.

$Y_0^TS_0 \succ 0$ is Matrix.PosDef, which includes symmetry. The inverse is Matrix.inv. It is a genuine inverse under this hypothesis.
Columns are 0-based. Column j : Fin p is the paper's $e_{j+1}$ . Ys Y₀ S₀ k and Ss Y₀ S₀ k are $Y_k$ and $S_k$ after $k$ steps, and they are left unchanged after step $p$ . d Y₀ S₀ j is $\langle Y_je_{j+1}, S_je_{j+1}\rangle$ .
The square root is Real.sqrt. The division by it is multiplication by an inverse. Both return junk values on non-positive arguments, which never occur under the hypothesis; milestone 2 states this.
$V$ , $U$ and $L$ are computed from the recursion (25)–(26). They are never chosen as some factorization satisfying the conclusion. The trivializing formalization, which defines $V$ as any factor of $Y_0(Y_0^TS_0)^{-1}Y_0^T$ , is ruled out by construction.
Each milestone carries the theorem's hypothesis $Y_0^TS_0 \succ 0$ . No hypothesis on the intermediate $Y_k^TS_k$ is assumed, since its symmetry is part of what must be proved.

No repair of the printed statements was needed. On p. 359 two misprints are not copied: $\langle Y_{p-1}^Te_p, S_{p-1}e_p\rangle$ for $\langle Y_{p-1}e_p, S_{p-1}e_p\rangle$ , and $S_i^TY_i$ for $Y_i^TS_i$ . The definition of $L$ uses $Y_i^TS_i$ .

A complete development needs rank-one updates of products, Schur complements of a positive definite matrix in its leading entry, and inverses of $LL^T$ for an invertible $L$ . Schnabel's existence theorem (Theorem 1 of the paper) and the applications on pp. 359–360 are outside the mission. A general lemma on Schur-complement recursions producing Cholesky factors would be reusable on its own. Contributions on the U-side identity $LU^T = S_0^T$ are welcome.

Selected references

J. Dahl, E. D. Andersen, A primal-dual interior-point algorithm for nonsymmetric exponential-cone optimization, Math. Program. 194:341–370, 2022. https://doi.org/10.1007/s10107-021-01631-4
R. B. Schnabel, Quasi-Newton methods using multiple secant equations, Technical Report, University of Colorado at Boulder, 1983 (no stable online link known; cited as [25] in Dahl–Andersen).
L. Tunçel, Generalization of primal-dual interior-point methods to convex optimization problems in conic form, Found. Comput. Math. 1:229–254, 2001. https://doi.org/10.1007/s102080010008
T. Myklebust, L. Tunçel, Interior-point algorithms for convex optimization based on primal-dual metrics, arXiv:1411.2129, 2014. https://arxiv.org/abs/1411.2129

7 thms2 active usersReviewed

Probability Random Matrix Theory·Captain: mikedeng1

User-Friendly Tail Bounds for Sums of Random Matrices II: Matrix Gaussian and Rademacher Series Have Subgaussian Tails with Variance Parameter ‖Σ A_k²‖Research Paper

Motivation

A matrix Gaussian series $\sum_k \gamma_k A_k$ , a sum of fixed self-adjoint matrices each multiplied by an independent standard normal variable, is the simplest sum of independent random matrices. It already appears in the analysis of random designs, in compressed sensing, in randomized numerical linear algebra and in quantum information, wherever one needs to know how large the spectrum of a random linear combination of matrices can be. Its Rademacher analogue $\sum_k \varepsilon_k A_k$ , with random signs, plays the same role in symmetrization arguments.

For real coefficients $a_k$ the answer is classical: $\sum_k \gamma_k a_k$ is normal with variance $\sum_k a_k^2$ , so its upper tail is at most $e^{-t^2/2\sigma^2}$ . Tropp's paper (arXiv:1004.4389v7) shows that the same bound holds for the largest eigenvalue of a matrix series, with an explicit dimensional factor and with the variance parameter $\|\sum_k A_k^2\|$ .

Timeline. Noncommutative Khintchine inequalities (Lust-Piquard 1986; Lust-Piquard and Pisier 1991) control the moments of matrix Rademacher and Gaussian series and imply tail bounds of this type. Ahlswede and Winter (2002, arXiv:quant-ph/0012127) introduced the matrix Laplace transform method, whose bounds depend on the sum of the norms $\sum_k\|A_k^2\|$ . Oliveira (2010, arXiv:1004.3821) obtained bounds of the same form as Theorem 4.1. Tropp (2012) derived the result from a master inequality built on Lieb's concavity theorem (1973), which produces the norm of the sum, $\|\sum_k A_k^2\|$ , as variance parameter. The paper itself notes that Theorem 4.1 and Corollary 4.2 are not new results; the contribution is the route through the master bound.

Setting

Fix a dimension $d\ge1$ . Matrices are $d\times d$ complex arrays; a matrix is self-adjoint if it equals its conjugate transpose. For a self-adjoint $A$ , $\lambda_{\max}(A)$ is its largest eigenvalue, and $\|A\|$ is the spectral norm, the operator norm on $\mathbb C^d$ with the Euclidean norm. Functions of a self-adjoint matrix are defined through its eigen-decomposition: $e^A$ , $\log A$ (for positive-definite $A$ ), $\cosh A$ . The semidefinite order $A\preccurlyeq H$ means that $H-A$ is positive semidefinite.

A random matrix is a measurable map from a probability space $(\Omega,\mathcal F,\mathbb P)$ into the $d\times d$ complex matrices; its expectation $\mathbb E X$ is taken entry by entry. A Rademacher variable takes the values $\pm1$ with probability $1/2$ each; a standard normal variable has law $N(0,1)$ .

The data of the mission are fixed self-adjoint matrices $A_1,\dots,A_n$ and independent scalar variables $\xi_1,\dots,\xi_n$ , all standard normal or all Rademacher. The variance parameter is

\sigma^2 := \Big\|\sum_k A_k^2\Big\|.

Formalization targets

Goal: Theorem 4.1 (p. 14)

For all $t\ge0$ ,

\mathbb P\Big\{\lambda_{\max}\Big(\sum_k\xi_kA_k\Big)\ge t\Big\}\le d\,e^{-t^2/2\sigma^2},\qquad \mathbb P\Big\{\Big\|\sum_k\xi_kA_k\Big\|\ge t\Big\}\le 2d\,e^{-t^2/2\sigma^2}.

Milestones

Theorem 3.6 (master tail bound, p. 12): for independent random self-adjoint $X_k$ and every $t$ ,

\mathbb P\Big\{\lambda_{\max}\Big(\sum_kX_k\Big)\ge t\Big\}\le\inf_{\theta>0}e^{-\theta t}\operatorname{tr}\exp\Big(\sum_k\log\mathbb Ee^{\theta X_k}\Big).

Corollary 3.7 (p. 12): if $\mathbb Ee^{\theta X_k}\preccurlyeq e^{g(\theta)A_k}$ with $g\ge0$ , then the tail is at most $d\inf_{\theta>0}e^{-\theta t+g(\theta)\rho}$ with $\rho=\lambda_{\max}(\sum_kA_k)$ .
Display (2.4) (p. 8): $\cosh(A)\preccurlyeq e^{A^2/2}$ for every self-adjoint $A$ .
Lemma 4.3 (p. 15): $\mathbb Ee^{\varepsilon\theta A}\preccurlyeq e^{\theta^2A^2/2}$ for Rademacher $\varepsilon$ and $\mathbb Ee^{\gamma\theta A}=e^{\theta^2A^2/2}$ for standard normal $\gamma$ .

Further item: Corollary 4.2 (p. 15)

For fixed $d_1\times d_2$ matrices $B_k$ and $\sigma^2=\max\{\|\sum_kB_kB_k^*\|,\|\sum_kB_k^*B_k\|\}$ ,

\mathbb P\Big\{\Big\|\sum_k\xi_kB_k\Big\|\ge t\Big\}\le(d_1+d_2)\,e^{-t^2/2\sigma^2}.

Significance

The result. Theorem 4.1 is the template for every inequality in the paper: a scalar tail bound carried over to matrices at the cost of a factor $d$ , with a variance parameter that is the norm of a sum rather than a sum of norms. The difference matters: $\sum_k\|A_k^2\|$ can exceed $\|\sum_kA_k^2\|$ by a factor of $d$ , and §4 of the paper shows that both the variance parameter and the dimensional factor in (4.3) are needed in general. Corollary 4.2 transfers the bound to the largest singular value of a rectangular series, which covers Gaussian matrices with nonuniform variances (§4.3).

Formalizing it. The theorem is proved in the paper; the work here is to formalize that proof. The milestones are reusable beyond this mission: Theorem 3.6 and Corollary 3.7 are the common entry point of the Chernoff, Bernstein and Azuma missions of this series, and the Rademacher half of Lemma 4.3 is used again in the matrix Azuma mission. No machine-checked proof of these matrix inequalities was found in Mathlib or on the platform when this mission was drafted.

Difficulty

The scalar argument bounds $\mathbb E e^{\theta\sum_k X_k}$ by the product of the individual mgfs, using $e^{a+b}=e^ae^b$ . For matrices this identity fails when the summands do not commute, and the trace inequality that replaces it for two matrices (Golden–Thompson) has no analogue for three or more. Controlling the trace mgf of a sum of many noncommuting independent matrices therefore requires a genuinely matrix-analytic input with no scalar counterpart; the naive product bound is not available. A second difficulty is infrastructural: matrix functions, the semidefinite order and expectations of random matrices must be combined in a single setting.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; self-adjointness is IsHermitian; $e^A$ , $\log A$ , $\cosh A$ are Mathlib's continuous functional calculus cfc; $\preccurlyeq$ is Mathlib's Loewner order under MatrixOrder; $\lambda_{\max}$ is the supremum of the real spectrum; $\|\cdot\|$ is the operator norm on $\ell_2$ . Expectation is entrywise, and the paper's standing regularity assumption is made explicit as entrywise integrability of every matrix whose expectation is taken. The infimum over $\theta>0$ is stated pointwise: the bound is asserted for every $\theta>0$ at which the mgfs exist, which is equivalent to the infimum form. Independence is iIndepFun of the scalar variables, and "Gaussian or Rademacher" is the disjunction of two hypotheses, never a mixture of laws.

The variance parameter is the norm of the sum $\|\sum_kA_k^2\|$ ; a formalization with $\sum_k\|A_k^2\|$ , with a constant different from $1/2$ , or with the dimensional factor omitted is a different theorem. At $\sigma^2=0$ , Lean's division by zero makes the bound the trivial $d$ ; this is the only degenerate case and it is valid.

The development needs: the spectral calculus for Hermitian matrices, monotonicity of the trace exponential, operator monotonicity of the matrix logarithm, Lieb's theorem, and moments of the Gaussian. These are reusable well beyond this paper; proofs of the milestones, of supporting matrix-analysis lemmas, and alternative routes (for instance through noncommutative Khintchine inequalities) are all welcome.

Selected references

J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited from arXiv:1004.4389v7. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://arxiv.org/abs/quant-ph/0012127
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
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
F. Lust-Piquard and G. Pisier, Non commutative Khintchine and Paley inequalities, Ark. Mat. 29 (1991) 241–260. https://doi.org/10.1007/BF02384340

8 thms2 active usersReviewed

Probability Random Matrix Theory·Captain: mikedeng1

User-Friendly Tail Bounds for Sums of Random Matrices I: The Master Tail Bound — the Largest Eigenvalue of an Independent Sum Is Controlled by the Sum of the Matrix Cumulant Generating FunctionsResearch Paper

Motivation

Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.

Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.

Timeline:

1973: Lieb proves concavity of $A\mapsto \operatorname{tr}\exp(H+\log A)$ on positive-definite matrices; Epstein gives a second proof (Epstein 1973).
2002: Ahlswede and Winter introduce the matrix Laplace transform method, decoupling summands with the Golden–Thompson inequality.
2010: Oliveira's variant of the matrix Laplace transform bound.
2010–2012: Tropp derives the master bound for independent sums from Lieb's theorem (journal version: Found. Comput. Math. 12 (2012)); in 2011 he also derives Lieb's theorem from the joint convexity of quantum relative entropy (arXiv:1101.1070).

Setting

All matrices are $d\times d$ arrays of complex numbers with $d\ge1$ . A matrix $A$ is self-adjoint (Hermitian) when $A=A^*$ ; it then has real eigenvalues, and $\lambda_{\max}(A)$ denotes the largest one. For a function $f:\mathbb R\to\mathbb R$ and a self-adjoint $A=Q\Lambda Q^*$ with $Q$ unitary and $\Lambda$ diagonal, $f(A):=Qf(\Lambda)Q^*$ . This defines the matrix exponential $e^{A}$ of every self-adjoint matrix and the matrix logarithm $\log A$ of every positive-definite matrix, with $\log(e^A)=A$ . The trace exponential is $A\mapsto\operatorname{tr}e^{A}$ .

A random self-adjoint matrix is a measurable map $X$ from a probability space $(\Omega,\mathcal F,\mathbb P)$ to the self-adjoint matrices. Its expectation $\mathbb E X$ is the matrix of the expectations of its entries. A finite sequence $X_1,\dots,X_n$ is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of $X$ are

M_X(\theta):=\mathbb E\,e^{\theta X},\qquad \Xi_X(\theta):=\log\mathbb E\,e^{\theta X},\qquad\theta\in\mathbb R,

which may fail to exist for some $\theta$ . In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.

Formalization targets

Goal: the master tail bound (Theorem 3.6)

For independent random self-adjoint matrices $X_1,\dots,X_n$ and every $t\in\mathbb R$ ,

\mathbb P\Bigl\{\lambda_{\max}\Bigl(\sum_k X_k\Bigr)\ge t\Bigr\}\le\inf_{\theta>0}\Bigl\{e^{-\theta t}\cdot\operatorname{tr}\exp\Bigl(\sum_k\log\mathbb E\,e^{\theta X_k}\Bigr)\Bigr\}.

It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.

Milestones

Proposition 3.1 (Laplace transform method): $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}\{e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}\}$ .
Theorem 3.2 (Lieb): for fixed self-adjoint $H$ , $A\mapsto\operatorname{tr}\exp(H+\log A)$ is concave on the positive-definite cone.
Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E\,e^{X})$ .
Lemma 3.4 (subadditivity of matrix cgfs): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$ for $\theta\in\mathbb R$ .

Significance

The master bound reduces every tail estimate for $\lambda_{\max}$ of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.

All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).

Difficulty

The scalar argument factors $\mathbb E\exp(\sum_k\theta X_k)=\prod_k\mathbb E\,e^{\theta X_k}$ , which needs $e^{a+b}=e^ae^b$ . For non-commuting matrices $e^{A+B}\ne e^Ae^B$ , so this step fails. The Golden–Thompson inequality $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever $\lambda_{\max}$ appears; for $d=0$ the largest eigenvalue would be $0$ and the bound would fail at $t\le0$ . Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.

The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of $e^{\theta X_k}$ is integrable for the $\theta$ in question. The infimum over $\theta>0$ is stated as the bound for every $\theta>0$ at which the moment generating functions exist; since an inequality $p\le\inf_\theta F(\theta)$ is equivalent to $p\le F(\theta)$ for every $\theta$ , and the paper treats a non-existent moment generating function as $+\infty$ , this is exact. A real-valued infimum over $\theta$ , or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ( $\inf$ of an unbounded set and the integral of a non-integrable function are $0$ ); the formalization rules both out.

Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48(3) (2002) 569–579. https://arxiv.org/abs/quant-ph/0012127
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
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
H. Epstein, Remarks on two theorems of E. Lieb, Comm. Math. Phys. 31 (1973) 317–325. https://doi.org/10.1007/BF01646492
J. A. Tropp, From joint convexity of quantum relative entropy to a concavity theorem of Lieb, Proc. Amer. Math. Soc. 140 (2012) 1757–1760. https://arxiv.org/abs/1101.1070

6 thms2 active usersReviewed

Control Theory Dynamical Systems Graph Theory·Captain: mikedeng1

Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators 2: λ₂(L(P_ij cos φ_ij)) > λ_critical Gives Phase Cohesiveness and Exponential Frequency SynchronizationResearch Paper

Motivation

Transient stability of a power grid asks whether the generators of the network return to synchronous operation after a large disturbance such as a fault or a line trip. In the classical network-reduced model the rotor angles obey second-order swing equations, and stability certificates usually come from energy functions evaluated numerically. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) relate this problem to a first-order system of coupled phase oscillators, the non-uniform Kuramoto model, and derive purely algebraic conditions on the network parameters under which the oscillators synchronize. Such conditions read as "the network connectivity dominates non-uniformity, losses and lack of phase cohesiveness" and are checked from the data alone, without simulation.

The paper gives two such sufficient conditions. This mission formalizes the second, Theorem V.5, which measures connectivity by the algebraic connectivity of the lossless coupling and therefore applies to sparse (connected, not necessarily complete) networks. A companion mission treats Theorem V.3, the condition for complete graphs.

Timeline. For the classical Kuramoto model, Jadbabaie, Motee and Barahona (ACC, 2004) and Chopra and Spong (IEEE TAC, 2009) analysed synchronization with the Lyapunov function $\|H\theta\|_2^2$ , and Chopra and Spong proved frequency synchronization under cohesive phases. Dörfler and Bullo (2009–2012) extended the analysis to non-uniform time constants $D_i$ , phase shifts $\varphi_{ij}$ and non-complete graphs, using a weighted Lyapunov function.

Setting

There are $n\ge2$ oscillators with phases $\theta_i$ , time constants $D_i>0$ , natural frequencies $\omega_i\in\mathbb R$ , coupling weights $P_{ij}\ge0$ and phase shifts $\varphi_{ij}\in[0,\pi/2[$ ( $i\ne j$ ), with $P_{ii}=\varphi_{ii}=0$ . The non-uniform Kuramoto model is

D_i\dot\theta_i=\omega_i-\sum_{j=1}^nP_{ij}\sin(\theta_i-\theta_j+\varphi_{ij}),\qquad i=1,\dots,n. \tag{8}

In this mission $P=P^T$ , and its non-zero entries induce a connected graph.

$H\in\mathbb R^{n(n-1)/2\times n}$ is the incidence matrix of the complete graph: $H\theta=(\theta_2-\theta_1,\dots)$ lists all pairwise differences, and $\|H\theta\|_2^2=\sum_{i<j}(\theta_i-\theta_j)^2$ .
$\Delta(\gamma)$ is the set of configurations contained in an open arc of length $\gamma$ , i.e. $\max_{i,j}|\theta_i-\theta_j|<\gamma$ .
The Laplacian of a symmetric matrix $A$ is $L(a_{ij})=\operatorname{diag}(\sum_ja_{ij})-A$ and $\lambda_2(L(a_{ij}))$ is its second-smallest eigenvalue, the algebraic connectivity. The lossless coupling is the matrix $(P_{ij}\cos\varphi_{ij})$ .
$\kappa=\sum_kD_k$ , $\alpha=\sqrt{\min_{i\ne j}\{D_iD_j\}/\max_{i\ne j}\{D_iD_j\}}$ , $\varphi_{\max}=\max_{i,j}\varphi_{ij}$ , $\Omega=\sum_i\omega_i/\sum_iD_i$ .
The critical value is

\lambda_{\mathrm{critical}}=\frac{\|HD^{-1}\omega\|_2+\sqrt n\,\big\|\big[\sum_j\tfrac{P_{1j}}{D_1}\sin\varphi_{1j},\dots,\sum_j\tfrac{P_{nj}}{D_n}\sin\varphi_{nj}\big]\big\|_2}{\cos(\varphi_{\max})(\kappa/n)\alpha/\max_{i\ne j}\{D_iD_j\}}. \tag{33}

The radii $\gamma_{\max}\in\,]\pi/2-\varphi_{\max},\pi]$ and $\gamma_{\min}\in[0,\pi/2-\varphi_{\max}[$ solve $\operatorname{sinc}(\gamma_{\max})/\operatorname{sinc}(\pi/2-\varphi_{\max})=\sin(\gamma_{\min})/\cos(\varphi_{\max})=\lambda_{\mathrm{critical}}/\lambda_2(L(P_{ij}\cos\varphi_{ij}))$ .

Formalization targets

Goal: Theorem V.5 (Synchronization condition II)

If $\lambda_2(L(P_{ij}\cos\varphi_{ij}))>\lambda_{\mathrm{critical}}$ , then

for every $\gamma\in[\gamma_{\min},\alpha\gamma_{\max}]$ the set $\{\theta\in\Delta(\pi):\|H\theta\|_2\le\gamma\}$ is positively invariant, and every solution with $\theta(0)\in\Delta(\pi)$ , $\|H\theta(0)\|_2<\alpha\gamma_{\max}$ eventually satisfies $\|H\theta(t)\|_2\le\gamma$ for every $\gamma>\gamma_{\min}$ ;
for every such solution the frequencies converge exponentially to a common $\dot\theta_\infty\in[\dot\theta_{\min}(0),\dot\theta_{\max}(0)]$ ; if $\varphi\equiv0$ , then $\dot\theta_\infty=\Omega$ and the rate is no worse than

\lambda_{\mathrm{fe}}(\gamma)=\lambda_2(L(P_{ij}))\cos(\gamma)\cos(\angle(D\mathbf 1,\mathbf 1))^2/D_{\max}\qquad(\gamma\in\,]\gamma_{\min},\pi/2[).

Milestones

Lemma V.8 (the identity (36) that replaces $HD^{-1}H^T$ by $\kappa$ ), Lemma V.9 (a quadratic-form bound by $\lambda_2$ ), the sinc estimate and the bound $\tilde X$ on the lossy coupling (p. 25), the Lyapunov-derivative bound (37), the sandwich bounds (39) on $W$ , the existence and uniqueness of $\gamma_{\min},\gamma_{\max}$ from the analysis of (41), and the eventual entry of every trajectory into $\{\|H\theta\|_2<\pi/2-\varphi_{\max}\}$ .

Significance

The condition is checkable from network data: $\lambda_2$ of a weighted Laplacian, two vector norms and the extreme time constants. It applies to sparse networks, where the complete-graph condition of Theorem V.3 does not, and specializes for classical Kuramoto oscillators to $K>\|H\omega\|_2$ (Remark V.7). Through the singular-perturbation argument of Section IV, conditions of this kind certify transient stability of the network-reduced power system.

The result is proved in the paper; no machine-checked version is known. A formalization fixes several points the printed text leaves loose: the norm $\|H\theta\|_2$ is written on p. 23 with a double sum that counts each pair twice; the chain defining $\tilde X$ on p. 25 is printed with its inequalities reversed; and "reaches $\{\|H\theta\|_2\le\gamma_{\min}\}$ " holds only asymptotically. The formal statements make each of these precise.

Difficulty

The obvious Lyapunov function, $\|H\theta\|_2^2$ , has a sign-indefinite derivative as soon as the $D_i$ differ, because the coupling $P_{ij}/D_i$ is not symmetric. The weighted function $W(H\theta)=\frac14\sum_{i,j}D_iD_j|\theta_i-\theta_j|^2$ restores a symmetric structure, but only through the non-obvious identity (36). After that, the sinusoidal coupling has to be bounded below by a quadratic form on a set where the phase differences stay below $\pi$ , the lossy coupling has to be bounded above uniformly in the state, and the resulting ultimate-boundedness argument has to be run with sublevel sets of $W$ , which are ellipsoids rather than balls of $\|H\theta\|_2$ unless all $D_i$ coincide. The constants $\alpha$ , $\gamma_{\min}$ , $\gamma_{\max}$ come from this mismatch, and the passage from sublevel sets back to balls is the most delicate step.

Formalization scope

Configurations are real lifts $\theta\in\mathbb R^n$ ; $\Delta(\pi)$ means $\theta_i-\theta_j<\pi$ for all $i,j$ , and $\|H\theta\|_2$ is the pair-sum norm. A solution is a function $\theta:\mathbb R\to\mathbb R^n$ with right derivative at $0$ and derivative at every $t>0$ equal to the vector field of (8), and statements quantify over every solution. $\dot\theta$ is the vector field evaluated along the solution.
Added hypotheses: $n\ge2$ (needed for $\lambda_2$ and the extrema over $i\ne j$ ), and $\varphi_{ij}=\varphi_{ji}$ , which the page uses silently (the lossless coupling must be a symmetric Laplacian) and which holds for power networks. $P_{ij}\ge0$ off the diagonal, since §V.B allows zero weights.
Corrections: $\|H\theta\|_2$ sums over pairs $i<j$ ; the $\tilde X$ chain is stated as $\|HX\|_2\le\tilde X$ ; the attraction clause of 1) is stated as "eventually below every $\gamma>\gamma_{\min}$ "; the rate of (19) is taken positive (it is printed with a minus sign), and the "Moreover" rate is stated for every $\gamma\in\,]\gamma_{\min},\pi/2[$ because (19) depends on an arc length the theorem does not name. The page's "Moreover, if $\gamma_{\max}=0$ " is read as $\varphi_{\max}=0$ , a misprint: $\gamma_{\max}>\pi/2-\varphi_{\max}$ is never zero.
$\gamma_{\min},\gamma_{\max}$ are quantified subject to their defining equations, and a milestone proves they exist and are unique, so they are not free parameters. Condition (33) is satisfiable (equal ratios $\omega_i/D_i$ and $\varphi\equiv0$ give $\lambda_{\mathrm{critical}}=0$ ), so the goal is not vacuous.
Source: the arXiv preprint v4 of the SICON article; every page and number refers to that preprint.
Infrastructure: weighted graph Laplacians, their second eigenvalue and Courant–Fischer-type bounds, incidence matrices, and ultimate-boundedness arguments for ODEs. The Laplacian and incidence-matrix layer is reusable for consensus and network-dynamics missions; contributions on any milestone are welcome.

Selected references

F. Dörfler, F. Bullo, Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators, SIAM J. Control Optim. 50(3), 2012; preprint arXiv:0910.5673v4. https://arxiv.org/abs/0910.5673v4
N. Chopra, M. W. Spong, On exponential synchronization of Kuramoto oscillators, IEEE Trans. Automatic Control 54(2), pp. 353–357, 2009 (reference [32] of the source).
A. Jadbabaie, N. Motee, M. Barahona, On the stability of the Kuramoto model of coupled nonlinear oscillators, American Control Conference, Boston, 2004, pp. 4296–4301 (reference [33] of the source).
H. K. Khalil, Nonlinear Systems, 3rd ed., Prentice Hall, 2002 (ultimate boundedness, Theorem 4.18; reference [51] of the source).

14 thms2 active usersReviewed

Graph Theory Probability Theoretical Computer Science·Captain: mikedeng1

Spectral Sparsification of Graphs 1: Sampling Each Edge of a High-Conductance Graph with Probability min(1, Υ/min(dᵢ, dⱼ)) Gives a (1+ε)-Spectral Approximation with Few EdgesResearch Paper

Motivation

A spectral sparsifier of a graph is a much sparser weighted graph whose Laplacian quadratic form is within a factor $\sigma$ of the original on every vector. Spielman and Teng introduced the notion in Spectral Sparsification of Graphs as a strengthening of the cut sparsifiers of Benczúr and Karger: a spectral sparsifier preserves every cut, and in addition every quantity determined by the Laplacian quadratic form, such as effective resistances, eigenvalues and the behaviour of random walks. Sparsifiers are the reason linear systems in graph Laplacians can be solved in nearly linear time: one preconditions with a sparsifier and solves the sparse system instead (Spielman–Teng, arXiv:cs/0607105).

The construction in the paper has two halves: decompose the graph into pieces of high conductance, then sparsify each piece by random sampling. This mission is the second half, Theorem 6.1 of §6: in a graph whose normalized Laplacian has a spectral gap, keeping each edge independently with probability inversely proportional to the smaller degree of its endpoints, and reweighting kept edges by the inverse probability, produces a $(1+\epsilon)$ -spectral approximation with few edges, with high probability.

Timeline. Benczúr and Karger (1996) sampled edges with probabilities depending on edge strength and preserved cuts. Achlioptas and McSherry (2001) analysed random sampling of matrices through the random-matrix norm bound of Füredi and Komlós (1981), corrected by Vu (2007). Spielman and Teng (arXiv 2008, SIAM J. Comput. 2011) proved Theorem 6.1 by refining the Füredi–Komlós trace method for downsampling graphs that may already be sparse. Spielman and Srivastava (2008) later replaced conductance-based probabilities by effective resistances.

Setting

Let $G=(V,E)$ be an unweighted graph on a finite vertex set $V$ , $n=|V|$ , with degrees $d_i$ , adjacency matrix $A$ , diagonal degree matrix $D$ and Laplacian $L_G=D-A$ . Its quadratic form is

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

A weighted graph $\widetilde G$ on $V$ with weights $w(u,v)\ge0$ has the form $x^TL_{\widetilde G}x=\sum_{\{u,v\}}w(u,v)(x(u)-x(v))^2$ . $\widetilde G$ is a $\sigma$ -approximation of $G$ if for all $x$

\tfrac1\sigma\,x^TL_{\widetilde G}x\le x^TL_Gx\le\sigma\,x^TL_{\widetilde G}x .

When every degree is positive, the normalized Laplacian is $\mathcal L_G=D^{-1/2}L_GD^{-1/2}$ ; its eigenvalues lie in $[0,2]$ , and a lower bound $\lambda$ on its smallest non-zero eigenvalue measures how well connected each component of $G$ is (by Cheeger's inequality it is equivalent to high conductance up to squaring).

Sampling. For a parameter $\Upsilon>1$ , edge $(i,j)$ is assigned

p_{i,j}=\min\Big(1,\frac{\Upsilon}{\min(d_i,d_j)}\Big),

each edge is kept independently with probability $p_{i,j}$ , and a kept edge gets weight $1/p_{i,j}$ . The sampled adjacency matrix $\widetilde A$ then has $\mathbf E[\widetilde A]=A$ ; $\widetilde D$ is the diagonal matrix of weighted degrees of the sampled graph.

The procedure. In Theorem 6.1 sampling is applied only to the edges $F$ of an induced subgraph $G(S)$ , $S\subseteq V$ ; the other edges $H=E-F$ are kept with weight 1. $\mathtt{Sample}((S,F),\epsilon,p,\lambda)$ sets $\Upsilon=(12k/(\epsilon\lambda))^2$ and uses the degrees $d_i$ of $G(S)$ ; the paper takes $k=\max(\log_2(3/p),\log_2|S|)$ .

Formalization targets

Goal: Theorem 6.1 (p. 8)

For $\epsilon,p\in(0,1/2)$ , $G$ without isolated vertices whose smallest non-zero normalized Laplacian eigenvalue is at least $\lambda>0$ , $S\subseteq V$ , and an even integer $k\ge\max(\log_2(3/p),\log_2|S|)$ : with probability at least $1-p$ , simultaneously

\text{(S.1)}\ \ \widetilde G=(V,\widetilde F\cup H)\ \text{is a }(1+\epsilon)\text{-approximation of }G,\qquad \text{(S.2)}\ \ |\widetilde F|\le\frac{288\,k^2}{(\epsilon\lambda)^2}\,|S| .

Milestones, in the order the proof uses them

Lemma 6.2 (p. 8): if $\lambda_2(D^{-1/2}LD^{-1/2})\ge\lambda$ and $\|D^{-1/2}(L-\widetilde L)D^{-1/2}\|\le\epsilon<\lambda$ , then $\widetilde G$ is a $\lambda/(\lambda-\epsilon)$ -approximation of a connected $G$ .
Claim 6.5 (p. 13): $|\Delta_{i,j}|\le1/\Upsilon$ for $\Delta=D^{-1}(\widetilde A-A)$ , on every outcome of positive probability.
Lemma 6.6 (p. 13): $\mathbf E[\Delta_{r,t}^k\Delta_{t,r}^l]\le\Upsilon^{-(k+l-1)}d_r^{-1}$ for every edge, $k\ge1$ , $l\ge0$ .
Lemma 6.4 (p. 10): $\mathbf E[\operatorname{Tr}(\Delta^k)]\le nk^k/\Upsilon^{k/2}$ for even $k$ .
Lemma 6.3 (p. 9): $\Pr[\|D^{-1/2}(\widetilde A-A)D^{-1/2}\|\ge 2kn^{1/k}/\sqrt\Upsilon]\le2^{-k}$ for even $k>0$ .
Theorem 6.8 (p. 15, Chernoff bound, cited from Raghavan 1988).
Lemma 6.7 (p. 14): $\Pr[\|D^{-1/2}(D-\widetilde D)D^{-1/2}\|\ge\epsilon]\le2ne^{-\Upsilon\epsilon^2/3}$ for $0<\epsilon<1$ .

Significance

Theorem 6.1 is the sampling engine of the first nearly-linear-time spectral sparsification algorithm: combined with a decomposition of an arbitrary graph into high-conductance pieces (§7–§10 of the paper), it yields sparsifiers with $O(n\log^c n/\epsilon^2)$ edges, which in turn give the nearly-linear-time Laplacian solvers that underlie fast algorithms for electrical flows, maximum flow approximation and graph partitioning. Lemma 6.3 is a self-contained random-matrix result: a norm bound for the normalized deviation of a downsampled graph that does not assume the original graph is dense.

The result is proved in the paper. As far as is known, none of it is formalized in Lean or Mathlib: Mathlib has the graph Laplacian (SimpleGraph.lapMatrix) and the spectral theorem for Hermitian matrices, but no normalized Laplacian, no spectral approximation and no trace-method bounds for random matrices. A complete formalization would be the first machine-checked proof of a spectral sparsification theorem, and the milestones (the trace-method moment bound, Chernoff for weighted two-point sums) are reusable on their own.

Difficulty

The obvious argument — bound each entry of $\widetilde A-A$ and apply a matrix concentration inequality — needs either a matrix Chernoff bound (not in the paper, and not in Mathlib) or the Füredi–Komlós trace method, which assumes every edge can appear and so fails when the graph is already sparse: a vertex of small degree has no room for its entries to average out. The paper's sampling probabilities keep every edge at a vertex of degree at most $\Upsilon$ , and the trace computation has to exploit exactly this through the moment bound of Lemma 6.6 and a combinatorial count of closed walks. Formally, the obstacles are the walk-counting argument of Lemma 6.4, the passage from a trace bound to an eigenvalue bound for the non-symmetric $\Delta$ (similar to a symmetric matrix), and Lemma 6.2's restriction to the orthogonal complement of the kernel, which must handle disconnected $G$ in the goal.

Formalization scope

Vertex sets are finite types V; graphs are SimpleGraph V with decidable adjacency; weighted graphs are weight functions V → V → ℝ (symmetric, nonnegative, loopless). The quadratic form is $\frac12\sum_{u,v}w(u,v)(x(u)-x(v))^2$ ; a $\sigma$ -approximation keeps both inequalities of (2).
The probability space is explicit: an outcome is the set $T$ of kept edges, with probability $\prod_{e\in T}p_e\prod_{e\notin T}(1-p_e)$ ; probabilities and expectations are finite sums. The goal is a probability bound over this law, not the existence of a good set of edges, which would be a much weaker statement.
Eigenvalue conditions are stated with real eigenpairs: "smallest non-zero eigenvalue $\ge\lambda$ " means every eigenvalue $\mu\ne0$ satisfies $\mu\ge\lambda$ ; " $\|M\|\le t$ " (" $\ge t$ ") for symmetric $M$ means every (some) eigenvalue has absolute value $\le t$ ( $\ge t$ ).
Hypotheses made explicit (the paper leaves them implicit): in Theorem 6.1, $k$ is an even integer with $k\ge\log_2(3/p)$ , $k\ge\log_2|S|$ (the proof applies Lemma 6.3 with Sample's $k$ , which the paper defines as a real maximum; the printed statement is the case where that maximum is an even integer), every vertex has degree $\ge1$ , and $\lambda>0$ ; in Lemma 6.2, $0\le\epsilon<\lambda$ ; in Lemma 6.7, $0<\epsilon<1$ (without it the printed bound is false for large $\epsilon$ ); in Lemmas 6.3–6.7 and Claim 6.5, positive degrees; in Lemma 6.3, $k>0$ ; in Theorem 6.8, $\beta>0$ , $\epsilon>0$ , $p_i\in[0,1]$ . $G$ is not assumed connected in Theorem 6.1.
In Theorem 6.1 the probabilities use the degrees of $G(S)$ (the input of $\mathtt{Sample}$ ), while $\lambda$ refers to $G$ ; $n$ in $\mathtt{Sample}$ is $|S|$ .
Trivializing readings ruled out: a one-sided "approximation", a goal that chooses the kept edges existentially, and a spectral hypothesis with $\lambda\le0$ or without positive degrees are all excluded by the statements.
Out of scope: running times, the decomposition algorithms of §7–§10, Cheeger's inequality (Theorem 4.1, cited and not used here), the weighted generalization remarked on p. 10, and the use of Theorem 6.1 in Lemma 9.1.
Contributions welcome: proofs of any milestone; a Loewner-order formulation equivalence; a general matrix Chernoff or trace-method library from which Lemma 6.3 follows.

Selected references

D. A. Spielman, S.-H. Teng, Spectral Sparsification of Graphs, arXiv:0808.4134v3, 2010; SIAM J. Comput. 40(4), 2011. https://arxiv.org/abs/0808.4134
A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
D. Achlioptas, F. McSherry, Fast computation of low rank matrix approximations, STOC 2001. https://doi.org/10.1145/380752.380858
Z. Füredi, J. Komlós, The eigenvalues of random symmetric matrices, Combinatorica 1(3), 1981. https://doi.org/10.1007/BF02579329
V. H. Vu, Spectral norm of random matrices, Combinatorica 27(6), 2007. https://doi.org/10.1007/s00493-007-2190-z
P. Raghavan, Probabilistic construction of deterministic algorithms: approximating packing integer programs, J. Comput. Syst. Sci. 37(2), 1988. https://doi.org/10.1016/0022-0000(88)90003-7
D. A. Spielman, N. Srivastava, Graph sparsification by effective resistances, STOC 2008; arXiv:0803.0929. https://arxiv.org/abs/0803.0929

13 thms2 active usersReviewed

Graph Theory Probability Random Matrix Theory+1·Captain: mikedeng1

Graph Sparsification by Effective Resistances 1: Sampling O(n log n/ε²) Edges by Effective Resistance Yields a (1±ε) Spectral Sparsifier with Probability 1/2Research Paper

Motivation

Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph $G$ is a graph $H$ on the same vertices with far fewer edges that approximates $G$ for the purpose at hand, so that the algorithm can be run on $H$ instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with $O(n\log n/\varepsilon^2)$ edges preserving the weight of every cut up to a factor $1\pm\varepsilon$ . Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had $O(n\log^c n)$ edges for a large constant $c$ and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.

Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of $O(n\log n/\varepsilon^2)$ edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained $O(n/\varepsilon^2)$ edges deterministically, by a slower method built on the same matrix $\Pi$ .

Setting

Let $G=(V,E,w)$ be a connected weighted undirected graph with $n=|V|$ vertices, $m=|E|$ edges and weights $w_e>0$ . Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).

The incidence matrix $B\in\mathbb R^{m\times n}$ has $B(e,v)=1$ if $v$ is the head of $e$ , $-1$ if $v$ is its tail, and $0$ otherwise; $b_e$ denotes its row for $e$ . $W$ is the diagonal $m\times m$ matrix with $W(e,e)=w_e$ .
The Laplacian is $L=B^{\mathsf T}WB$ , with quadratic form $x^{\mathsf T}Lx=\sum_e w_e\,(x(\mathrm{head}\,e)-x(\mathrm{tail}\,e))^2$ .
$L^{+}$ is the Moore–Penrose pseudoinverse of $L$ : if $L=\sum_{i=1}^{n-1}\lambda_iu_iu_i^{\mathsf T}$ over its nonzero eigenvalues, then $L^{+}=\sum_{i=1}^{n-1}\lambda_i^{-1}u_iu_i^{\mathsf T}$ .
The effective resistance of the edge $e$ is $R_e=b_eL^{+}b_e^{\mathsf T}$ : the potential difference across $e$ when a unit current enters at one end and leaves at the other, the edges being resistors of conductance $w_e$ .
$\Pi=W^{1/2}BL^{+}B^{\mathsf T}W^{1/2}$ is an $m\times m$ matrix with $\Pi(e,e)=w_eR_e$ .
Sparsify $(G,q)$ draws $q$ edges independently with replacement, the edge $e$ with probability $p_e=w_eR_e/\sum_f w_fR_f$ , and gives $e$ the weight $w_e/(qp_e)$ for each time it is drawn. Its output $H$ has Laplacian $\tilde L=B^{\mathsf T}W^{1/2}SW^{1/2}B$ , where $S$ is the random diagonal matrix with $S(e,e)=\#\{\text{draws of }e\}/(qp_e)$ .

Formalization targets

Goal: Theorem 1

There are an absolute constant $C$ and a threshold $N_0$ such that, for every $n\ge N_0$ , every connected weighted graph on $n$ vertices and every $1/\sqrt n<\varepsilon\le1$ , with $q=\lceil 9C^2n\log n/\varepsilon^2\rceil$ , with probability at least $1/2$

\forall x\in\mathbb R^n:\qquad (1-\varepsilon)\,x^{\mathsf T}Lx\;\le\;x^{\mathsf T}\tilde Lx\;\le\;(1+\varepsilon)\,x^{\mathsf T}Lx .

The constant $C$ is left unfixed; the statement asserts the shape $q=O(n\log n/\varepsilon^2)$ with the paper's explicit dependence on $C$ .

Milestones

Lemma 3 (four parts): $\Pi$ is an orthogonal projection; $\operatorname{im}\Pi=\operatorname{im}W^{1/2}B$ ; the eigenvalues of $\Pi$ are $1$ with multiplicity $n-1$ and $0$ with multiplicity $m-n+1$ ; $\Pi(e,e)=\|\Pi(\cdot,e)\|^2$ .
Lemma 4: for a nonnegative diagonal $S$ , $\|\Pi S\Pi-\Pi\Pi\|_2\le\varepsilon$ implies $(1-\varepsilon)x^{\mathsf T}Lx\le x^{\mathsf T}B^{\mathsf T}W^{1/2}SW^{1/2}Bx\le(1+\varepsilon)x^{\mathsf T}Lx$ for all $x$ .
Lemma 5 (Rudelson–Vershynin): for independent samples $y_1,\dots,y_q$ of a random vector with $\|y\|_2\le M$ and $\|\mathbb E\,yy^{\mathsf T}\|_2\le1$ , and $q\ge2$ ,

\mathbb E\Big\|\frac1q\sum_{j=1}^q y_jy_j^{\mathsf T}-\mathbb E\,yy^{\mathsf T}\Big\|_2\le CM\sqrt{\frac{\log q}{q}}\quad\text{whenever the right side is }<1.

Significance

Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with $O(n\log n/\varepsilon^2)$ edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to $1\pm\varepsilon$ , effective resistances, and the condition number of $L$ as a preconditioner, so any algorithm whose output depends on these quantities can run on $H$ . Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where $w_eR_e$ is exactly the statistical leverage of a row.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of $\Pi$ (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.

Difficulty

The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of $H$ equals $L$ , but bounding the deviation uniformly over all $x\in\mathbb R^n$ is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of $n$ in the sample count rather than $\log n$ . Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.

Formalization scope

All declarations sit in the namespace EffResSparsify.Sampling.

Graphs. A structure WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes $V\ne\emptyset$ . In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.
Pseudoinverse. $L^{+}$ is the matrix of the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on Euclidean $\mathbb R^V$ ; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of $Lx=y$ ".
Sampling. $p_e$ is defined as $w_eR_e/\sum_f w_fR_f$ ; the identity $\sum_f w_fR_f=n-1$ is part of the proof. An outcome of Sparsify is a sequence in $E^q$ with probability $\prod_i p_{s_i}$ , and probabilities and expectations are finite sums over $E^q$ , with no measure theory.
Norms and logarithms. $\|\cdot\|_2$ is the $\ell_2$ operator norm on matrices (Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; $\log$ is natural (the base is absorbed into $C$ ).
Constants. In Theorem 1, $\exists C>0,\ \exists N_0,\ \forall n\ge N_0$ precede the graph and $\varepsilon$ ; the sample count is $\lceil 9C^2n\log n/\varepsilon^2\rceil$ , rounded up because the printed value is not an integer. In Lemma 5, $\exists C>0$ precedes the dimension, the distribution, $M$ and $q$ .
Corrected statement. Lemma 5 as printed, with right side $\min(CM\sqrt{\log q/q},1)$ , is false (at $q=1$ the bound is $0$ ). The formal milestone is Rudelson and Vershynin's own Theorem 3.1: $q\ge2$ , and the bound $a=CM\sqrt{\log q/q}$ holds when $a<1$ . It is stated for finitely supported distributions, which is all Theorem 1 uses. Theorem 1 applies it with $a\le\varepsilon/2$ , so the correction does not affect the goal.
Not a trivialization. Theorem 1 does not take Lemma 5, a bound on $\mathbb E\|\Pi S\Pi-\Pi\|_2$ , or a free sample count as a hypothesis; a statement with any of these, or with " $\exists q$ " in place of $\lceil 9C^2n\log n/\varepsilon^2\rceil$ , is a different theorem.

Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.

Selected references

D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
M. Rudelson, R. Vershynin, Sampling from large matrices: an approach through geometric functional analysis, J. ACM 54(4), 2007. https://doi.org/10.1145/1255443.1255449
M. Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164(1), 1999. https://doi.org/10.1006/jfan.1998.3384
A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
D. A. Spielman, S.-H. Teng, Spectral sparsification of graphs, SIAM J. Comput. 40(4), 2011 (arXiv:0808.4134). https://arxiv.org/abs/0808.4134
J. Batson, D. A. Spielman, N. Srivastava, Twice-Ramanujan sparsifiers, SIAM J. Comput. 41(6), 2012 (arXiv:0808.0163). https://arxiv.org/abs/0808.0163

9 thms2 active usersReviewed

Completed

Graph Theory Theoretical Computer Science·Captain: mikedeng1

Graph Sparsification by Effective Resistances 2: Approximate Laplacian Solves Preserve Effective-Resistance Sketches up to (1±ε)²Research Paper

Motivation

The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.

Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to $O(\log n)$ dimensions, and the projected vectors are obtained from $O(\log n)$ calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.

Setting

Let $G=(V,E,w)$ be a connected, simple, weighted undirected graph with $n=|V|$ vertices, edge set $E$ and edge weights $w_e>0$ . Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix $B\in\mathbb R^{E\times V}$ has $B(e,v)=1$ if $v$ is the head of $e$ , $-1$ if $v$ is its tail, and $0$ otherwise. With $W$ the diagonal matrix of weights, the Laplacian is $L=B^{\mathsf T}WB$ , a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when $G$ is connected. Its Moore–Penrose pseudoinverse is $L^+=\sum_{\lambda_i\neq 0}\lambda_i^{-1}u_iu_i^{\mathsf T}$ , where $u_i$ are orthonormal eigenvectors of $L$ with nonzero eigenvalues $\lambda_i$ .

For a vertex $u$ let $\chi_u$ be its indicator vector. The effective resistance between $u$ and $v$ is

R_{uv}=(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v),

and $R_e=R_{ab}$ for an edge $e$ with endpoints $a,b$ . The $L$ -norm of $y\in\mathbb R^V$ is $\|y\|_L=\sqrt{y^{\mathsf T}Ly}$ . Let $w_{\min}$ and $w_{\max}$ be the smallest and largest edge weights.

A resistance sketch is a $k\times n$ matrix $Z$ (columns indexed by $V$ ) with

(1-\varepsilon)R_{uv}\le\|Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)R_{uv}\quad\text{for all }u,v,

where $\|\cdot\|$ is the Euclidean norm. In the paper, $Z=QW^{1/2}BL^+$ for a random $\pm1/\sqrt k$ matrix $Q$ with $k=O(\log n/\varepsilon^2)$ , and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write $z_i$ and $\tilde z_i$ for the $i$ -th rows of $Z$ and of an approximation $\widetilde Z$ , as vectors in $\mathbb R^V$ .

Formalization targets

Goal: Lemma 9 (p. 11)

Let $0<\varepsilon<1$ . If $Z$ is a resistance sketch, if every row satisfies

\|z_i-\tilde z_i\|_L\le\delta\|z_i\|_L,\tag{4}

and if

\delta\le\frac{\varepsilon}{3}\sqrt{\frac{2(1-\varepsilon)w_{\min}}{(1+\varepsilon)n^3w_{\max}}},\tag{5}

then for every pair $u,v$

(1-\varepsilon)^2R_{uv}\le\|\widetilde Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)^2R_{uv}.

The lemma is stated for arbitrary $k$ , $Z$ and $\widetilde Z$ : nothing about the random projection or the solver enters beyond (4) and the sketch property.

Milestones

Trace identity (§3, p. 8): $\sum_{e}w_eR_e=n-1$ for a connected graph.
Proposition 10 (p. 12): $R_{uv}\ge 2/(nw_{\max})$ for distinct vertices $u\neq v$ of a connected simple graph.

Significance

Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in $\widetilde O(m\log r/\varepsilon^2)$ time, that returns any effective resistance to within a factor $(1\pm\varepsilon)^2$ in $O(\log n/\varepsilon^2)$ time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.

The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity $\sum_e w_eR_e=n-1$ (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative $L$ -norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.

Difficulty

The hypothesis (4) controls the error row by row, in the $L$ -norm on $\mathbb R^V$ , while the conclusion concerns the columns of $\widetilde Z$ applied to $\chi_u-\chi_v$ , in the Euclidean norm on $\mathbb R^k$ , and it is a relative bound for every pair at once. A relative bound cannot hold unless $R_{uv}$ is bounded below uniformly over all pairs of distinct vertices, which is where the factors $n^3$ , $w_{\min}$ and $w_{\max}$ of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make $R_{uv}$ arbitrarily small, and the relation between the $L$ -norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between $u$ and $v$ .

Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from $(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v)$ ; no theorem relating the two is available.

Formalization scope

The graph is a structure WGraph V E over finite types $V$ (vertices, $n=$ Fintype.card V) and $E$ (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes $V\neq\emptyset$ ); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by $E$ and $V$ . $L^+$ is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on the Euclidean space $\mathbb R^V$ , converted back to a matrix; for symmetric $L$ this is the spectral pseudoinverse of §2.2. $\|Z x\|^2$ is the sum of squares of the coordinates, not Lean's sup norm. $n^3$ is the real number $n^3$ .

Choices committed to, relative to the page:

$w_{\min}$ , $w_{\max}$ are any reals with $0<w_{\min}\le w_e\le w_{\max}$ for all edges; the exact extremes are an instance, and looser bounds only make (5) and Proposition 10 weaker.
$\varepsilon$ is assumed to satisfy $0<\varepsilon<1$ ; the paper gives no range, and for $\varepsilon\ge1$ the square root in (5) has a non-positive argument.
The graph is assumed simple in Lemma 9 and Proposition 10. Proposition 10 is false for multigraphs (two parallel unit edges give $R=1/2<1=2/(nw_{\max})$ ), and the proof of Lemma 9 uses it.
Proposition 10 is stated for $u\neq v$ . As printed it claims all $u,v$ , which fails at $u=v$ since $R_{uu}=0$ .
The trace identity requires connectivity only.

A trivializing formalization is ruled out: the goal does not assume the intermediate inequality $|\|Zx\|-\|\widetilde Zx\||\le(\varepsilon/3)\|Zx\|$ of the proof, nor a stronger condition on $\delta$ than (5); its hypotheses are satisfiable (for example $\widetilde Z=Z$ with $Z=W^{1/2}BL^+$ and $\delta=0$ ), and its conclusion is not vacuous for $n\ge2$ .

Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity $L^+LL^+=L^+$ and $LL^+$ as the projection onto $\mathbf 1^\perp$ for a connected Laplacian; the trace identity; Loewner-order monotonicity of $R_{uv}$ in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.

Selected references

D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems, arXiv:cs/0607105. https://arxiv.org/abs/cs/0607105
D. Achlioptas, Database-friendly random projections: Johnson–Lindenstrauss with binary coins, J. Comput. Syst. Sci. 66(4), 2003. https://doi.org/10.1016/S0022-0000(03)00025-4
P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057

5 thms2 active usersReviewed

Markov Chain·Captain: mikedeng1

Search via Quantum Walk 3: For an Irreducible Chain with Positive Self-Loops the Discriminant diag(π)^{1/2}·P·diag(π)^{−1/2} Has Exactly One Singular Value Equal to 1Research Paper

Motivation

Quantum walks give quadratic speed-ups for a class of search problems that classical algorithms solve by running a Markov chain until it hits a marked state. Ambainis's element-distinctness algorithm (Ambainis 2007) and Szegedy's quantization of reversible Markov chains (Szegedy 2004) are the two starting points. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026v4, SIAM J. Comput. 2011) combined them into one search algorithm whose cost is governed by the eigenvalue gap of a reversible chain $P$ .

For a non-reversible chain the relevant spectral quantity is not the eigenvalue gap of $P$ . It is the singular value gap of a related matrix, the discriminant $D(P)$ . In §5 the paper observes that its search algorithm and the proof of its main theorem carry over to non-reversible chains once the eigenvalue gap of $P$ is replaced by the singular value gap of $D(P)$ . Positivity of that gap therefore decides whether the algorithm can be used at all. The paper also notes that irreducibility, and even ergodicity, does not guarantee a positive gap. Its Proposition 3 (p. 17, proved in the appendix on pp. 20–21) gives a simple sufficient condition: every state has a positive probability of staying where it is. This mission formalizes that proposition.

Setting

Let $X$ be a finite set of states. A Markov chain on $X$ is a real matrix $P=(p_{xy})_{x,y\in X}$ with nonnegative entries whose rows sum to one; $p_{xy}$ is the probability of moving from $x$ to $y$ . The graph underlying $P$ has an edge $x\to y$ whenever $p_{xy}>0$ . The chain is irreducible if this graph is strongly connected, so that every state can be reached from every other state.

A stationary distribution of $P$ is a vector $\pi=(\pi_x)_{x\in X}$ with

\pi_x>0,\qquad \sum_x \pi_x=1,\qquad \sum_x \pi_x p_{xy}=\pi_y\quad(y\in X).

Every irreducible chain has exactly one.

The discriminant of $P$ is the matrix

D(P)=\operatorname{diag}(\pi)^{1/2}\cdot P\cdot \operatorname{diag}(\pi)^{-1/2},\qquad D(P)_{xy}=\frac{\sqrt{\pi_x}\,p_{xy}}{\sqrt{\pi_y}},

viewed as an operator on $\mathbb C^X$ with the inner product $\langle u,w\rangle=\sum_x\overline{u_x}w_x$ . Its singular values $\sigma_0\ge\sigma_1\ge\dots\ge\sigma_{|X|-1}\ge 0$ are the square roots of the eigenvalues of $D(P)^\dagger D(P)$ , repeated according to multiplicity. The vector $v=(\sqrt{\pi_x})_{x\in X}$ satisfies $D(P)v=v$ and $v^{\mathsf T}D(P)=v^{\mathsf T}$ , so $1$ is always a singular value of $D(P)$ . When $P$ is reversible, $D(P)$ is symmetric and its singular values are the absolute values of the eigenvalues of $P$ . In general the two can differ.

Formalization targets

Goal: Proposition 3

If $P$ is an irreducible Markov chain on a finite state space $X$ with $p_{xx}>0$ for every $x$ , then $D(P)$ has exactly one singular value equal to $1$ :

\#\{\,i<|X|:\ \sigma_i(D(P))=1\,\}=1 .

Together with the bound below, this says that $1=\sigma_0>\sigma_1$ , i.e. the singular value gap $1-\sigma_1$ is positive. The goal asserts no explicit lower bound on the gap, so it does not depend on any quantitative estimate.

Milestones, in the order the proof uses them

Eq. (9). For unit vectors $u,v\in\mathbb C^X$ ,

|u^\dagger D(P)v|\le\Bigl(\sum_{x,y}|u_x|^2p_{xy}\Bigr)^{1/2}\Bigl(\sum_{x,y}|v_y|^2\tfrac{\pi_x}{\pi_y}p_{xy}\Bigr)^{1/2}\le 1 .

Lemma 3. Every singular value of $D(P)$ lies in $[0,1]$ .
§5, p. 17. $v=(\sqrt{\pi_x})$ is a left and right eigenvector of $D(P)$ with eigenvalue $1$ .
Equality case. If $u,w$ are unit vectors with $u^\dagger D(P)w=1$ , then $u_x=w_y\sqrt{\pi_x/\pi_y}$ whenever $p_{xy}>0$ .
Path chaining. If $u_y=u_x\sqrt{\pi_y/\pi_x}$ along every edge $x\to y$ and $P$ is irreducible, then $u_y=u_{x_1}\sqrt{\pi_y/\pi_{x_1}}$ for all $x_1,y$ .

Significance

The result. Proposition 3 is what makes the search algorithm of the paper usable with non-reversible chains. Theorem 8 of the paper bounds the cost of finding a marked element in terms of the singular value gap of $D(P)$ , and it needs that gap to be positive. The hypothesis $p_{xx}>0$ costs little: replacing $P$ by $\alpha I+(1-\alpha)P$ for any $\alpha\in(0,1)$ makes every self-loop positive and keeps the stationary distribution. The proposition also connects to the classical study of non-reversible chains: the squared singular values of $D(P)$ are the eigenvalues of the multiplicative reversiblization $PP^*$ , which Fill (1991) used to bound convergence to stationarity.

Formalizing it. The proposition and its proof are in the paper and are not in dispute. To our knowledge neither is machine-checked anywhere. The work is a formal proof of the known argument. It exercises Mathlib's recently added singular values of linear maps between finite-dimensional inner product spaces and its theory of irreducible nonnegative matrices, in a setting where the matrix is neither symmetric nor normal.

Difficulty

The obvious route goes through eigenvalues. Irreducibility plus self-loops make $P$ aperiodic, so by Perron–Frobenius the eigenvalue $1$ of $P$ is simple and every other eigenvalue has modulus less than $1$ . This does not settle the question. The singular values of a non-normal matrix are not the moduli of its eigenvalues, and the paper points out ergodic chains whose discriminant has zero singular value gap even though their eigenvalue gap is positive. Simplicity of the eigenvalue $1$ of $P$ therefore says nothing about the multiplicity of the singular value $1$ of $D(P)$ .

The real content is the equality case of a Cauchy–Schwarz inequality in $\mathbb C^{X\times X}$ . It has to be translated into an edge-by-edge relation between the coordinates of the left and right singular vectors, then propagated along directed paths of the chain's graph. The self-loops are what identify the left and right singular vectors with each other. Bookkeeping that is routine on paper costs effort here: passing between the eigenvalue sequence of $D(P)^\dagger D(P)$ and the dimension of its $1$ -eigenspace, and between paths in Mathlib's quiver of positive entries and chains of equalities.

Formalization scope

States and chain. The state space is a Fintype with decidable equality. $P$ is a real matrix in Matrix.rowStochastic ℝ X, and irreducibility is Mathlib's Matrix.IsIrreducible (nonnegative entries and a strongly connected quiver with an edge $x\to y$ iff $p_{xy}>0$ ). For a row-stochastic matrix this agrees with "every state is reachable from every other state".
Stationary distribution. It enters as data $\pi$ with the three properties above. Positivity is explicit because $\operatorname{diag}(\pi)^{-1/2}$ needs it. Existence and uniqueness (Perron–Frobenius) are neither needed nor stated.
Discriminant. $D(P)$ is the complex matrix with entries $\sqrt{\pi_x}p_{xy}/\sqrt{\pi_y}$ , acting on EuclideanSpace ℂ X. Its singular values are Mathlib's LinearMap.singularValues, a sequence indexed by $\mathbb N$ that is $0$ beyond $|X|$ . The goal counts the indices $i<|X|$ with $\sigma_i=1$ . The inner product $u^\dagger D(P)w$ is Mathlib's inner ℂ u (D(P) w). Since the equality-case milestone assumes this equals $1$ exactly, no phase ambiguity remains.
What is not assumed. Reversibility of $P$ is not assumed. Neither is aperiodicity, primitivity, or a "lazy" bound $p_{xx}\ge 1/2$ : the hypothesis is exactly $p_{xx}>0$ for every $x$ .
Ruled-out trivializations. " $1$ is a singular value of $D(P)$ " holds for every chain and is not the goal. The goal is that this singular value has multiplicity one. A conclusion such as "some singular value is $<1$ " would also be too weak.
Cost. The paper's search algorithm and its cost bounds (Theorem 8) are out of scope. This mission is purely linear-algebraic.
Welcome contributions. Proofs of the milestones. The path-chaining milestone is a reusable fact about functions that are multiplicative along the edges of a strongly connected quiver. A general lemma relating the multiplicity of a singular value to the dimension of an eigenspace of $T^\dagger T$ would be useful well beyond this mission.

Selected references

F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1):142–164, 2011; arXiv:quant-ph/0608026v4. https://arxiv.org/abs/quant-ph/0608026 (DOI 10.1137/090745854)
M. Szegedy, Quantum speed-up of Markov chain based algorithms, Proc. 45th IEEE FOCS, 32–41, 2004. https://doi.org/10.1109/FOCS.2004.53
A. Ambainis, Quantum walk algorithm for element distinctness, SIAM J. Comput. 37(1):210–239, 2007; arXiv:quant-ph/0311001. https://arxiv.org/abs/quant-ph/0311001
J. A. Fill, Eigenvalue bounds on convergence to stationarity for nonreversible Markov chains, with an application to the exclusion process, Ann. Appl. Probab. 1(1):62–87, 1991. https://doi.org/10.1214/aoap/1177005981

7 thms2 active usersReviewed

Quantum Information·Captain: marwahaha

Entanglement with zero distillable secret key in local dimension tenOpen Problem

Motivation

Positive partial transpose imposes strong constraints on quantum maps, but composition may retain entanglement. Explicit finite-dimensional examples make that distinction a precise algebraic target. The pinned manuscript supplies the research context.

Setting

The selected maps act on complex 10 by 10 matrices. Complete positivity is quantified over matrix amplifications, while separability is expressed by finite sums of positive tensor factors.

Formalization target

The selected goal is OAI.DimensionTen.main_pair. Its central assertion is

\Phi_1=\mathrm{phiOne},\quad\Phi_2=\mathrm{phiTwo},\quad\neg\mathrm{EB}(\Phi_2\circ\Phi_1).

The theorem states that there exist maps Φ₁ and Φ₂ from 10×10 complex matrices to 10×10 complex matrices, equal to the defined maps phiOne and phiTwo, each of which is PPT, meaning complex-linear, completely positive, and such that composing with the transpose of the output is also completely positive (complete positivity means that applying the map to one factor of any positive semidefinite block matrix on ℂᵏ⊗ℂ¹⁰, for every k≥1, yields a positive semidefinite matrix). Here phiOne sends A to the 6×6 matrix obtained from the transpose of A by embedding it as a symmetric tensor in ℂ⁴⊗ℂ⁴, applying the tensor square of an explicit 4×4 pencil map built from four integer 6×4 blocks, and compressing to the antisymmetric subspace, then padding it to a 10×10 matrix in the first six coordinates. phiTwo is the Hilbert–Schmidt adjoint of an associated complementary map, which uses a Hodge-type complement matrix, applied to the compression of its input onto the first six coordinates. Moreover, letting Z be the Choi matrix of the composition Φ₂∘Φ₁, a 100×100 matrix with entries given by the images of the matrix units, Z is nonzero; no nonzero product vector u⊗v with u,v∈ℂ¹⁰ lies in the range of Z, that is, whenever Z applied to some w∈ℂ¹⁰ˣ¹⁰ equals u⊗v then u=0 or v=0; and Φ₂∘Φ₁ is not entanglement breaking, where entanglement breaking means completely positive and sending every positive semidefinite amplification to a separable matrix, a finite sum of Kronecker products of positive semidefinite matrices. This theorem is admitted in the source, not proved.

Significance and status

The selected target is the explicit pair of PPT maps in dimension ten, including its nonzero Choi matrix and product-vector obstruction. It does not state a secret-key distillation theorem. The separate 21-dimensional channel is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

PPT properties and non-entanglement-breaking composition require different certificates. The range condition must exclude every nonzero product vector.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

OAI.DimensionTen.exists_channel_fin21 (Open).

Selected references

OpenAI, Entanglement with zero distillable secret key in local dimension ten, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

9 thms2 active usersReviewed

Quantum Information·Captain: marwahaha

Exact Fourier certificates for complex Hadamard matrices of order sixOpen Problem

Motivation

Character sums express phase constraints on complex Hadamard matrices. In dimension six these constraints also bear on how many mutually unbiased bases can coexist. The pinned manuscript supplies the research context.

Setting

A complex Hadamard matrix has unit-modulus entries and conjugate-transpose product 6I. Equivalence permits row and column permutations and unit phases. Tao's cubic matrix supplies the exceptional class.

Formalization target

The selected goal is OAI.MUB6.fourier_and_family_bound. Its central assertion is

g_H(\pi(1,1,1,-1,-1,-1))=0,\qquad n_{\rm MUB}\leq5.

The theorem states a conjunction of two claims about 6x6 complex matrices and mutually unbiased bases in C^6. First, for every complex Hadamard matrix H of order 6 (all entries of modulus 1 and HH = 6I, where H is the conjugate transpose) that is not equivalent to the specific matrix tao, every permutation π of the six coordinates gives g(H, alpha∘π) = 0. Here the character of a column x at an integer exponent vector a is the product over i of x_i^{a_i}, g(H,a) is (1/6) times the sum over the six columns k of H of the character of column k at a, and alpha is the exponent vector (1,1,1,-1,-1,-1), so alpha∘π is alpha with its entries permuted. Equivalence of H and K means K_{ij} = u_i H_{r(i),c(j)} v_j for some row and column permutations r, c and unit-modulus complex phase vectors u and v. The matrix tao has entries ω^{e_{ij}}, where ω = exp(2πi/3) and e is a fixed 6x6 exponent matrix with zero first row and column and a five-cycle pattern of exponents 0, 1, 2 in the remaining 5x5 block. Second, for every natural number n, if there exist n orthonormal bases of C^6 that are pairwise mutually unbiased, meaning |<b_i, b'_j>|^2 = 1/6 for all vectors of two distinct bases, then n ≤ 5. This is stated as an admitted theorem, not a verified proof.

Significance and status

The goal is the conjunction of Fourier vanishing outside the specified equivalence class and the bound on attainable families. The cube-fiber statement is an additional published supporting target with its own hypotheses. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Orthogonality immediately kills certain degree-two characters, but the target concerns a balanced degree-six character and a separate global bound on families of bases.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

OAI.HadamardSix.rowRatio_cubeFiber_sum_zero (Open).

Selected references

OpenAI, Exact Fourier certificates for complex Hadamard matrices of order six, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

7 thms2 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion 4: The Estimator Never Overestimates rank(A₀), Recovers It Above a Singular-Value Gap, and Obeys a Matching Lower BoundResearch Paper

Motivation

Noisy low-rank matrix completion asks to reconstruct an $m_1\times m_2$ matrix $A_0$ from $n$ noisy observations of randomly chosen entries. It is the statistical model behind collaborative filtering (recommender systems), sensor localization and system identification, and the nuclear-norm penalized least-squares estimator is its standard convex method. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4, Ann. Statist. 2011) proved sharp oracle inequalities for this estimator and showed that its Frobenius error is of order $\operatorname{rank}(A_0)(m_1\vee m_2)\log(m_1+m_2)/n$ up to normalization, which matches the minimax lower bound up to a logarithmic factor.

An upper bound alone does not say whether the estimator really attains this rate on a given matrix, nor whether it reports the correct rank. Section 5.1 of the paper answers both questions with a single deterministic theorem, Theorem 8: with a slightly inflated regularization parameter the estimator never overestimates the rank of $A_0$ ; if the nonzero singular values of $A_0$ are separated from zero it recovers the rank exactly, and its error is then bounded below by a quantity of the same order as the upper bounds. Rank recovery is the property practitioners rely on when they use the estimator for model selection (choosing the number of latent factors). This mission formalizes Theorem 8 and the steps of its proof.

Setting

Fix integers $m_1,m_2,n\ge1$ . The matrix completion basis is $\mathcal X=\{e_j(m_1)e_k(m_2)^\top\}$ , the $m_1m_2$ matrices with a single entry equal to $1$ . A sample consists of $n$ pairs $(X_i,Y_i)$ with $X_i\in\mathcal X$ (an observed position $(j_i,k_i)$ ) and $Y_i\in\mathbb R$ (a noisy observation of the corresponding entry of the unknown matrix $A_0$ ). Write $\langle A,B\rangle=\operatorname{tr}(A^\top B)$ , $\|A\|_2$ for the Frobenius norm, $\|A\|_1$ for the nuclear norm (the sum of the singular values) and $\|A\|_\infty$ for the operator norm (the largest singular value). The singular values of $B$ are $\sigma_1(B)\ge\sigma_2(B)\ge\dots\ge\sigma_{m_1\wedge m_2}(B)\ge0$ .

From the sample form

\mathbf X=\frac{m_1m_2}{n}\sum_{i=1}^nY_iX_i,\qquad \mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).

In the paper's model $\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle$ with $X_i$ uniform on $\mathcal X$ , so $\mathbb E(Y_iX_i)=A_0/(m_1m_2)$ and $\mathbf X-A_0=m_1m_2\mathbf M$ : the matrix $\mathbf M$ is the stochastic error. For $\lambda>0$ the estimator (3.1) is

\hat A^\lambda=\operatorname{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1\Big).

The objective is strictly convex, so the minimizer is unique; by (3.2) it is obtained from a singular value decomposition of $\mathbf X$ by soft thresholding every singular value at level $\lambda m_1m_2/2$ .

Formalization targets

Goal: Theorem 8 (p. 20)

Let $\lambda\ge2\|\mathbf M\|_\infty$ , $0<\delta<1$ and $\lambda'=\lambda/(1-\delta)$ , and put $\hat r=\operatorname{rank}(\hat A^{\lambda'})$ . Then

\hat r\le\operatorname{rank}(A_0).\tag{5.1}

If in addition $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ , then

\hat r\ge\operatorname{rank}(A_0)\tag{5.2}

and

\|\hat A^{\lambda'}-A_0\|_2^2\ge\frac{\delta^2}{4(1-\delta)^2}\operatorname{rank}(A_0)\,(\lambda m_1m_2)^2.\tag{5.3}

Milestones

The milestones follow the proof on p. 20 in order:

the singular value perturbation display $|\sigma_j(\mathbf X)-\sigma_j(A_0)|\le\sigma_1(\mathbf X-A_0)=m_1m_2\|\mathbf M\|_\infty\le\lambda m_1m_2/2$ ;
the rank of $\hat A^\lambda$ equals the number of singular values of $\mathbf X$ above $\lambda m_1m_2/2$ (the consequence of (3.2) the proof uses);
(5.1);
(5.2);
$\|\mathcal P(\hat A^{\lambda'}-\mathbf X)\|_2=\sqrt r\,\lambda'm_1m_2/2$ when $\hat r=r$ , for the projector $\mathcal P$ onto the span of the top $r$ singular pairs $u_j(\mathbf X)v_j(\mathbf X)^\top$ ;
$\|\mathcal P(\mathbf X-A_0)\|_2\le\sqrt r\|\mathbf M\|_\infty m_1m_2\le\sqrt r\lambda m_1m_2/2$ .

Significance

The result. Theorem 8 turns the paper's upper bounds into two-sided statements. Combined with a probability bound for $\|\mathbf M\|_\infty$ (Corollary 3 of the paper), it shows that with high probability the estimator selects the true rank and that its error on well-conditioned low-rank matrices is not smaller than the rate of the upper bounds, so those bounds cannot be improved for this estimator. Because the theorem is deterministic given the event $\lambda\ge2\|\mathbf M\|_\infty$ , it applies unchanged to any noise model for which such a bound on the stochastic error is available.

Formalizing it. The theorem is proved in the paper; nothing in it is open. The mission produces a machine-checked version and, along the way, reusable linear algebra that is not on the platform in this form: Weyl's perturbation inequality for singular values in operator norm, the rank of a nuclear-norm proximal point, and the Frobenius norm of a projection onto a span of orthonormal rank-one matrices. The soft-thresholding representation (3.2) itself is the open platform item CaiCandesShen.Convergence.shrink_eq_prox (Cai–Candès–Shen, Theorem 2.1, after halving the objective); this mission references it rather than posing it again, and a proof of it would serve both missions.

Difficulty

The arithmetic of the proof is three lines; the content is in two facts about singular values that the paper takes from the literature. The first is Weyl's inequality $|\sigma_j(B)-\sigma_j(C)|\le\|B-C\|_\infty$ , which needs the min–max (Courant–Fischer) characterization of singular values; Mathlib defines singular values through the eigenvalues of $T^*T$ but has neither the min–max principle for them nor this inequality. The second is the description of the minimizer of $\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1$ : one needs the subdifferential of the nuclear norm (2.1), or an equivalent von Neumann trace inequality, to show that soft thresholding is optimal, and then that its rank and its projection onto the top singular pairs are what the formula suggests. A naive approach that compares the estimator with $\mathbf X$ entrywise gives nothing about the rank; the proof needs the spectral structure.

Formalization scope

Matrices are MatrixCompletion.RealMatrix m₁ m₂ (Matrix (Fin m₁) (Fin m₂) ℝ) with the published norms frobeniusNormSq, frobeniusNorm, nuclearNorm, spectralNorm and SVD data SVD. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin, 0-based: the Lean singularValue B j is the paper's $\sigma_{j+1}(B)$ . The conventions committed to:

The statements are realization-wise: positions idx : Fin n → Fin m₁ × Fin m₂ and responses y : Fin n → ℝ are fixed, and every theorem holds for every data set satisfying $\lambda\ge2\|\mathbf M\|_\infty$ . The matrix $\mathbf M$ is written as $\frac1n\sum_iY_iX_i-A_0/(m_1m_2)$ , which is (2.2) under the model (1.1) and the uniform design; this is the paper's "Note that $\mathbf X-A_0=m_1m_2\mathbf M$ ". The probabilistic hypotheses are used for nothing else.
$n,m_1,m_2\ge1$ and $\lambda>0$ are assumed, as in the paper.
The estimator is any minimizer of (3.1) over all matrices, never the soft-thresholding formula; replacing the minimizer by formula (3.2) would assume the open Cai–Candès–Shen item.
$\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ is written "for every $j$ with $\sigma_j(A_0)\ne0$ "; for $A_0=0$ it is vacuous, as on the page. No real infimum over a possibly empty set is used.
The projector $\mathcal P$ is built from a singular value decomposition of $\mathbf X$ carried as data, with decreasing singular values, from its first $r$ pairs.

No printed slip was found in Theorem 8 or its proof; no hypothesis beyond the above is added.

Contributions welcome: Weyl's inequality for singular values (generally useful), the rank and top- $r$ projection of the nuclear-norm proximal point, and a proof of CaiCandesShen.Convergence.shrink_eq_prox.

The source is the arXiv preprint arXiv:1011.6256v4; all page and display numbers refer to it.

Selected references

V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://doi.org/10.1137/080738970
G. W. Stewart, J.-G. Sun, Matrix Perturbation Theory, Academic Press, 1990 (reference [25] of the paper, p. 203).
E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Flows and Decompositions of Games: Harmonic and Potential Games 5: Every ϵ-Equilibrium of the Closest Potential Game Is an (ϵ + max_m 2α/√h_m)-Equilibrium of the Game, and ConverselyResearch Paper

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.

Setting

A finite game has a finite set of players $\mathcal M$ ; each player $m$ has a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements, and a utility $u^m : E \to \mathbb R$ on the set of strategy profiles $E = \prod_m E^m$ . For a profile $p$ , $(q^m, p^{-m})$ denotes $p$ with player $m$ 's strategy replaced by $q^m$ .

A profile $p$ is an $\epsilon$ -equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m}) - \epsilon$ for every player $m$ and strategy $q^m$ (equation (2) of the paper). A game is a potential game if there is $\varphi : E \to \mathbb R$ with $\varphi(p^m, p^{-m}) - \varphi(q^m, p^{-m}) = u^m(p^m, p^{-m}) - u^m(q^m, p^{-m})$ for all $m$ , $p^m$ , $q^m$ , $p^{-m}$ (Definition 2.1).

A game is identified with its tuple of utilities, an element of $C_0^M$ where $C_0 = \{f : E \to \mathbb R\}$ . The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator $D_m$ sends $u^m$ to its differences along the edges where player $m$ deviates, $D = \sum_m D_m$ , $\delta_0$ is the gradient of the game graph, $\Pi_m = D_m^\dagger D_m$ , and $\dagger$ is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces

\mathcal P = \{u = \Pi u,\ Du \in \operatorname{im}\delta_0\},\qquad \mathcal H = \{u = \Pi u,\ Du \in \ker\delta_0^*\},\qquad \mathcal N = \ker D ,

and a harmonic game is a game in $\mathcal H \oplus \mathcal N$ .

Section 6 introduces the weighted inner product and norm

\langle G, \hat G\rangle_{M,E} = \sum_{m} h_m \sum_{p \in E} u^m(p)\,\hat u^m(p), \qquad \|G\|_{M,E}^2 = \langle G, G\rangle_{M,E} .

A closest potential game to $G$ is a potential game $\hat G$ with $\|G - \hat G\|_{M,E} \le \|G - G'\|_{M,E}$ for every potential game $G'$ ; a closest harmonic game is defined in the same way.

Formalization targets

Goal: Theorem 6.3

Let $\hat G$ be the closest potential game to $G$ and $\alpha = \|G - \hat G\|_{M,E}$ . Then for every $\epsilon_1$ , every $\epsilon_1$ -equilibrium of $\hat G$ is an $\epsilon$ -equilibrium of $G$ , and every $\epsilon_1$ -equilibrium of $G$ is an $\epsilon$ -equilibrium of $\hat G$ , where

\epsilon = \max_{m \in \mathcal M} \frac{2\alpha}{\sqrt{h_m}} + \epsilon_1 .

Milestones

Lemma 2.1. If $|u^m(p) - \hat u^m(p)| \le \epsilon_0$ for all $m$ and $p$ , every $\epsilon_1$ -equilibrium of one game is a $(2\epsilon_0 + \epsilon_1)$ -equilibrium of the other.
Theorem 5.1. The set of potential games is the subspace $\mathcal P \oplus \mathcal N$ .
Theorem 6.1. Under $\langle\cdot,\cdot\rangle_{M,E}$ the subspaces $\mathcal P$ , $\mathcal H$ , $\mathcal N$ are pairwise orthogonal.
Theorem 6.2. With $\varphi = \delta_0^\dagger D u$ , the closest potential game to $G$ has utilities $\Pi_m \varphi + (I - \Pi_m)u^m$ , and the closest harmonic game has utilities $u^m - \Pi_m\varphi$ .

Significance

The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.

Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections $\Pi_m$ ), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for $\epsilon$ -equilibria.

Difficulty

Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into $\mathcal P$ , $\mathcal H$ , $\mathcal N$ ) and properties of pseudoinverses of the operators $D_m$ and $\delta_0$ that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality $\mathcal P \perp \mathcal H$ under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the $h_m$ differ, so the standard orthogonal-complement machinery cannot be applied to $C_0^M$ with its default inner product.

Formalization scope

Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product $\tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$ of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.

Hypotheses made explicit: every strategy set is nonempty (the paper's $E^m = \{1,\dots,h_m\}$ ), so $h_m \ge 1$ ; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an $\epsilon$ -equilibrium for some $\epsilon \le B$ " is stated as "a $B$ -equilibrium", which is equivalent because (2) is monotone in $\epsilon$ . Both directions of Lemma 2.1 and Theorem 6.3 are included.

The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance $\alpha$ would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.

Contributions welcome: the Penrose identities for the pseudoinverse, the identities $D^\dagger D = \Pi$ and $\Delta_{0,m} = h_m \Pi_m$ , and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.

Selected references

O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Math. Oper. Res. 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
D. Monderer, L. S. Shapley, Potential Games, Games Econ. Behav. 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044

14 thms2 active usersReviewed

Convex Optimization Numerical Analysis·Captain: mikedeng1

Low-rank Matrix Recovery via Iteratively Reweighted Least Squares Minimization 2: A Rank Restricted Isometry Constant δ_4k < √2 − 1 Implies the Strong Rank Null Space Property of Order kResearch Paper

Motivation

Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem $\min \operatorname{rank}(X)$ subject to $\mathcal S(X) = \mathcal M$ is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization $\min \|X\|_*$ subject to $\mathcal S(X) = \mathcal M$ or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).

Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that $\mathcal S$ nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of $\mathcal S$ be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.

Timeline.

2005: Candès and Tao introduce restricted isometry constants for sparse vectors and prove exact recovery by $\ell_1$ minimization under a condition on them (IEEE Trans. Inf. Theory).
2008: Candès shows that $\delta_{2s} < \sqrt 2 - 1$ suffices in the vector case (C. R. Math.).
2010: Recht, Fazel and Parrilo define the rank restricted isometry property and prove that nuclear-norm minimization recovers every rank- $r$ matrix when $\delta_{5r}$ is small enough (SIAM Review).
2011: Candès and Plan prove the matrix analogue of the $\sqrt 2 - 1$ threshold and the orthogonality estimate quoted here as Lemma 6.9 (IEEE Trans. Inf. Theory).
2011: Fornasier, Rauhut and Ward prove Proposition 6.8, the target of this mission: $\delta_{4k} < \sqrt 2 - 1$ implies the SRNSP of order $k$ .

Setting

Fix integers $n, p, m$ . A measurement map is a linear map $\mathcal S : \mathbb R^{n\times p} \to \mathbb R^m$ ; it is given by $m$ matrices $A_1,\dots,A_m$ through $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$ , where $\langle X, Y\rangle = \operatorname{Tr}(XY^{\top}) = \sum_{i,j} X_{ij}Y_{ij}$ . The Frobenius norm is $\|X\|_F = \langle X, X\rangle^{1/2}$ , the nuclear norm $\|X\|_*$ is the sum of the singular values of $X$ , and $\|\mathcal S(X)\|_{\ell_2^m}$ is the Euclidean norm of the vector $\mathcal S(X)$ . A matrix is $k$ -rank if its rank is at most $k$ .

The restricted isometry constant $\delta_k = \delta_k(\mathcal S)$ (Definition 1.1) is the smallest $\delta \ge 0$ such that

(1 - \delta)\|X\|_F^2 \le \|\mathcal S(X)\|_{\ell_2^m}^2 \le (1+\delta)\|X\|_F^2 \qquad \text{for all $k$-rank } X .

The map $\mathcal S$ has the strong rank null space property of order $k$ with constant $\eta \in (0,1)$ (Definition 6.4) if for every $X \in \ker \mathcal S \setminus\{0\}$ and every decomposition $X = X_1 + X_2$ with $X_1$ $k$ -rank, there is another decomposition $X = H_1 + H_2$ with $\operatorname{rank} H_1 \le 2k$ , $\langle H_1, H_2\rangle = 0$ , $X_1H_2^{\top} = 0$ , $X_1^{\top}H_2 = 0$ , and

\|H_1\|_* \le \eta\,\|H_2\|_* .

In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X $= \|\mathcal S(X)\|^2_{\ell_2^m}$ , built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).

Formalization targets

Goal: Proposition 6.8

If $\delta_{4k} > 0$ and

\delta_{4k} < \sqrt 2 - 1,

then $\mathcal S$ satisfies the SRNSP of order $k$ with constant

\eta = \sqrt 2\,\frac{\delta_{4k}}{1 - \delta_{3k}} \in (0,1).

The constant $\eta$ is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including $\eta \in (0,1)$ .

Milestones

Lemma 6.9 (Candès–Plan): for $\langle X, Y\rangle = 0$ and $\operatorname{rank}X + \operatorname{rank}Y \le k$ , $|\langle \mathcal S(X), \mathcal S(Y)\rangle| \le \delta_k \|X\|_F\|Y\|_F$ .
Lemma 6.10 (Recht–Fazel–Parrilo): $XZ^{\top} = 0$ and $X^{\top}Z = 0$ imply $\|X + Z\|_* = \|X\|_* + \|Z\|_*$ .
The block decomposition of the proof: relative to an SVD $X_1 = U(\begin{smallmatrix}\Sigma & 0\\ 0 & 0\end{smallmatrix})V^{\top}$ , the matrices $H_0$ and $H_c$ obtained by zeroing blocks of $U^{\top}XV$ satisfy $X = H_0 + H_c$ , $\operatorname{rank}H_0 \le 2k$ , $X_1H_c^{\top} = 0$ , $X_1^{\top}H_c = 0$ , $\langle H_0, H_c\rangle = 0$ .
$\|H\|_* \le \sqrt r\,\|H\|_F$ for $\operatorname{rank}H \le r$ , and $\|H\|_F \le \|H + K\|_F$ for $\langle H, K\rangle = 0$ .
The shelling bound: for a nonincreasing nonnegative sequence cut into blocks of length $\ell$ , each block's $\ell_2$ norm is at most $\ell^{-1/2}$ times the $\ell_1$ norm of the previous block.
Monotonicity $\delta_k \le \delta_{k'}$ for $k \le k'$ , and $\eta \in (0,1)$ under $0 < \delta_{4k} < \sqrt2 - 1$ .

Significance

The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once $m$ is of order $k\max(n,p)$ ) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every $k$ -rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best $k$ -rank approximation error in the nuclear norm.

Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.

Difficulty

The obvious argument would bound $\|H_1\|_*$ directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element $X$ has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to $X$ , or to $H_2$ , as a whole, and the constant $\eta$ depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.

Formalization scope

Real matrices Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. $X^*$ is $X^{\top}$ and $\langle\cdot,\cdot\rangle$ is traceInner.
Measurement map by matrices: $\mathcal S(X)_\ell = \langle A_\ell, X\rangle$ (observationOp); $\|\mathcal S(X)\|^2_{\ell_2^m}$ is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.
The squared RIP constant of Definition 1.1, defined as the infimum of the admissible $\delta \ge 0$ (attained, never a junk value), for every $k \in \mathbb N$ ; the page's range $1 \le k \le n$ is dropped because the goal uses $\delta_{4k}$ with $4k$ possibly larger than $n$ . The unsquared constant $(1-\delta)\|X\|_F \le \|\mathcal S(X)\| \le (1+\delta)\|X\|_F$ used by other formalizations is a different quantity and is not used.
Positivity $\delta_{4k} > 0$ is a hypothesis of the goal: it is Definition 1.1's own " $\delta_k > 0$ ", and without it $\eta = 0 \notin (0,1)$ .
No n ≤ p assumption: the proof does not use it.
The block decomposition milestone states the page's explicit construction, with a general (not necessarily diagonal) top-left block, and without the unused hypothesis $X \in \ker\mathcal S$ .
The shelling bound is stated in its vector form for every block; the page writes "for $j \ge 2$ " but display (6.7) uses it for every $j \ge 1$ .

A formalization that proved only $\eta < 1$ , or only the existence of some decomposition without the bound $\|H_1\|_* \le \eta\|H_2\|_*$ , or that defined $\delta_k$ as any admissible constant rather than the smallest one, would not be this mission's goal.

Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.

Selected references

M. Fornasier, H. Rauhut, R. Ward, Low-rank matrix recovery via iteratively reweighted least squares minimization, SIAM J. Optim. 21(4), 2011; read as arXiv:1010.2471v4. https://arxiv.org/abs/1010.2471
E. J. Candès, Y. Plan, Tight oracle inequalities for low-rank matrix recovery from a minimal number of noisy random measurements, IEEE Trans. Inf. Theory 57(4), 2011. https://doi.org/10.1109/TIT.2011.2111771
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835
E. J. Candès, T. Tao, Decoding by linear programming, IEEE Trans. Inf. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Math. Acad. Sci. Paris 346, 2008. https://doi.org/10.1016/j.crma.2008.03.014

11 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

The Primal-Dual Active Set Strategy as a Semismooth Newton Method II: Global Convergence and Monotonicity for M-MatricesResearch Paper

Motivation

Obstacle problems, contact problems and box-constrained quadratic programs share one finite-dimensional core: the linear complementarity problem "find $y \le \psi$ and $\lambda \ge 0$ with $Ay + \lambda = f$ and $\lambda_i(y_i - \psi_i) = 0$ ". After discretization by finite differences or piecewise linear finite elements, the matrix $A$ is typically an M-matrix, which is why this class sits at the centre of the numerical analysis of variational inequalities.

The primal-dual active set strategy solves such problems by guessing which constraints are active, solving one linear system on that guess, and updating the guess from the new primal and dual values. Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the problem. Local superlinear convergence then follows from Newton theory. This mission concerns the paper's global result: for M-matrices the method converges from every starting point, and its primal iterates decrease monotonically. A related global result for a purely primal active set method appears in Hoppe's 1987 analysis of multigrid methods for obstacle problems, which the paper cites as [H].

Setting

Fix $n \ge 0$ , a matrix $A \in \mathbb{R}^{n\times n}$ , vectors $f, \psi \in \mathbb{R}^n$ and a constant $c > 0$ . Vectors are compared componentwise. The paper writes $A$ for the matrix and calligraphic $\mathcal{A}$ , $\mathcal{I}$ for index sets; Lean uses A for the matrix and activeSet for $\mathcal{A}$ .

Problem (3.1). Find $(y, \lambda) \in \mathbb{R}^n \times \mathbb{R}^n$ with

Ay + \lambda = f, \qquad \lambda - \max(0, \lambda + c(y - \psi)) = 0,

the maximum taken componentwise. For $c > 0$ the second equation says exactly $y \le \psi$ , $\lambda \ge 0$ and $\lambda_i (y_i - \psi_i) = 0$ for every $i$ .

M-matrix. $A$ is an M-matrix if it is nonsingular, its off-diagonal entries satisfy $a_{ij} \le 0$ for $i \ne j$ , and its inverse is entrywise nonnegative, $A^{-1} \ge 0$ .

Blocks. For an index set $\mathcal{I}$ with complement $\mathcal{A}$ , $A_{\mathcal{I}}$ is the principal submatrix with rows and columns in $\mathcal{I}$ , and $A_{\mathcal{I}\mathcal{A}}$ the submatrix with rows in $\mathcal{I}$ and columns in $\mathcal{A}$ .

The algorithm. Start from arbitrary $(y^0, \lambda^0)$ . Given $(y^k, \lambda^k)$ , let

\mathcal{A}_k = \{ i : \lambda^k_i + c(y^k - \psi)_i > 0\}, \qquad \mathcal{I}_k = \{ i : \lambda^k_i + c(y^k - \psi)_i \le 0\},

and let $(y^{k+1}, \lambda^{k+1})$ solve

Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k.

A sequence obeying this rule for every $k$ is a run. The solution of (3.1) is written $x^* = (y^*, \lambda^*)$ and the iterates $x^k = (y^k, \lambda^k)$ .

Formalization targets

Goal: Theorem 3.2 (p. 7)

If $A$ is an M-matrix, then for arbitrary initial data

x^k \to x^*, \qquad y^* \le y^{k+1} \le y^k \ \text{ for all } k \ge 1, \qquad y^k \le \psi \ \text{ for all } k \ge 2.

Milestones (Appendix A, p. 20)

For every partition $\mathcal{I}, \mathcal{A}$ : $A_{\mathcal{I}}$ is regular, $A_{\mathcal{I}}^{-1} \ge 0$ and $A_{\mathcal{I}}^{-1} A_{\mathcal{I}\mathcal{A}} \le 0$ .
Complementarity (A.1): $\lambda^k_i = 0$ or $y^k_i = \psi_i$ , for all $i$ and $k \ge 1$ , for every run and every matrix.
Monotonicity: $y^{k+1} \le y^k$ for $k \ge 1$ .
Primal feasibility: $y^k \le \psi$ for $k \ge 2$ .
Lower bound: $y^* \le y^k$ for $k \ge 1$ .
Remark A.1 and dual feasibility: if $\lambda^{\bar k}_i < 0$ with $\bar k \ge 1$ , then $\lambda^k_i = 0$ and $y^k_i \le \psi_i$ for all $k \ge \bar k + 1$ ; and $\lambda^k \ge 0$ for all $k$ beyond some $k_o$ .

A companion item states that a run exists from every initial pair when $A$ is an M-matrix.

Significance

The result. Theorem 3.2 makes the active set strategy a globally convergent method for the discretized obstacle problem, with no line search, no merit function and no damping. The monotonicity statement says more: from the second iterate on, every primal iterate is feasible and lies above the solution, and the iterates descend to it. Combined with the paper's observation (p. 7) that convergent iterates of the method converge in finitely many steps, it gives finite termination from every starting point. The theorem is the model for later global results on the method under weaker hypotheses, two of which (a norm condition and small perturbations of M-matrices) appear in the same paper as Theorems 3.3 and 3.4.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires the classical sign facts on principal blocks of M-matrices, which Mathlib does not contain, and a careful treatment of the iteration as a relation on pairs of vectors. The M-matrix block lemma is reusable well beyond this mission, for instance in comparison principles for discretized elliptic problems.

Difficulty

The obvious argument would bound a merit function or a contraction factor; neither is available, because the iteration map is discontinuous and the active sets change from step to step. The paper's argument is instead an order argument. Its central step is the monotonicity $y^{k+1} \le y^k$ : it requires the complementarity (A.1) of the previous iterate, which holds only from $k = 1$ on, and the sign structure of the blocks $A_{\mathcal{I}_k}^{-1}$ and $A_{\mathcal{I}_k}^{-1} A_{\mathcal{I}_k \mathcal{A}_k}$ for every possible active set. The index bounds are sharp in the sense that the statements fail at $k = 0$ (respectively $k = 1$ for feasibility), because the initial data are arbitrary. Convergence of the multipliers is a separate step: negative multiplier coordinates must be shown to vanish permanently after one more iteration.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the product is A *ᵥ y, and $\le$ on vectors is componentwise. Convergence of $x^k$ is in the product topology on $\mathbb{R}^n \times \mathbb{R}^n$ .
Nonsingularity of an M-matrix is IsUnit A.det. Lean's inverse of a singular matrix is the zero matrix, so without this clause every singular matrix with nonpositive off-diagonal entries would count as an M-matrix; the M-matrix definition is the page's, not an equivalent characterization.
The solution is a hypothesis IsSolution A f ψ c ystar lamstar. The paper speaks of "the unique solution"; for an M-matrix it exists and is unique by Berman–Plemmons, so the hypothesis assumes nothing the paper does not have. The uniqueness fact is not restated.
The algorithm is a relation. One step is IsStep, a run is IsRun with free initial data y 0, lam 0. The stopping option of step (iv) is not modelled. Because a universally quantified statement over runs would be empty if no run existed, the companion item run_exists states existence of a run from every initial pair.
The constant $c > 0$ is a binder of every statement that needs it; (A.1) needs neither $c > 0$ nor any hypothesis on $A$ , and has none.
Remark A.1 is printed without " $\bar k \ge 1$ "; its proof assumes it and the statement is false at $\bar k = 0$ , so the bound is kept.
A trivializing formalization is ruled out: no statement assumes monotonicity, feasibility or convergence of the iterates, and the M-matrix hypothesis cannot be met by a singular matrix.
Needed infrastructure: principal submatrices of M-matrices (Berman–Plemmons, Ch. 6), and inverse-nonnegativity arguments for block systems. Proofs of the block lemma, of (A.1) and of the order lemmas are welcome independently of the goal.

The printed closing step of the proof writes $\lambda^k = Ay^k + f$ ; step (iii) gives $\lambda^k = f - Ay^k$ . No item quotes or depends on that line.

Selected references

M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3):865–888, 2002. https://doi.org/10.1137/S1052623401383558 (authors' version: https://hal.science/hal-01660511)
A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, Academic Press, 1979; reprinted as SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262
R. H. W. Hoppe, Multigrid algorithms for variational inequalities, SIAM J. Numer. Anal. 24(5):1046–1065, 1987. https://doi.org/10.1137/0724069
L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Program. 58:353–367, 1993. https://doi.org/10.1007/BF01581275

9 thms2 active usersReviewed

Algorithmic Game Theory Dynamical Systems·Captain: mikedeng1

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 1: Near the Two-Player Unit-Disk Game Γ₀ of Section II, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

Learning in games asks whether players who adjust their strategies over time, by simple rules, end up at a Nash equilibrium. Many adaptive dynamics share one informational feature: each player's adjustment depends on the current play and on that player's own payoff function, but not on the payoffs of the others. Hart and Mas-Colell (AER 2003) call such dynamics uncoupled, and show that this feature alone rules out guaranteed convergence to Nash equilibrium, even for families of games in which every game has exactly one equilibrium. Earlier non-convergence results, such as Shapley's example for fictitious play and the cycling examples of Jordan (1993) and Foster and Young (1998), concern particular dynamics; this one applies to the whole class of uncoupled dynamics. It is one reason the learning literature turned to weaker targets such as correlated equilibrium, which regret-based uncoupled procedures do reach (Hart and Mas-Colell, Econometrica 2000).

The paper proves its theorem in two settings: a two-player game with a continuum of strategies (§II and the Appendix) and a three-player game with two strategies each (§III). This mission formalizes the first setting.

Setting

There are two players, $i=1,2$ , and $j=3-i$ denotes the other player. Each player's strategy set is the closed unit disk $D=\{z\in\mathbb R^2:\|z\|\le1\}$ , and a profile is $x=(x^1,x^2)\in X:=D\times D$ . A game $\Gamma=(u^1,u^2)$ is a pair of payoff functions on $X$ . A profile $\bar x$ is a (pure) Nash equilibrium if no player gains by changing only their own strategy. A dynamic for a family $\mathcal U$ of games is a vector field $F(x;\Gamma)$ on $X$ for each $\Gamma\in\mathcal U$ , read $\dot x=F(x;\Gamma)$ . It is uncoupled if $F^i$ depends on the game only through $u^i$ : two games of $\mathcal U$ in which player $i$ has the same payoff function give the same $F^i(x;\cdot)$ at every $x\in X$ .

A dynamic is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ with its Nash equilibrium $\bar x(\Gamma)$ :

$F(\cdot\,;\Gamma)$ is $C^1$ on $X$ ;
$F(\bar x(\Gamma);\Gamma)=0$ ;
all eigenvalues of the $4\times4$ Jacobian matrix of $F(\cdot\,;\Gamma)$ at $\bar x(\Gamma)$ have negative real parts;
every solution $x(t)$ converges to $\bar x(\Gamma)$ as $t\to\infty$ , from any initial condition.

The game $\Gamma_0$ has payoffs $u_0^i(x^i,x^j)=-\|x^i-\varphi(x^j)\|^2$ . Here $\varphi:D\to D$ is continuous, $\varphi(z)=2z$ for $\|z\|\le\frac13$ , $\varphi$ rotates the unit circle by $\pi/4$ , and $\varphi$ is affine on rays in between. The family $\mathcal U_0$ consists of the games $u^i(x^i,x^j)=-\|x^i-\xi^i(x^j)\|^2$ with continuous $\xi^i:D\to D$ such that $\xi^i(\xi^j(x^i))=x^i$ has a unique solution. Every such game has a unique Nash equilibrium, and $\Gamma_0\in\mathcal U_0$ has the equilibrium $(0,0)$ .

Formalization targets

Goal: THEOREM 1 for the game $\Gamma_0$ of §II

Let $\mathcal U$ be a family in which each game has a single Nash equilibrium and which contains every game of $\mathcal U_0$ within some $\eta>0$ of $\Gamma_0$ . Then

F\ \text{uncoupled for}\ \mathcal U\ \Longrightarrow\ F\ \text{is not Nash-convergent for}\ \mathcal U.

Milestones

the explicit $\varphi$ has the two required properties, and rotates by an angle in $[0,\pi/4]$ (fn. 21);
every game of $\mathcal U_0$ has a unique Nash equilibrium, and that of $\Gamma_0$ is $(0,0)$ ;
Lemma 2: for an uncoupled Nash-convergent dynamic on $\mathcal U_0$ , at a unique best reply $F^i=0$ and the own-strategy Jacobian block $J^i$ has eigenvalues with negative real parts;
the derivative identity, giving the Jacobian at $\Gamma_0$ the block form

J=\begin{bmatrix}J^1&-2J^1\\-2J^2&J^2\end{bmatrix};

the coefficient $a_3=3\det(J^1)\operatorname{tr}(J^2)+3\det(J^2)\operatorname{tr}(J^1)$ of $\lambda$ in $\det(J-\lambda I)$ , and Lemma 3: if $J^1,J^2$ are stable, then $J$ has an eigenvalue with positive real part;
the main-text result: no uncoupled dynamic is Nash-convergent for $\mathcal U_0$ ;
the Appendix: the functions $\psi_a$ satisfy conditions (1)–(4), and the conclusions of Lemma 2 at $\Gamma_0$ already follow from the games of $\mathcal U_0$ near $\Gamma_0$ .

A companion statement, that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent, shows that the notion of Nash-convergence can be met.

Significance

The theorem identifies an informational obstruction rather than a computational one. Convergence to Nash equilibrium is easy if the dynamic may use the whole game, as the coupled dynamic $\dot x=\bar x(\Gamma)-x$ shows. It fails once each player may react only to their own payoff function, and the failure persists on an arbitrarily small neighborhood of a single game. It explains why no natural adaptive procedure has been found that converges to Nash equilibrium in general, and it motivates the stochastic, finite-memory and correlated-equilibrium variants studied afterwards (for example Hart and Mas-Colell, GEB 2006).

The result is proved in the paper. As far as the curators know, it has no machine-checked proof. A formalization fixes the model precisely. That matters here, because the conclusion depends on details the prose treats lightly: which perturbations the family must contain, what the Jacobian is at boundary points, and which solutions count.

Difficulty

The obvious argument fails because an uncoupled dynamic is a different vector field for each game, and nothing forces the fields to fit together except the uncoupledness constraint. The proof extracts information about $F(\cdot\,;\Gamma_0)$ from auxiliary games that share one player's payoff with $\Gamma_0$ , and in which that player's best reply is constant. Making those auxiliary games lie in the family is the delicate part: in $\mathcal U_0$ they are immediate, but near $\Gamma_0$ they require the functions $\psi_a$ of the Appendix, whose fixed-point conditions (3) and (4) rest on an angle argument. The linear-algebra step is exact: the stability of $J^1$ and $J^2$ must be shown to force instability of the coupled $4\times4$ matrix through the sign of one coefficient of its characteristic polynomial.

Formalization scope

$\mathbb R^2$ is modelled as $\mathbb C$ , and rotation by $\theta$ is multiplication by $e^{i\theta}$ . Players are Fin 2, 0-based, and the other player is i + 1. A game is a pair of real functions on $\mathbb C^2$ , but every definition looks only at its values on $X=D\times D$ . Nash equilibria are pure equilibria in $X$ (fn. 9 notes there are no mixed ones). Derivatives are Fréchet derivatives within $X$ . Eigenvalue conditions use the published predicate FatkhullinPolyak.Discrete.IsHurwitz, with the $4\times4$ Jacobian indexed in player-major order. The $C^1$ and Jacobian conditions, which the paper imposes on every dynamic it considers, are part of NashConvergent. The single-Nash-equilibrium property is a hypothesis of the goal.

Two encodings are deliberate:

The neighborhood. " $\mathcal U$ contains a neighborhood of $\Gamma_0$ " is read as the Appendix reads it: $\mathcal U$ contains every game of $\mathcal U_0$ close to $\Gamma_0$ in the sense of fn. 7. This is implied by the literal hypothesis, so the formal theorem is at least as strong. A full neighborhood contains games with several equilibria, so together with the single-equilibrium hypothesis it would make the theorem vacuous.
Solutions. Solutions are curves that stay in $X$ . If curves were allowed to leave $X$ , they would follow values of $F$ that no game constrains, and Nash-convergence would fail for every $F$ , which makes the goal trivial. The goal must also not be met through an empty family: the hypotheses are jointly satisfiable, for instance by $\{\Gamma\in\mathcal U_0:\Gamma\text{ within }1\text{ of }\Gamma_0\}$ .

The development needs:

calculus of $C^1$ maps on a product of disks;
spectra of real matrices viewed over $\mathbb C$ and the characteristic polynomial of a $4\times4$ block matrix;
elementary planar geometry of rotations and radial interpolation.

The linear-algebra milestones (block Jacobian, $a_3$ , Lemma 3) are independent of game theory and reusable. Contributions are welcome on any milestone, in any order.

Selected references

S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5), 1830–1836, 2003. https://doi.org/10.1257/000282803322655581
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5), 1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153
J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3), 368–386, 1993. https://doi.org/10.1006/game.1993.1022
D. P. Foster and H. P. Young, On the Nonconvergence of Fictitious Play in Coordination Games, Games and Economic Behavior 25(1), 79–96, 1998. https://doi.org/10.1006/game.1997.0615
S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2), 286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007

14 thms2 active usersReviewed

Completed

Algorithmic Game Theory Dynamical Systems·Captain: mikedeng1

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 2: Near Jordan's Three-Player Game Γ₀ of Section III, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

A central question of the theory of learning in games is whether simple adaptive behavior leads players to a Nash equilibrium. Many natural dynamics — fictitious play, best-reply dynamics, replicator dynamics — fail to converge in some games, and the failures are usually exhibited one dynamic at a time. Hart and Mas-Colell (AER 2003) asked a structural question instead: is there any continuous-time dynamic, satisfying one informational restriction, that converges to Nash equilibrium for all games in a reasonable family? The restriction is uncoupledness: each player's adjustment may depend on the current strategy profile and on that player's own payoff function, but not on the payoff functions of the others. This is the situation of players who do not know the opponents' preferences.

Their answer is negative, and the paper proves it with two examples. This mission formalizes the second, built on a three-player game introduced by James Jordan (GEB 1993) in his study of learning mixed-strategy equilibria. A companion mission formalizes the first example, a two-player game on the unit disk.

Setting

Three players each choose between two pure strategies, $0$ and $1$ . A game $\Gamma$ is identified with its payoff functions $(u^1,u^2,u^3)$ , $u^i:\{0,1\}^3\to\mathbb R$ . A state is a mixed profile $x=(x^1,x^2,x^3)\in X=[0,1]^3$ , where $x^i$ is the probability that player $i$ plays $0$ (top row, left column, left matrix). Payoffs extend to $X$ by expectation over independent randomizations, and $\bar x$ is a Nash equilibrium when no player can raise its expected payoff by changing its own coordinate.

Jordan's family $\mathcal U_0$ consists of the games

u^i(s)=\begin{cases}a^i & s^i=0,\ s^{i+1}=1,\\ 1 & s^i=1,\ s^{i+1}=0,\\ 0&\text{otherwise,}\end{cases}

indices modulo 3, with parameters $a^i$ close to $1$ : each player wants to mismatch the next player. Jordan's game $\Gamma_0$ is the member with all $a^i=1$ ; every game of $\mathcal U_0$ has a unique Nash equilibrium $\bar x^i(\Gamma)=a^{i-1}/(a^{i-1}+1)$ , and $\bar x(\Gamma_0)=(1/2,1/2,1/2)$ .

A dynamic for a family $\mathcal U$ is a vector field $\dot x=F(x;\Gamma)$ on $X$ , one for each $\Gamma\in\mathcal U$ . It is uncoupled if $F^i(x;\Gamma)=F^i(x;\Gamma')$ whenever $\Gamma,\Gamma'\in\mathcal U$ give player $i$ the same payoff function. When every game of $\mathcal U$ has a single Nash equilibrium $\bar x(\Gamma)$ , $F$ is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ , $\bar x(\Gamma)$ is a rest point, every solution converges to it, $F(\cdot;\Gamma)$ is $C^1$ , and the Jacobian $J$ of $F(\cdot;\Gamma)$ at $\bar x(\Gamma)$ is hyperbolic and stable: all its eigenvalues have negative real parts.

Formalization targets

Goal: Theorem 1 near Jordan's game

Let $\mathcal U$ have the single-Nash-equilibrium property and contain every game of $\mathcal U_0$ that is close to $\Gamma_0$ . Then

\text{no uncoupled dynamic for }\mathcal U\text{ is Nash-convergent for }\mathcal U .

Milestones

Every game of $\mathcal U_0$ (indeed every $a$ with all $a^i>0$ ) has the unique equilibrium $\bar x^i=a^{i-1}/(a^{i-1}+1)$ ; in particular $\bar x_0=(1/2,1/2,1/2)$ .
If $F$ is uncoupled and Nash-convergent, then $f=F(\cdot;\Gamma_0)$ satisfies $f^i(\bar x_0+(y-\tfrac12)e_i)=0$ for $y$ near $1/2$ , hence the diagonal and the trace of $J=Df(\bar x_0)$ vanish:

\operatorname{tr}J=0.

A real $3\times3$ matrix with zero trace and nonzero determinant has an eigenvalue with positive real part.

Two further items record the paper's observations: uncoupledness forces $J=\begin{pmatrix}0&c&0\\0&0&d\\e&0&0\end{pmatrix}$ , and such a matrix has an eigenvalue with positive real part when $cde\ne0$ and spectrum $\{0\}$ otherwise. A last item shows that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent.

Significance

The theorem says that convergence to Nash equilibrium is not a property that adaptive dynamics can deliver on informational grounds alone: as soon as a family contains the games near $\Gamma_0$ , any rule in which players respond only to their own payoffs fails for some game, even though every game in the family has a unique equilibrium and a coupled rule converges for all of them. The finite example matters because it shows that the obstruction is not an artifact of continuum strategy spaces: it occurs in a $2\times2\times2$ game in mixed strategies. The paper contrasts it (§IV) with the existence of uncoupled dynamics that converge to correlated equilibria: Nash equilibrium cannot be reached in an uncoupled way, while correlated equilibrium, a notion based on coordination, can. Follow-up work extends the impossibility to stochastic uncoupled dynamics (Hart and Mas-Colell, GEB 2006) and surveys the area (Hart, Econometrica 2005).

The result has been proved since 2003; no machine-checked proof of it is known. A formal proof requires an equilibrium computation in a parametric family of finite games, a careful treatment of the derivative of a vector field defined only on a cube, and a spectral fact about real $3\times3$ matrices. The definitions of uncoupled and Nash-convergent dynamics written here are reusable for other impossibility results of the same kind.

Difficulty

The obvious attempt is to analyze a particular dynamic and show that it cycles around $\bar x_0$ . That proves nothing about other dynamics: the statement quantifies over every uncoupled $F$ , so the argument must extract a constraint on $F$ from uncoupledness alone. Uncoupledness only relates the dynamic at different games through single coordinates of $F$ , and Nash-convergence only constrains $F$ at the equilibria of the games in $\mathcal U$ ; neither says anything directly about the Jacobian at $\Gamma_0$ . Formally, the delicate steps are the uniqueness of the equilibrium for all nearby parameters, which requires excluding pure and partially mixed equilibria, and the passage from vanishing along a segment to a vanishing partial derivative.

Formalization scope

Players are indexed $0,1,2$ in Lean (the page's player $i$ is index $i-1$ ), strategies are Fin 2, and a game is Fin 3 → (Fin 3 → Fin 2) → ℝ. The state space is $X=[0,1]^3\subset\mathbb R^3$ ; a dynamic is any map $F:\mathbb R^3\times\text{Game}\to\mathbb R^3$ , whose values outside $X$ never matter. Committed conventions:

Solutions stay in $X$ : a solution is a curve on $[0,\infty)$ with values in $X$ satisfying the ODE (one-sided derivative at $0$ ). Allowing curves that leave $X$ would let the junk values of $F$ outside $X$ falsify convergence for every $F$ and trivialize the goal.
Uncoupledness is required only between games of $\mathcal U$ and only at states of $X$ .
Nash-convergence bundles four clauses for every game of $\mathcal U$ and every Nash equilibrium of it: rest point, $C^1$ on $X$ , all eigenvalues of the Jacobian with negative real part (the published FatkhullinPolyak.Discrete.IsHurwitz), and convergence of every solution. The Jacobian is the derivative within $X$ .
The single-Nash-equilibrium property of $\mathcal U$ is a hypothesis of the goal.
The neighborhood hypothesis. The page assumes that $\mathcal U$ contains a neighborhood of $\Gamma_0$ . The goal assumes less: $\mathcal U$ contains every game of $\mathcal U_0$ in some footnote-7 neighborhood of $\Gamma_0$ . The page's hypothesis implies this one, so the formal goal is at least as strong. The literal hypothesis is not used because it is not known (and not claimed on the page) to be compatible with the single-equilibrium property, and a contradictory pair of hypotheses would make the goal vacuous.
Milestone 1 assumes only $a^i>0$ instead of $|a^i-1|<\varepsilon$ for small $\varepsilon$ ; this covers every such family with $\varepsilon\le1$ .

The family $\mathcal U$ cannot be vacuous: Jordan's games with $|a^i-1|<1/2$ satisfy both hypotheses, and the coupled-dynamic item certifies that Nash-convergence itself can be met, so the goal's force rests on uncoupledness. Contributions welcome include the equilibrium computation for $\mathcal U_0$ , the spectral lemmas (which are independent of game theory), and the calculus step from vanishing along a segment to a vanishing partial derivative within a cube.

Selected references

S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5):1830–1836, 2003. https://doi.org/10.1257/000282803322655581
J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3):368–386, 1993. https://doi.org/10.1006/game.1993.1022
S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2):286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007
S. Hart, Adaptive Heuristics, Econometrica 73(5):1401–1430, 2005. https://doi.org/10.1111/j.1468-0262.2005.00625.x

6 thms2 active usersReviewed