Gordon's theorem for Gaussian matrices: $\sqrt N-\sqrt n\le\mathbb E\,s_{\min}(A)\le\mathbb E\,s_{\max}(A)\le\sqrt N+\sqrt n$

Proved

GaussianMatrix.gordon

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

gaussian-matrixprobabilityrandom-matrix-theoryrandomized-numerical-linear-algebra

Let $A\in\mathbb R^{N\times n}$ , $n\ge1$ , be a matrix whose entries are independent standard normal random variables, with extreme singular values

s_{\min}(A)=\inf_{\|x\|_2=1}\|Ax\|_2,\qquad s_{\max}(A)=\sup_{\|x\|_2=1}\|Ax\|_2=\|A\|.

Then $s_{\min}(A)$ and $s_{\max}(A)$ are integrable and

\sqrt N-\sqrt n\ \le\ \mathbb E\,s_{\min}(A)\ \le\ \mathbb E\,s_{\max}(A)\ \le\ \sqrt N+\sqrt n .

This is the exact non-asymptotic counterpart of the Bai–Yin law for Gaussian matrices (Gordon; Davidson–Szarek). The upper bound is proved from Slepian's comparison inequality, the lower bound from Gordon's minimax comparison inequality for Gaussian processes. Together with Gaussian concentration it yields the deviation inequalities for $s_{\min}$ and $s_{\max}$ , and the lower bound $\mathbb E\,\sigma_{\min}\ge\sqrt t-\sqrt k$ is the starting point of small-ball estimates for Gaussian sketches.

Formalization Note. $s_{\min}$ is the infimum over the unit sphere of $\mathbb R^n$ (the hypothesis $n\ge1$ makes the sphere nonempty); $N\ge n$ is not required — for $N<n$ one has $s_{\min}(A)=0$ and the lower bound is trivially true. $s_{\max}(A)$ is Mathlib's $\ell_2$ operator norm. The conclusion includes integrability of both functions, so that the integrals are genuine expectations.

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem gordon {N n : ℕ} (hn : 1 ≤ n) :
    Integrable (fun A : Fin N → Fin n → ℝ => sMin (Matrix.of A)) (gaussianMatrix N n) ∧
    Integrable (fun A : Fin N → Fin n → ℝ => specNorm (Matrix.of A)) (gaussianMatrix N n) ∧
    Real.sqrt N - Real.sqrt n ≤ ∫ A, sMin (Matrix.of A) ∂(gaussianMatrix N n) ∧
    ∫ A, sMin (Matrix.of A) ∂(gaussianMatrix N n)
      ≤ ∫ A, specNorm (Matrix.of A) ∂(gaussianMatrix N n) ∧
    ∫ A, specNorm (Matrix.of A) ∂(gaussianMatrix N n) ≤ Real.sqrt N + Real.sqrt n := by sorry
end GaussianMatrix

Source

R. Vershynin, *Introduction to the non-asymptotic analysis of random matrices*, Chapter 5 of Compressed Sensing: Theory and Applications (Y. Eldar, G. Kutyniok, eds.), Cambridge University Press, 2012, https://arxiv.org/abs/1011.3027 (v7), §5.3.1 p. 20–21, Theorem 5.32 (Gordon's theorem for Gaussian matrices): for an

N\times n

matrix with independent standard normal entries,

\sqrt N-\sqrt n\le\mathbb E s_{\min}(A)\le\mathbb E s_{\max}(A)\le\sqrt N+\sqrt n

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Let $N, n$ be natural numbers with $1 \le n$ (there is no hypothesis relating $N$ and $n$ ; $N = 0$ and $N < n$ are allowed). Let $\mu_{N,n}$ be the product measure on $N \times n$ real arrays $A$ with i.i.d. $\mathcal N(0,1)$ entries, a probability measure. For an $N \times n$ real matrix $A$ define

$\sigma_{\min}(A) := \inf\big\{\, \sqrt{(Ax)\cdot(Ax)} \;:\; x \in \mathbb R^n,\ x \cdot x = 1 \,\big\} = \inf_{\|x\|_2 = 1} \|Ax\|_2$ , where the infimum is the real-number infimum (equal to $0$ if the index set were empty or the set unbounded below; here $n \ge 1$ makes the unit sphere nonempty and the values are $\ge 0$ , so it is a genuine infimum);
$\|A\|_{\mathrm{op}}$ := the $\ell_2 \to \ell_2$ operator norm of $A$ (largest singular value), i.e. $\sup_{\|x\|_2 \le 1} \|Ax\|_2$ .

When $N = 0$ , $A$ is the empty $0 \times n$ matrix, $Ax$ is the empty vector, and both $\sigma_{\min}(A) = 0$ and $\|A\|_{\mathrm{op}} = 0$ .

The statement asserts the conjunction of five claims:

$A \mapsto \sigma_{\min}(A)$ is integrable with respect to $\mu_{N,n}$ ;
$A \mapsto \|A\|_{\mathrm{op}}$ is integrable with respect to $\mu_{N,n}$ ;
$\sqrt N - \sqrt n \le \displaystyle\int \sigma_{\min}(A)\, d\mu_{N,n}(A)$ ;
$\displaystyle\int \sigma_{\min}(A)\, d\mu_{N,n}(A) \le \int \|A\|_{\mathrm{op}}\, d\mu_{N,n}(A)$ ;
$\displaystyle\int \|A\|_{\mathrm{op}}\, d\mu_{N,n}(A) \le \sqrt N + \sqrt n$ .

Here $\sqrt N, \sqrt n$ are real square roots of the natural numbers viewed as reals. The integrals are Lebesgue integrals (which would be $0$ by convention for a non-integrable integrand, but claims 1 and 2 exclude that). In particular, when $N < n$ (allowed), claim 3 asserts the nonpositive number $\sqrt N - \sqrt n$ is at most the mean of $\sigma_{\min}$ .

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by tc · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Gordon's theorem for Gaussian matrices: N−n≤E smin⁡(A)≤E smax⁡(A)≤N+n\sqrt N-\sqrt n\le\mathbb E\,s_{\min}(A)\le\mathbb E\,s_{\max}(A)\le\sqrt N+\sqrt nN​−n​≤Esmin​(A)≤Esmax​(A)≤N​+n​

Gordon's theorem for Gaussian matrices: $\sqrt N-\sqrt n\le\mathbb E\,s_{\min}(A)\le\mathbb E\,s_{\max}(A)\le\sqrt N+\sqrt n$