Distance of a standard Gaussian vector to a fixed subspace: if $\operatorname{rank}B+d\le N$ then $\mathbb P\{\operatorname{dist}(g,\operatorname{col}B)^2\le u\}\le (eu/d)^{d/2}$

Let $g$ be a standard Gaussian vector in $\mathbb R^N$ (independent $N(0,1)$ coordinates) and let $B$ be a fixed real $N\times p$ matrix with column space $\operatorname{col}B\subseteq\mathbb R^N$. Let $d\ge1$ be an integer with $\operatorname{rank}B+d\le N$, and let

Then for every real $u$ with $0\le u\le d$,

Choose orthonormal vectors $w_1,\dots,w_d$ in $(\operatorname{col}B)^\perp$ (possible since its dimension is $N-\operatorname{rank}B\ge d$). By Bessel's inequality, $\|g-Bc\|^2\ge\sum_{k\le d}\langle w_k,g-Bc\rangle^2=\sum_{k\le d}\langle w_k,g\rangle^2$ for every $c$. By rotation invariance of the standard Gaussian, $(\langle w_k,g\rangle)_{k\le d}$ is a standard Gaussian vector in $\mathbb R^d$, so the probability is at most $\mathbb P\{\chi^2_d\le u\}\le(eu/d)^{d/2}$.

This is the fixed-subspace ingredient for small-ball estimates of the smallest singular value: applied conditionally on the other columns of a Gaussian matrix, it controls the distance of one column to the span of the others.

Formalization Note. The law of $g$ is Measure.pi fun _ : Fin N => gaussianReal 0 1; $\|v\|_2$ is Real.sqrt (v ⬝ᵥ v); B.rank is Mathlib's Matrix.rank. The case $p=0$ (trivial subspace) is included.