Expected squared Frobenius norm of a pseudo-inverted Gaussian matrix: $\mathbb E\|G^{\dagger}\|_F^2=\frac{r}{k-r-1}$

Proved

GaussianMatrix.pinv_frobenius_moment

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

gaussian-matrixprobabilityrandom-matrix-theoryrandomized-numerical-linear-algebra

Let $G\in\mathbb R^{r\times k}$ be a standard Gaussian matrix with $k-r\ge2$ , and let $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$ be its pseudoinverse. Then $\|G^{\dagger}\|_F^2$ is integrable and

\mathbb E\,\|G^{\dagger}\|_F^2=\frac{r}{k-r-1}.

In the notation of Halko–Martinsson–Tropp, $G$ is $k\times(k+p)$ and the right-hand side reads $k/(p-1)$ : this is the inverse moment that enters the expected Frobenius error bound $\bigl(1+\tfrac{k}{p-1}\bigr)^{1/2}\|\Sigma_2\|_F$ of the randomized SVD, and more generally every expected-error bound for Gaussian sketching with oversampling.

Formalization Note. $G^{\dagger}$ is pinvR, which is $0$ on the null set where $GG^{\mathsf T}$ is singular; the conclusion is the conjunction of integrability and the identity. No lower bound on $r$ is needed ( $r=0$ gives $0=0$ ).

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem pinv_frobenius_moment {r k : ℕ} (hrk : r + 2 ≤ k) :
    Integrable (fun G : Fin r → Fin k → ℝ => frobSq (pinvR (Matrix.of G))) (gaussianMatrix r k) ∧
    ∫ G, frobSq (pinvR (Matrix.of G)) ∂(gaussianMatrix r k) = (r : ℝ) / ((k : ℝ) - r - 1) := by sorry
end GaussianMatrix

Source

N. Halko, P.-G. Martinsson, J. A. Tropp, *Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions*, SIAM Review 53(2), 2011, https://arxiv.org/abs/0909.4061 (v2), §10.1 p. 55, Proposition 10.2 eq. (10.3) (

k\times(k+p)

p\ge2

) and Appendix A.2 p. 65, Proposition A.5 (

m\times n

n-m\ge2

\mathbb E\|G^\dagger\|_F^2=\frac{m}{n-m-1}

); also 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. 51, Lemma B.2 (trace of the first formula).

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Throughout, $\mu_{r,k}$ denotes the measure called gaussianMatrix r k: the product measure on the function space $\{0,\dots,r-1\}\times\{0,\dots,k-1\}\to\mathbb{R}$ in which every one of the $rk$ coordinates is an independent standard normal $\mathcal N(0,1)$ ; it is a probability measure, and a sample $G$ is viewed as the real $r\times k$ matrix with entries $G_{ij}$ . Matrix inversion $(\cdot)^{-1}$ is Mathlib's total inverse on square real matrices: it is the usual inverse when the determinant is nonzero and is the zero matrix otherwise. For an $r\times k$ matrix $G$ , write

G^{\dagger} \;:=\; G^{\top}\,\big(G G^{\top}\big)^{-1},

a $k\times r$ real matrix (this is the bundle's pinvR); when $GG^{\top}$ is singular, $G^{\dagger}$ is the zero $k\times r$ matrix. The bundle's frobSq of a matrix $A$ is $\sum_{i}\sum_{j} A_{ij}^{2} = \|A\|_F^{2}$ (the squared Frobenius norm), a sum over all entries.

Statement. Let $r,k$ be natural numbers with $r+2\le k$ . The theorem asserts the conjunction of:

Integrability. The function $G\mapsto \|G^{\dagger}\|_F^{2} = \sum_{i=0}^{k-1}\sum_{j=0}^{r-1}\big(G^{\top}(GG^{\top})^{-1}\big)_{ij}^{2}$ is integrable with respect to $\mu_{r,k}$ .
Value.

\int \big\|G^{\top}(GG^{\top})^{-1}\big\|_F^{2}\;d\mu_{r,k}(G) \;=\; \frac{r}{k - r - 1},

where $r$ , $k$ are cast to real numbers and $k-r-1\ge 1$ by the hypothesis, so the division is ordinary.

Edge cases. The integral is the real Bochner integral (which would be $0$ for a non-integrable integrand, but integrability is asserted in part 1). When $r=0$ the inner sum is empty, so the integrand is identically $0$ , and the right-hand side is $0/(k-1) = 0$ ; the hypothesis is then $2 \le k$ . The sum in frobSq runs over the $k\times r$ index set of $G^{\dagger}$ (not $r\times k$ ).

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

Expected squared Frobenius norm of a pseudo-inverted Gaussian matrix: E∥G†∥F2=rk−r−1\mathbb E\|G^{\dagger}\|_F^2=\frac{r}{k-r-1}E∥G†∥F2​=k−r−1r​

Expected squared Frobenius norm of a pseudo-inverted Gaussian matrix: $\mathbb E\|G^{\dagger}\|_F^2=\frac{r}{k-r-1}$