Deviation of the extreme singular values of a Gaussian matrix: $\sqrt N-\sqrt n-t\le s_{\min}(A)\le s_{\max}(A)\le\sqrt N+\sqrt n+t$ with probability $\ge1-2e^{-t^2/2}$

Proved

GaussianMatrix.extreme_singular_values_deviation

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. Then for every $t\ge0$ , with probability at least $1-2\exp(-t^2/2)$ ,

\sqrt N-\sqrt n-t\ \le\ s_{\min}(A)\qquad\text{and}\qquad s_{\max}(A)\ \le\ \sqrt N+\sqrt n+t ,

where $s_{\min}(A)=\inf_{\|x\|_2=1}\|Ax\|_2$ and $s_{\max}(A)=\|A\|$ is the spectral norm.

This is Vershynin's Corollary 5.35, the non-asymptotic Gaussian analogue of the Bai–Yin law with explicit sub-Gaussian deviations. It follows from Gordon's expectation bounds and Gaussian concentration, since $s_{\min}$ and $s_{\max}$ are $1$ -Lipschitz functions of the matrix in the Frobenius norm. It is the standard tool for showing that a Gaussian sketch is a near-isometry, and for lower-bounding $\sigma_{\min}$ of the head block $\Omega_1$ in randomized low-rank approximation.

Formalization Note. The probability is a measure in $[0,\infty]$ and the lower bound $1-2e^{-t^2/2}$ is computed with truncated subtraction, so the statement is vacuous when $2e^{-t^2/2}\ge1$ , i.e. $t\le\sqrt{2\log2}$ , exactly as in the source. The inequality $s_{\min}(A)\le s_{\max}(A)$ is not part of the event (it is immediate).

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem extreme_singular_values_deviation {N n : ℕ} (hn : 1 ≤ n) (t : ℝ) (ht : 0 ≤ t) :
    1 - ENNReal.ofReal (2 * Real.exp (-t ^ 2 / 2))
      ≤ (gaussianMatrix N n) {A | Real.sqrt N - Real.sqrt n - t ≤ sMin (Matrix.of A) ∧
          specNorm (Matrix.of A) ≤ Real.sqrt N + Real.sqrt n + t} := 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. 21, Corollary 5.35 (Gaussian matrices, deviation): for every

t\ge0

, with probability at least

1-2\exp(-t^2/2)

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

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$ (no relation between $N$ and $n$ is assumed; $N = 0$ and $N < n$ are allowed) and let $t$ be a real number with $t \ge 0$ . Let $\mu_{N,n}$ be the law of an $N \times n$ array with i.i.d. $\mathcal N(0,1)$ entries. For an $N \times n$ real matrix $A$ write $\sigma_{\min}(A) := \inf\{\|Ax\|_2 : x \in \mathbb R^n,\ x\cdot x = 1\}$ (real infimum over the unit sphere, equal to $\inf_{\|x\|_2=1}\sqrt{(Ax)\cdot(Ax)}$ ; nonempty index set since $n \ge 1$ , values $\ge 0$ , so $\sigma_{\min}(A) \ge 0$ ) and $\|A\|_{\mathrm{op}}$ for the $\ell_2\to\ell_2$ operator norm (largest singular value). The statement asserts the inequality in the extended nonnegative reals

1 \;\dot{-}\; \operatorname{ofReal}\!\big(2 e^{-t^2/2}\big) \;\le\; \mu_{N,n}\Big(\big\{A : \sqrt N - \sqrt n - t \le \sigma_{\min}(A)\ \text{ and }\ \|A\|_{\mathrm{op}} \le \sqrt N + \sqrt n + t\big\}\Big),

where $\dot{-}$ is truncated subtraction in $[0,\infty]$ : whenever $2e^{-t^2/2} \ge 1$ , i.e. $0 \le t \le \sqrt{2\ln 2}$ , the left-hand side is $0$ and the claim holds trivially. The right-hand side is the outer measure of the displayed set (no measurability is assumed). When $N \le n$ the quantity $\sqrt N - \sqrt n - t$ is $\le 0 \le \sigma_{\min}(A)$ , so the first condition in the event holds for every $A$ and only the operator-norm condition is binding. When $N = 0$ both $\sigma_{\min}$ and the operator norm are identically $0$ .

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

Deviation of the extreme singular values of a Gaussian matrix: N−n−t≤smin⁡(A)≤smax⁡(A)≤N+n+t\sqrt N-\sqrt n-t\le s_{\min}(A)\le s_{\max}(A)\le\sqrt N+\sqrt n+tN​−n​−t≤smin​(A)≤smax​(A)≤N​+n​+t with probability ≥1−2e−t2/2\ge1-2e^{-t^2/2}≥1−2e−t2/2

Deviation of the extreme singular values of a Gaussian matrix: $\sqrt N-\sqrt n-t\le s_{\min}(A)\le s_{\max}(A)\le\sqrt N+\sqrt n+t$ with probability $\ge1-2e^{-t^2/2}$