Prove2Me

Mixed diagonal second moment of the inverse Wishart matrix: E[(W−1)ii(W−1)jj]=(k−r−2)/((k−r)(k−r−1)(k−r−3))\mathbb{E}[(W^{-1})_{ii}(W^{-1})_{jj}] = (k-r-2)/((k-r)(k-r-1)(k-r-3)), i≠ji\neq j

Proved
GaussianMatrix.inverse_wishart_diag_prod_moment

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

gaussianinverse-wishartmomentsrandom-matriceswishart

Let 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 W=GG⊤W = GG^\top. For distinct indices i≠ji \ne j the product (W−1)ii(W−1)jj(W^{-1})_{ii}(W^{-1})_{jj} is integrable and

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

This is the off-diagonal term β\beta in E[(tr⁡W−1)2]=∑i,jE[(W−1)ii(W−1)jj]=rα+r(r−1)β\mathbb{E}[(\operatorname{tr} W^{-1})^2] = \sum_{i,j}\mathbb{E}[(W^{-1})_{ii}(W^{-1})_{jj}] = r\alpha + r(r-1)\beta, i.e. in the fourth moment E∥G†∥F4\mathbb{E}\|G^\dagger\|_F^4 of the pseudoinverse. It follows from α=β+2γ\alpha = \beta + 2\gamma (rotation identity) with α=1/((k−r−1)(k−r−3))\alpha = 1/((k-r-1)(k-r-3)) and γ=1/((k−r)(k−r−1)(k−r−3))\gamma = 1/((k-r)(k-r-1)(k-r-3)).

Formalization Note. Lean's matrix inverse returns 00 on singular input; GG⊤GG^\top is a.s. invertible, so this does not affect the statement. Integrability is part of the conclusion.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem inverse_wishart_diag_prod_moment {r k : ℕ} (hrk : r + 4 ≤ k) (i j : Fin r) (hij : i ≠ j) :
    Integrable (fun G : Fin r → Fin k → ℝ =>
        (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ i i * (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ j j)
      (gaussianMatrix r k) ∧
    ∫ G, (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ i i * (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ j j
        ∂(gaussianMatrix r k)
      = ((k : ℝ) - r - 2) / (((k : ℝ) - r) * ((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)}; A. K. Gupta and D. K. Nagar, Matrix Variate Distributions, Chapman & Hall/CRC 2000, Thm. 3.4.3; D. von Rosen, 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\ne k=l.

View graph