Prove2Me

Chevet–Gordon bound: E∥SGT∥≤∥S∥∥T∥F+∥S∥F∥T∥\mathbb E\|SGT\|\le\|S\|\|T\|_F+\|S\|_F\|T\| for a standard Gaussian matrix GG

Proved
GaussianMatrix.chevet_expectation_bound

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

chevet-inequalitygaussian-matrixrandom-matricesrandomized-svdspectral-norm

Let S∈Ra×pS\in\mathbb R^{a\times p} and T∈Rm×nT\in\mathbb R^{m\times n} be fixed matrices, and let GG be a p×mp\times m random matrix with independent standard normal entries. Write ∥⋅∥\|\cdot\| for the spectral norm and ∥⋅∥F\|\cdot\|_F for the Frobenius norm. Then

E ∥SGT∥  ≤  ∥S∥ ∥T∥F+∥S∥F ∥T∥.\mathbb E\,\|SGT\|\;\le\;\|S\|\,\|T\|_F+\|S\|_F\,\|T\| .

This sharp-constant form of Chevet's inequality is used in the analysis of randomized range finders (randomized SVD), where it controls the error term ∥Σ2Ω2Ω1†∥\|\Sigma_2\Omega_2\Omega_1^\dagger\|. Note that it does not follow from the Sudakov–Fernique inequality with the naive comparison process when the index sets are ellipsoids rather than spheres. It also follows from the second-moment bound spectral_second_moment_bound by Cauchy–Schwarz.

Formalization Note. The law of GG is gaussianMatrix p m, and the matrix is S * Matrix.of G * T. All dimensions may be zero. The integrand is integrable (∥S∥∥T∥\|S\|\|T\|-Lipschitz for the Frobenius norm).

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem chevet_expectation_bound {a p m n : ℕ} (S : Matrix (Fin a) (Fin p) ℝ)
    (T : Matrix (Fin m) (Fin n) ℝ) :
    ∫ 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', SIAM Review 53(2) (2011), Proposition 10.1 (numbering from memory), attributing the bound to Y. Gordon (Israel J. Math. 50 (1985); Israel J. Math. 64 (1988)); see also S. Chevet (1978) for the inequality with non-sharp form.

View graph