One-sided Gaussian tail for the smallest singular value: $\mathbb P\{s_{\min}(A)\le\sqrt N-\sqrt n-u\}\le e^{-u^2/2}$

Proved

GaussianMatrix.sMin_lower_tail

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}$ be a standard Gaussian matrix with $1\le n\le N$ and let $s_{\min}(A)=\inf_{\|x\|_2=1}\|Ax\|_2$ be its smallest singular value. For every $u\ge0$ ,

\mathbb P\bigl\{s_{\min}(A)\le\sqrt N-\sqrt n-u\bigr\}\ \le\ e^{-u^2/2}.

This is the one-sided form of the deviation inequality for $s_{\min}$ : Gordon's inequality gives $\mathbb E\,s_{\min}(A)\ge\sqrt N-\sqrt n$ , and one-sided Gaussian concentration for the $1$ -Lipschitz function $A\mapsto s_{\min}(A)$ gives $\mathbb P\{s_{\min}\le\mathbb E s_{\min}-u\}\le e^{-u^2/2}$ . It saves the factor $2$ of the two-sided corollary, and it is the tail bound used to control inverse moments of $\sigma_{\min}$ of a Gaussian sketch in the regime $s$ close to $\sqrt N-\sqrt n$ .

Formalization Note. For a wide $k\times t$ Gaussian matrix $G$ ( $k\le t$ ) the usual $\sigma_{\min}(G)$ equals $s_{\min}(G^{\mathsf T})$ , so the wide form is this statement with $(N,n)=(t,k)$ . The event uses $\le$ ; Davidson–Szarek state it with $<$ for the matrix normalized by $N^{-1/2}$ .

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem sMin_lower_tail {N n : ℕ} (hn : 1 ≤ n) (hnN : n ≤ N) (u : ℝ) (hu : 0 ≤ u) :
    (gaussianMatrix N n) {A | sMin (Matrix.of A) ≤ Real.sqrt N - Real.sqrt n - u}
      ≤ ENNReal.ofReal (Real.exp (-u ^ 2 / 2)) := by sorry
end GaussianMatrix

Source

K. R. Davidson, S. J. Szarek, *Local operator theory, random matrices and Banach spaces*, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001, https://doi.org/10.1016/S1874-5849(01)80010-3, §II.7 p. 334, Theorem II.13: for an

N\times n

matrix

\Gamma

with independent

\mathcal N(0,1/N)

entries and

t>0

\mathbb P\{s_{\min}(\Gamma)<1-\sqrt{n/N}-t\}\le e^{-Nt^2/2}

(rescaling by

\sqrt N

gives the statement with

\le

by right-continuity of the bound). Equivalently the one-sided form of 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, obtained from Theorem 5.32 (

\mathbb E s_{\min}\ge\sqrt N-\sqrt n

) and Proposition 5.34 applied to the

1

-Lipschitz function

-s_{\min}

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 \le N$ , and let $u$ be a real number with $u \ge 0$ . Let $\mu_{N,n}$ be the product measure on $N \times n$ real arrays with i.i.d. $\mathcal N(0,1)$ entries. For an $N \times n$ real matrix $A$ let

\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,

the real infimum over the unit sphere (nonempty since $n \ge 1$ ; values $\ge 0$ , so this is a genuine infimum and $\sigma_{\min}(A) \ge 0$ ). The statement asserts

\mu_{N,n}\big(\{A : \sigma_{\min}(A) \le \sqrt N - \sqrt n - u\}\big) \;\le\; \operatorname{ofReal}\!\big(e^{-u^2/2}\big),

with the left side the outer measure of the displayed set (no measurability assumed) and the right side an element of $[0,\infty]$ ; since $e^{-u^2/2} > 0$ no truncation occurs. Edge cases: if $\sqrt N - \sqrt n - u < 0$ the set is empty (as $\sigma_{\min} \ge 0$ ) and the left side is $0$ ; when $u = 0$ the bound is $1$ , which is automatic for a probability measure; when $N = n$ the threshold is $-u \le 0$ , so the event is $\{\sigma_{\min}(A) \le -u\}$ , which is empty for $u > 0$ and equals $\{\sigma_{\min}(A) = 0\}$ for $u = 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

One-sided Gaussian tail for the smallest singular value: P{smin⁡(A)≤N−n−u}≤e−u2/2\mathbb P\{s_{\min}(A)\le\sqrt N-\sqrt n-u\}\le e^{-u^2/2}P{smin​(A)≤N​−n​−u}≤e−u2/2

One-sided Gaussian tail for the smallest singular value: $\mathbb P\{s_{\min}(A)\le\sqrt N-\sqrt n-u\}\le e^{-u^2/2}$