Gordon–Chevet bound on the expected spectral norm of a scaled Gaussian matrix: $\mathbb E\|S\Gamma T\|\le\|S\|\|T\|_F+\|S\|_F\|T\|$

Proved

GaussianMatrix.chevet

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

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

Fix matrices $S\in\mathbb R^{a\times p}$ and $T\in\mathbb R^{m\times n}$ and let $\Gamma\in\mathbb R^{p\times m}$ be a standard Gaussian matrix. Then $\|S\Gamma T\|$ is integrable and

\mathbb E\,\|S\,\Gamma\,T\|\ \le\ \|S\|\,\|T\|_F+\|S\|_F\,\|T\|,

where $\|\cdot\|$ is the spectral norm and $\|\cdot\|_F$ the Frobenius norm.

This is the expected spectral norm bound of Halko–Martinsson–Tropp Proposition 10.1 (eq. (10.2)) and Appendix A, Proposition A.2, due to Gordon and proved from a sharp form of Slepian's lemma (Chevet's inequality). With $S=I$ , $T=I$ it recovers $\mathbb E\|\Gamma\|\le\sqrt p+\sqrt m$ ; in the randomized SVD it bounds $\mathbb E\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|$ conditionally on $\Omega_1$ .

Formalization Note. The conclusion is the conjunction of integrability (so the integral is a genuine expectation) and the bound.

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem chevet {a p m n : ℕ} (S : Matrix (Fin a) (Fin p) ℝ) (T : Matrix (Fin m) (Fin n) ℝ) :
    Integrable (fun G : Fin p → Fin m → ℝ => specNorm (S * Matrix.of G * T)) (gaussianMatrix p m) ∧
    ∫ G, specNorm (S * Matrix.of G * T) ∂(gaussianMatrix p m)
      ≤ specNorm S * frobNorm T + frobNorm S * specNorm T := 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. 55, Proposition 10.1 eq. (10.2), and Appendix A.1 p. 64, Proposition A.2:

\mathbb E\|SGT\|\le\|S\|\|T\|_F+\|S\|_F\|T\|

Read-back

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

Let $a, p, m, n$ be arbitrary natural numbers (any of them may be $0$ ), let $S$ be an arbitrary $a \times p$ real matrix and $T$ an arbitrary $m \times n$ real matrix; no hypotheses are placed on $S$ or $T$ . Let $\mu_{p,m}$ be the product measure on $p \times m$ real arrays $G$ with i.i.d. $\mathcal N(0,1)$ entries (a probability measure; a Dirac mass on a one-point space if $p = 0$ or $m = 0$ ). For a real matrix $M$ write $\|M\|_{\mathrm{op}}$ for its $\ell_2 \to \ell_2$ operator norm (largest singular value, $\sup_{\|x\|_2 \le 1}\|Mx\|_2$ ) and $\|M\|_F := \sqrt{\sum_{i,j} M_{ij}^2}$ for its Frobenius norm (real square root of the sum of squared entries). The statement asserts the conjunction of

the function $G \mapsto \|S\,G\,T\|_{\mathrm{op}}$ (operator norm of the $a \times n$ product matrix) is integrable with respect to $\mu_{p,m}$ ; and

\int \|S\,G\,T\|_{\mathrm{op}}\; d\mu_{p,m}(G) \;\le\; \|S\|_{\mathrm{op}}\,\|T\|_F + \|S\|_F\,\|T\|_{\mathrm{op}}.

The integral is the Lebesgue integral (which would be $0$ for a non-integrable integrand, but item 1 excludes this). If any of $a, p, m, n$ is $0$ , the matrix $S G T$ is empty (or $S$ or $T$ is empty), all norms involved that concern empty matrices are $0$ , and the inequality reduces to $0 \le$ (a nonnegative number).

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–Chevet bound on the expected spectral norm of a scaled Gaussian matrix: E∥SΓT∥≤∥S∥∥T∥F+∥S∥F∥T∥\mathbb E\|S\Gamma T\|\le\|S\|\|T\|_F+\|S\|_F\|T\|E∥SΓT∥≤∥S∥∥T∥F​+∥S∥F​∥T∥

Gordon–Chevet bound on the expected spectral norm of a scaled Gaussian matrix: $\mathbb E\|S\Gamma T\|\le\|S\|\|T\|_F+\|S\|_F\|T\|$