Prove2Me

Second-moment Chevet bound: E∥SGT∥2≤(∥S∥∥T∥F+∥S∥F∥T∥)2\mathbb E\|SGT\|^2\le(\|S\|\|T\|_F+\|S\|_F\|T\|)^2

Proved
GaussianMatrix.spectral_second_moment_bound

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

chevet-inequalitygaussian-matrixrandom-matricesrandomized-svdsecond-moment

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∥2  ≤  (∥S∥ ∥T∥F+∥S∥F ∥T∥)2.\mathbb E\,\|SGT\|^2\;\le\;\big(\|S\|\,\|T\|_F+\|S\|_F\,\|T\|\big)^2 .

This strengthens the first-moment Chevet–Gordon bound: by Cauchy–Schwarz it implies E∥SGT∥≤∥S∥∥T∥F+∥S∥F∥T∥\mathbb E\|SGT\|\le\|S\|\|T\|_F+\|S\|_F\|T\|. It is used in the mean-square error analysis of the randomized SVD. It does not follow from the first-moment bound combined with Gaussian concentration: that route only gives (∥S∥∥T∥F+∥S∥F∥T∥)2+∥S∥2∥T∥2(\|S\|\|T\|_F+\|S\|_F\|T\|)^2+\|S\|^2\|T\|^2.

Formalization Note. The integrand ∥S of(G) T∥2\|S\,\mathrm{of}(G)\,T\|^2 is integrable, since it is the square of a Lipschitz function of a Gaussian matrix, so the Bochner-integral convention plays no role. All dimensions may be zero.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem spectral_second_moment_bound {a p m n : ℕ} (S : Matrix (Fin a) (Fin p) ℝ)
    (T : Matrix (Fin m) (Fin n) ℝ) :
    ∫ G, specNorm (S * Matrix.of G * T) ^ 2 ∂(gaussianMatrix p m)
      ≤ (specNorm S * frobNorm T + frobNorm S * specNorm T) ^ 2 := by sorry

end GaussianMatrix
Source
J. A. Tropp and R. J. Webber, 'Randomized algorithms for low-rank matrix approximation: Design, analysis, and applications', arXiv:2306.12418 (2023), Lemma B.1 (first upper bound; proof in Appendix B, p. 47) — lemma number as cited in the task; obtained there by a Gaussian comparison argument.

View graph