Prove2Me

Lower tail of the smallest Wishart eigenvalue: P{λmin⁡(GG⊤)≤t}≤1Γ(k−r+2)(t(k+r)2)(k−r+1)/2\mathbb P\{\lambda_{\min}(GG^\top)\le t\}\le \frac{1}{\Gamma(k-r+2)}\big(\tfrac{t(k+r)}{2}\big)^{(k-r+1)/2}

Open
GaussianMatrix.wishart_lambda_min_tail

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

gaussian-matrixrandom-matricessmall-ball-probabilitysmallest-eigenvaluewishart-matrix

Let 1≤r≤k1\le r\le k be integers and let GG be an r×kr\times k random matrix with independent standard normal entries. Let

λmin⁡(GG⊤)=min⁡x∈Rr, ∥x∥2=1x⊤GG⊤x=σmin⁡(G⊤)2\lambda_{\min}(GG^\top)=\min_{x\in\mathbb R^r,\ \|x\|_2=1} x^\top GG^\top x=\sigma_{\min}(G^\top)^2

be the smallest eigenvalue of the r×rr\times r Wishart matrix GG⊤GG^\top, where σmin⁡(G⊤)=inf⁡∥x∥2=1∥G⊤x∥2\sigma_{\min}(G^\top)=\inf_{\|x\|_2=1}\|G^\top x\|_2 is the smallest singular value of the tall k×rk\times r matrix G⊤G^\top. Then for every t>0t>0,

P{λmin⁡(GG⊤)≤t}  ≤  1Γ(k−r+2)(t (k+r)2)(k−r+1)/2.\mathbb P\big\{\lambda_{\min}(GG^\top)\le t\big\}\;\le\;\frac{1}{\Gamma(k-r+2)}\Big(\frac{t\,(k+r)}{2}\Big)^{(k-r+1)/2}.

The bound comes from Edelman's estimate for the density of λmin⁡\lambda_{\min},

fλmin⁡(λ)≤2(k−r−1)/2 Γ(k+12)Γ(r2) Γ(k−r+1) λ(k−r−1)/2e−λ/2,λ>0,f_{\lambda_{\min}}(\lambda)\le\frac{2^{(k-r-1)/2}\,\Gamma(\frac{k+1}{2})}{\Gamma(\frac r2)\,\Gamma(k-r+1)}\,\lambda^{(k-r-1)/2}e^{-\lambda/2},\qquad \lambda>0,

after dropping e−λ/2e^{-\lambda/2}, bounding 2(k−r+1)/2Γ(k+12)/Γ(r2)≤((k+r)/2)(k−r+1)/22^{(k-r+1)/2}\Gamma(\frac{k+1}2)/\Gamma(\frac r2)\le((k+r)/2)^{(k-r+1)/2} (via Γ(z+12)≤z1/2Γ(z)\Gamma(z+\frac12)\le z^{1/2}\Gamma(z) and (r+i)(k−i)≤((k+r)/2)2(r+i)(k-i)\le((k+r)/2)^2), and integrating over (0,t](0,t].

This is the key probabilistic input for the tail of ∥G†∥=λmin⁡(GG⊤)−1/2\|G^\dagger\|=\lambda_{\min}(GG^\top)^{-1/2} (Chen–Dongarra / Halko–Martinsson–Tropp Prop. A.3) and for the inverse moments E∥(GG⊤)−1∥p\mathbb E\|(GG^\top)^{-1}\|^p (Tropp–Webber Lemma B.3).

Formalization Note. The law of GG is gaussianMatrix r k on Fin r → Fin k → ℝ; λmin⁡(GG⊤)\lambda_{\min}(GG^\top) is written sMin (Matrix.of G)ᵀ ^ 2. The hypothesis r≥1r\ge1 is necessary: for r=0r=0 the sphere in R0\mathbb R^0 is empty, sMin is 00 and the event is the whole space, while the right-hand side is <1<1 for small tt. Γ\Gamma is Real.Gamma and the exponent is a real power.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem wishart_lambda_min_tail {r k : ℕ} (hr : 1 ≤ r) (hrk : r ≤ k) (t : ℝ) (ht : 0 < t) :
    (gaussianMatrix r k) {G | sMin (Matrix.of G)ᵀ ^ 2 ≤ t}
      ≤ ENNReal.ofReal ((1 / Real.Gamma ((k : ℝ) - r + 2))
          * (t * ((k : ℝ) + r) / 2) ^ (((k : ℝ) - r + 1) / 2)) := by sorry

end GaussianMatrix
Source
A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4) (1988), Prop. 5.1 (density bound for λ_min of a Wishart matrix); combined as in J. A. Tropp and R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, arXiv:2306.12418, Appendix B, proof of Lemma B.3, eqs. (B.5)–(B.7); the statement is eq. (B.7).

View graph