Tropp–Webber spectral second moment: $(\mathbb E\|S\Gamma T\|^2)^{1/2}\le\|S\|\|T\|_F+\|S\|_F\|T\|$

Proved

GaussianMatrix.spectral_second_moment

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\|^2$ is integrable and

\bigl(\mathbb E\,\|S\,\Gamma\,T\|^2\bigr)^{1/2}\ \le\ \|S\|\,\|T\|_F+\|S\|_F\,\|T\| ,

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

This is the second-moment version of the Gordon–Chevet bound (Tropp–Webber Lemma B.1); it is the form needed when spectral-norm errors are analyzed in mean square, e.g. for the core-noise and range-residual terms of truncated sketching algorithms, where it is combined with the inverse moments $\mathbb E\|G^{\dagger}\|^2$ and $\mathbb E\|G^{\dagger}\|_F^2$ .

Formalization Note. The bound is stated in the equivalent squared form $\mathbb E\|S\Gamma T\|^2\le(\|S\|\|T\|_F+\|S\|_F\|T\|)^2$ , together with integrability of the integrand.

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem spectral_second_moment {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) ^ 2) (gaussianMatrix p m) ∧
    ∫ 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, R. J. Webber, *Randomized algorithms for low-rank matrix approximation: design, analysis, and applications*, 2023, https://arxiv.org/abs/2306.12418 (v1), Appendix B p. 47, Lemma B.1 (Moment bounds), first upper bound:

(\mathbb E\|SGT\|^2)^{1/2}\le\|S\|\|T\|_F+\|T\|\|S\|_F

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 may be $0$ ), let $S$ be an arbitrary $a \times p$ real matrix and $T$ an arbitrary $m \times n$ real matrix, with no hypotheses 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 when $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) and $\|M\|_F := \sqrt{\sum_{i,j} M_{ij}^2}$ for its Frobenius norm. The statement asserts the conjunction of

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

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

Here the squares are ordinary real squares (natural-number exponent $2$ ). The integral is the Lebesgue integral (equal to $0$ by convention for a non-integrable integrand, which item 1 excludes). If any of $a, p, m, n$ is $0$ the relevant matrices are empty, their norms are $0$ , and the inequality reads $0 \le (\text{nonnegative})^2$ . Nothing is asserted about the first moment or about any relation between this bound and the mean of $\|SGT\|_{\mathrm{op}}$ .

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

Tropp–Webber spectral second moment: (E∥SΓT∥2)1/2≤∥S∥∥T∥F+∥S∥F∥T∥(\mathbb E\|S\Gamma T\|^2)^{1/2}\le\|S\|\|T\|_F+\|S\|_F\|T\|(E∥SΓT∥2)1/2≤∥S∥∥T∥F​+∥S∥F​∥T∥

Tropp–Webber spectral second moment: $(\mathbb E\|S\Gamma T\|^2)^{1/2}\le\|S\|\|T\|_F+\|S\|_F\|T\|$