Second Frobenius moment of an inverse-Wishart matrix: $\mathbb E\|(GG^{\mathsf T})^{-1}\|_F^2=\frac{r(k-1)}{(k-r)(k-r-1)(k-r-3)}$

Proved

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

\mathbb E\,\bigl\|(GG^{\mathsf T})^{-1}\bigr\|_F^2=\frac{r(k-1)}{(k-r)(k-r-1)(k-r-3)} .

This is the squared Frobenius norm of the inverse-Wishart matrix $W^{-1}$ , $W=GG^{\mathsf T}\sim\mathrm{Wishart}_r(k,I)$ ; it is the companion of the nuclear-norm second moment and follows from the second-order moments $\mathbb E[(W^{-1})_{ij}(W^{-1})_{kl}]$ of the inverse-Wishart distribution. Since $\|(GG^{\mathsf T})^{-1}\|_F^2=\|G^{\dagger}(G^{\dagger})^{\mathsf T}\|_F^2$ , it controls the fourth moments of the singular values of $G^{\dagger}$ .

Formalization Note. Mathlib's inverse is total ( $0$ on the singular null set), which does not affect the integral; the conclusion is the conjunction of integrability and the identity.

Preamble

import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix

Formal statement

namespace GaussianMatrix
theorem inverse_wishart_frobenius_moment {r k : ℕ} (hrk : r + 4 ≤ k) :
    Integrable (fun G : Fin r → Fin k → ℝ => frobSq (Matrix.of G * (Matrix.of G)ᵀ)⁻¹)
      (gaussianMatrix r k) ∧
    ∫ G, frobSq (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ ∂(gaussianMatrix r k)
      = (r : ℝ) * ((k : ℝ) - 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), third formula:

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

for

r\le k-4

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. Write $\|A\|_F^2 := \sum_i\sum_j A_{ij}^2$ for the bundle's frobSq.

Statement. Let $r,k$ be natural numbers with $r+4\le k$ , and let $W = GG^{\top}$ be the $r\times r$ Gram matrix of a sample $G$ . The theorem asserts the conjunction of:

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

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

with $r,k$ cast to $\mathbb{R}$ . Since $k\ge r+4$ , the factors $k-r$ , $k-r-1$ , $k-r-3$ are all at least $1$ , so the denominator is positive.

Edge cases. The integral is Lean's real Bochner integral (which is $0$ for non-integrable integrands; part 1 asserts integrability). On the null set where $GG^{\top}$ is singular, the inverse is the zero matrix and the integrand is $0$ . When $r=0$ the sum is empty, the integrand is identically $0$ , and the right-hand side is $0$ ; the hypothesis is then $4\le 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

Second Frobenius moment of an inverse-Wishart matrix: E∥(GGT)−1∥F2=r(k−1)(k−r)(k−r−1)(k−r−3)\mathbb E\|(GG^{\mathsf T})^{-1}\|_F^2=\frac{r(k-1)}{(k-r)(k-r-1)(k-r-3)}E∥(GGT)−1∥F2​=(k−r)(k−r−1)(k−r−3)r(k−1)​

Second Frobenius moment of an inverse-Wishart matrix: $\mathbb E\|(GG^{\mathsf T})^{-1}\|_F^2=\frac{r(k-1)}{(k-r)(k-r-1)(k-r-3)}$