Gaussian concentration for Lipschitz functions of a Gaussian matrix: $\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}$

Proved

GaussianMatrix.gaussian_concentration

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

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

Let $h:\mathbb R^{p\times m}\to\mathbb R$ be Lipschitz with respect to the Frobenius norm with constant $L>0$ ,

|h(X)-h(Y)|\le L\,\|X-Y\|_F\qquad\text{for all }X,Y,

and let $G\in\mathbb R^{p\times m}$ be a standard Gaussian matrix. Then $h(G)$ is integrable and, for every $t\ge0$ ,

\mathbb P\bigl\{h(G)\ \ge\ \mathbb E\,h(G)+L\,t\bigr\}\ \le\ e^{-t^2/2}.

This is the concentration-of-measure inequality in Gauss space (Tsirelson–Ibragimov–Sudakov; Vershynin Proposition 5.34, Halko–Martinsson–Tropp Proposition 10.3) for the standard Gaussian vector $\operatorname{vec}G\in\mathbb R^{pm}$ . Applied to the $1$ -Lipschitz functions $G\mapsto\sigma_{\max}(G)$ , $G\mapsto\sigma_{\min}(G)$ and $G\mapsto\|SGT\|$ it upgrades the expectation bounds of Gordon's theorem into tail bounds.

Formalization Note. The source states the bound with $\ge$ and no sign condition on $L$ and $t$ ; the formal statement requires $L>0$ and $t\ge0$ , since for $L=0$ (a constant $h$ ) or $t<0$ the event has probability $1$ . Vectors in $\mathbb R^{n}$ are the case $m=1$ .

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem gaussian_concentration {p m : ℕ} (h : (Fin p → Fin m → ℝ) → ℝ) (L : ℝ) (hL : 0 < L)
    (hLip : ∀ X Y, |h X - h Y| ≤ L * frobNorm (Matrix.of X - Matrix.of Y)) (t : ℝ) (ht : 0 ≤ t) :
    Integrable h (gaussianMatrix p m) ∧
    (gaussianMatrix p m) {X | (∫ Y, h Y ∂(gaussianMatrix p m)) + L * t ≤ h X}
      ≤ ENNReal.ofReal (Real.exp (-t ^ 2 / 2)) := by sorry
end GaussianMatrix

Source

N. Halko, P.-G. Martinsson, J. A. Tropp, *Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions*, SIAM Review 53(2), 2011, https://arxiv.org/abs/0909.4061 (v2), §10.1 p. 56, Proposition 10.3 (Concentration for functions of a Gaussian matrix):

|h(X)-h(Y)|\le L\|X-Y\|_F

implies

\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}

; also 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, Proposition 5.34 (Concentration in Gauss space).

Read-back

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

Let $p, m$ be arbitrary natural numbers (either may be $0$ ). Let $\mu_{p,m}$ denote the product measure on the space of $p \times m$ real arrays $X = (X_{ij})_{i < p,\, j < m}$ under which all $pm$ entries are independent standard normals $\mathcal N(0,1)$ ; it is a probability measure (when $p = 0$ or $m = 0$ the space is a single point and $\mu_{p,m}$ is the Dirac mass there). Let $h$ be any real-valued function on this space of arrays, let $L$ be a real number with $L > 0$ , and assume the Lipschitz condition that for all arrays $X, Y$

|h(X) - h(Y)| \le L \cdot \sqrt{\textstyle\sum_{i<p}\sum_{j<m} (X_{ij} - Y_{ij})^2} = L\,\|X - Y\|_F,

where $\|\cdot\|_F$ is the Frobenius norm (square root of the sum of squared entries; the square root is the real square root, which would return $0$ on a negative input, but the radicand is a sum of squares). Let $t$ be a real number with $t \ge 0$ . The statement asserts the conjunction of two things:

$h$ is integrable with respect to $\mu_{p,m}$ (i.e. $h$ is almost-everywhere strongly measurable and $\int |h|\, d\mu_{p,m} < \infty$ ); and
writing $\mathbb E h := \int h(Y)\, d\mu_{p,m}(Y)$ for the Lebesgue integral (which would be $0$ by convention if $h$ were not integrable, but item 1 excludes that), the $\mu_{p,m}$ -outer measure of the set

\{X : \mathbb E h + L\,t \le h(X)\}

is at most $\operatorname{ofReal}\!\big(e^{-t^2/2}\big)$ , an extended-nonnegative-real quantity; since $e^{-t^2/2} > 0$ no truncation occurs, and for $t = 0$ the bound is $1$ (so that case is automatic for a probability measure). No measurability of the set or of $h$ is assumed; the measure of a non-measurable set is its outer measure.

The Lipschitz hypothesis is with respect to the Frobenius norm of the entrywise difference; nothing else is assumed about $h$ . In the degenerate case $p = 0$ or $m = 0$ , $h$ is a function on a one-point space, the Lipschitz hypothesis is vacuous, and the event is empty when $t > 0$ and the whole space when $t = 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

Gaussian concentration for Lipschitz functions of a Gaussian matrix: P{h(G)≥Eh(G)+Lt}≤e−t2/2\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}P{h(G)≥Eh(G)+Lt}≤e−t2/2

Gaussian concentration for Lipschitz functions of a Gaussian matrix: $\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}$