Prove2Me

Second moment of a diagonal entry of the inverse Wishart matrix: E[((GG⊤)−1)ii2]=1/((k−r−1)(k−r−3))\mathbb{E}[((GG^\top)^{-1})_{ii}^2] = 1/((k-r-1)(k-r-3))

Proved
GaussianMatrix.inverse_wishart_diag_sq_moment

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

gaussianinverse-wishartmomentsrandom-matriceswishart

Let r,kr, k be natural numbers with r+4≤kr + 4 \le k, let G∈Rr×kG \in \mathbb{R}^{r\times k} have independent N(0,1)\mathcal{N}(0,1) entries, and let W=GG⊤W = GG^\top be the corresponding (real, identity-covariance) Wishart matrix with kk degrees of freedom. For every index i∈{1,…,r}i \in \{1,\dots,r\} the squared diagonal entry ((W−1)ii)2((W^{-1})_{ii})^2 is integrable and

E[((GG⊤)−1)ii 2]  =  1(k−r−1)(k−r−3).\mathbb{E}\Big[\big((GG^\top)^{-1}\big)_{ii}^{\,2}\Big] \;=\; \frac{1}{(k-r-1)(k-r-3)}.

Indeed ((GG⊤)−1)ii=1/∥(I−P−i)gi∥2((GG^\top)^{-1})_{ii} = 1/\|(I-P_{-i})g_i\|^2, where gig_i is the ii-th row and P−iP_{-i} the projector onto the span of the other rows, and conditionally on those rows the squared residual is χk−r+12\chi^2_{k-r+1}; the claim is then E[(χd2)−2]=1/((d−2)(d−4))\mathbb{E}[(\chi^2_d)^{-2}] = 1/((d-2)(d-4)) with d=k−r+1d = k-r+1. This is the diagonal term α\alpha in the second-moment formulas E[(tr⁡W−1)2]=rα+r(r−1)β\mathbb{E}[(\operatorname{tr} W^{-1})^2] = r\alpha + r(r-1)\beta and E∥W−1∥F2=rα+r(r−1)γ\mathbb{E}\|W^{-1}\|_F^2 = r\alpha + r(r-1)\gamma.

Formalization Note. Lean's matrix inverse is total (A−1=0A^{-1} = 0 for singular AA); since GG⊤GG^\top is almost surely invertible this does not affect the value. The hypothesis r+4≤kr+4 \le k is exactly the integrability threshold.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem inverse_wishart_diag_sq_moment {r k : ℕ} (hrk : r + 4 ≤ k) (i : Fin r) :
    Integrable (fun G : Fin r → Fin k → ℝ => (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ i i ^ 2)
      (gaussianMatrix r k) ∧
    ∫ G, (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ i i ^ 2 ∂(gaussianMatrix r k)
      = 1 / (((k : ℝ) - r - 1) * ((k : ℝ) - r - 3)) := by sorry

end GaussianMatrix
Source
standard fact (second moments of the inverse Wishart matrix): for W∼Wr(k,I)W \sim W_r(k, I), E[(W−1)ij(W−1)kl]=(k−r−2)δijδkl+δikδjl+δilδjk(k−r)(k−r−1)(k−r−3)\mathbb{E}[(W^{-1})_{ij}(W^{-1})_{kl}] = \frac{(k-r-2)\delta_{ij}\delta_{kl} + \delta_{ik}\delta_{jl} + \delta_{il}\delta_{jk}}{(k-r)(k-r-1)(k-r-3)}; see A. K. Gupta and D. K. Nagar, Matrix Variate Distributions, Chapman & Hall/CRC 2000, Thm. 3.4.3, and D. von Rosen, Moments for the inverted Wishart distribution, Scand. J. Statist. 15 (1988) 97–109; cf. R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley 1982, Sec. 3.2 (theorem numbers from memory). This is the case i=j=k=li=j=k=l.

View graph