Expected spectral norm of a Gaussian matrix: $\mathbb E\|G\|\le\sqrt N+\sqrt n$

Let $G$ be an $N\times n$ random matrix with independent standard normal entries, and let $\|G\|=\max_{\|x\|_2=1}\|Gx\|_2$ be its spectral norm (largest singular value). Then

This is the upper half of Gordon's theorem for Gaussian matrices. It is the input for the deviation bound $\mathbb P\{\|G\|\ge\sqrt N+\sqrt n+t\}\le e^{-t^2/2}$, and for the upper half of the conjunction gordon. It follows from the Sudakov–Fernique inequality by comparing $\langle Gu,v\rangle$ with $\langle g,u\rangle+\langle h,v\rangle$ on finite nets of the unit spheres.

Formalization Note. The law of $G$ is gaussianMatrix N n, and specNorm is Mathlib's $\ell_2\to\ell_2$ operator norm. No hypothesis on $N,n$ is needed: for $N=0$ or $n=0$ the norm is identically $0$. The integrand is integrable (it is $1$-Lipschitz for the Frobenius norm), so the Bochner-integral convention for non-integrable functions plays no role.