Fourth Frobenius moment of a pseudo-inverted Gaussian matrix: $\mathbb E\|G^{\dagger}\|_F^4=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)}$

Proved

GaussianMatrix.pinv_frobenius_fourth_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 $r\le k-4$ and $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$ . Then $\|G^{\dagger}\|_F^4$ is integrable and

\mathbb E\,\|G^{\dagger}\|_F^4=\mathbb E\bigl[\operatorname{tr}(GG^{\mathsf T})^{-1}\bigr]^2=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)} .

Since $(GG^{\mathsf T})^{-1}$ is positive semidefinite, $\operatorname{tr}(GG^{\mathsf T})^{-1}=\|(GG^{\mathsf T})^{-1}\|_*$ is its nuclear (Schatten-1) norm, so this is the second moment of the nuclear norm of an inverse-Wishart matrix, Tropp–Webber Lemma B.2. Combined with the mean $r/(k-r-1)$ it gives the variance of $\|G^{\dagger}\|_F^2$ , which is what deviation bounds for the Frobenius error of the randomized SVD require.

Formalization Note. The left side is written as $\|G^{\dagger}\|_F^4=(\|G^{\dagger}\|_F^2)^2$ with $G^{\dagger}$ = pinvR; on the null set where $GG^{\mathsf T}$ is singular pinvR is $0$ , which does not affect the integral.

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

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

Source

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 (Inverse moment bounds), second formula:

\mathbb E\|(GG^*)^{-1}\|_*^2=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)}

for

r\le k-4

, using

\|(GG^*)^{-1}\|_*=\operatorname{tr}(GG^*)^{-1}=\|G^\dagger\|_F^2

(cf. 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), Appendix A.2 p. 65, proof of Proposition A.5).

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}(GG^{\top})^{-1}$ , a $k\times r$ real matrix (the bundle's pinvR; it is the zero matrix when $GG^{\top}$ is singular), and $\|A\|_F^2 := \sum_i\sum_j A_{ij}^2$ (the bundle's frobSq).

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

Integrability. The function $G\mapsto \big(\|G^{\dagger}\|_F^{2}\big)^{2} = \|G^{\top}(GG^{\top})^{-1}\|_F^{4}$ is integrable with respect to $\mu_{r,k}$ (the outer square is the natural-number power $2$ ).
Value.

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

with $r,k$ cast to $\mathbb{R}$ . Under $k\ge r+4$ the three factors $k-r$ , $k-r-1$ , $k-r-3$ are at least $4$ , $3$ , $1$ respectively, so the denominator is positive and the division is ordinary.

Edge cases. The integral is the real Bochner integral (returning $0$ for non-integrable integrands, but part 1 asserts integrability). When $r = 0$ the integrand is identically $0$ (empty sum) and the right-hand side is $\frac{0 - 0}{(k)(k-1)(k-3)} = 0$ ; the hypothesis is then $4\le k$ . When $r = 1$ the numerator is $k-1$ .

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

Fourth Frobenius moment of a pseudo-inverted Gaussian matrix: E∥G†∥F4=r2(k−r)−2r(r−1)(k−r)(k−r−1)(k−r−3)\mathbb E\|G^{\dagger}\|_F^4=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)}E∥G†∥F4​=(k−r)(k−r−1)(k−r−3)r2(k−r)−2r(r−1)​

Fourth Frobenius moment of a pseudo-inverted Gaussian matrix: $\mathbb E\|G^{\dagger}\|_F^4=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)}$