Prove2Me

Each diagonal entry of an inverse Wishart matrix is a reciprocal chi-square: ((GG⊤)−1)ii∼1/χk−r+12((GG^\top)^{-1})_{ii} \sim 1/\chi^2_{k-r+1}

Proved
GaussianMatrix.inverse_wishart_diag_law

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

chi-squaregaussianinverse-wishartprobabilityrandom-matriceswishart

Let 1≤r≤k1 \le r \le k and let G∈Rr×kG \in \mathbb{R}^{r\times k} be a standard Gaussian matrix, i.e. its rkrk entries are independent N(0,1)\mathcal{N}(0,1) random variables. Let W=GG⊤∈Rr×rW = GG^\top \in \mathbb{R}^{r\times r} be the associated Wishart matrix and fix a row index i∈{1,…,r}i \in \{1,\dots,r\}. Then the ii-th diagonal entry of W−1W^{-1} has the law of the reciprocal of a chi-square variable with k−r+1k-r+1 degrees of freedom:

(W−1)ii  =d  1Ξ,Ξ=∑j=1k−r+1xj2,x∼N(0,Ik−r+1).\big(W^{-1}\big)_{ii} \;\overset{d}{=}\; \frac{1}{\Xi}, \qquad \Xi = \sum_{j=1}^{k-r+1} x_j^2,\quad x \sim \mathcal{N}(0, I_{k-r+1}).

Equivalently, 1/(W−1)ii=∥(I−P−i)gi∥22∼χk−r+121/(W^{-1})_{ii} = \|(I-P_{-i})g_i\|_2^2 \sim \chi^2_{k-r+1}, where gig_i is the ii-th row of GG and P−iP_{-i} is the orthogonal projector onto the span of the other r−1r-1 rows. The proof combines the Schur-complement formula for a diagonal entry of an inverse, the fact that the other r−1r-1 rows are almost surely linearly independent, and the rotation invariance of the Gaussian row gig_i, which is independent of the other rows (Fubini over rows).

This identifies the law of each summand in ∥G†∥F2=tr⁡(W−1)=∑i(W−1)ii\|G^\dagger\|_F^2 = \operatorname{tr}(W^{-1}) = \sum_i (W^{-1})_{ii}; together with LqL^q bounds for reciprocal chi-square variables it yields tail bounds for the Frobenius norm of a pseudo-inverted Gaussian matrix.

Formalization Note. Laws are push-forward measures on R\mathbb{R} (Measure.map). Lean's matrix inverse is total (A−1=0A^{-1}=0 for singular AA) and 0−1=00^{-1}=0, so both maps are defined everywhere; the singular events are null. The hypothesis r≤kr \le k is needed: for r=k+1r = k+1 the natural-number expression k−r+1k-r+1 would equal 11, whereas WW is then singular.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem inverse_wishart_diag_law {r k : ℕ} (hrk : r ≤ k) (i : Fin r) :
    Measure.map (fun G : Fin r → Fin k → ℝ => (Matrix.of G * (Matrix.of G)ᵀ)⁻¹ i i)
        (gaussianMatrix r k)
      = Measure.map (fun x : Fin (k - r + 1) → ℝ => (∑ j, x j ^ 2)⁻¹)
        (Measure.pi fun _ : Fin (k - r + 1) => gaussianReal 0 1) := by sorry

end GaussianMatrix
Source
standard fact: if A∼Wr(k,I)A \sim W_r(k, I) with k≥rk \ge r, then 1/(A−1)ii∼χk−r+121/(A^{-1})_{ii} \sim \chi^2_{k-r+1}; see R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley 1982, Theorem 3.2.11 (with M=ei⊤M = e_i^\top); it is also the computation underlying N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: Probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2) (2011), 217–288 (arXiv:0909.4061), Proposition A.5.

View graph