$\|(AA^\top)^{-1}\|=1/\sigma_{\min}(A^\top)^2$ (with Mathlib's conventions $0^{-1}=0$)

Let $A$ be a real $r\times k$ matrix, let $\sigma_{\min}(A^\top)=\inf_{x\in\mathbb R^r,\ \|x\|_2=1}\|A^\top x\|_2$ be the smallest singular value of $A^\top$, and let $\|\cdot\|$ be the spectral ($\ell_2\to\ell_2$ operator) norm. Then

with the conventions that the inverse of a singular matrix is $0$ and $1/0=0$.

When $AA^\top$ is invertible this is the statement $\|M^{-1}\|=1/\lambda_{\min}(M)$ for the positive definite matrix $M=AA^\top$, using $\lambda_{\min}(AA^\top)=\min_{\|x\|=1}\|A^\top x\|^2$. When $AA^\top$ is singular, some unit vector $x$ satisfies $A^\top x=0$, so both sides are $0$. It lets you restate any bound on $\lambda_{\min}(GG^\top)$ as a bound on $\|(GG^\top)^{-1}\|$.

Formalization Note. specNorm is Mathlib's $\ell_2$ operator norm on matrices and ⁻¹ is Mathlib's total matrix inverse, which is $0$ on singular input. sMin is the infimum over the unit sphere, which is $0$ when $r=0$ (empty sphere). Because Lean has $1/0=0$, the identity holds for every $A$ with no hypothesis, including $r=0$.