Norms of Gaussian vectors: $\mathbb E\|h_N\|_2-\mathbb E\|g_n\|_2\ge\sqrt N-\sqrt n$ for $1\le n\le N$

Let $1\le n\le N$ be integers. Let $h$ be a standard Gaussian vector in $\mathbb R^N$ and $g$ a standard Gaussian vector in $\mathbb R^n$, each with independent $N(0,1)$ coordinates, and let $\|\cdot\|_2$ be the Euclidean norm. Then

Equivalently, $m\mapsto \mathbb E\|g_m\|_2-\sqrt m$ is nondecreasing on $m\ge1$, where $g_m$ is standard Gaussian in $\mathbb R^m$.

This is the elementary input that turns Gordon's bound $\mathbb E\,\sigma_{\min}(G)\ge\mathbb E\|h_N\|_2-\mathbb E\|g_n\|_2$ into the familiar $\mathbb E\,\sigma_{\min}(G)\ge\sqrt N-\sqrt n$. Note that $\mathbb E\|h_N\|_2\le\sqrt N$, so the inequality is not a consequence of Jensen's inequality. It is sharp to second order: with $a_m=\mathbb E\|g_m\|_2$, the gap $(a_{m+1}-a_m)-(\sqrt{m+1}-\sqrt m)$ is of order $m^{-3/2}/8$. One proof uses $a_m=\sqrt2\,\Gamma(\tfrac{m+1}2)/\Gamma(\tfrac m2)$, hence $a_m a_{m+1}=m$, together with log-convexity of $\Gamma$ and a monotone-ratio argument that yields $a_m^2\le m-\tfrac12+\tfrac{3}{20m}$.

Formalization Note. The law of $h$ is Measure.pi fun _ : Fin N => gaussianReal 0 1, and $\|x\|_2$ is written $\sqrt{\sum_i x_i^2}$. The hypothesis $n\ge1$ is necessary: for $n=0$ the claim would read $\sqrt N\le\mathbb E\|h_N\|_2$, which is false for every $N\ge1$ (e.g. $\mathbb E\|h_1\|=\sqrt{2/\pi}<1$). The hypothesis $n\le N$ is also needed, since the inequality reverses for $N<n$. Both integrands are integrable.