Prove2Me

Inverse moment of the chi-square distribution: E[1/χd2]=1/(d−2)\mathbb{E}[1/\chi^2_d] = 1/(d-2) for d≥3d \ge 3

Proved
GaussianMatrix.inv_chi_square_moment

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

chi-squaregaussianmomentsprobability

Let d≥3d \ge 3 and let x=(x1,…,xd)x = (x_1, \dots, x_d) have independent standard normal coordinates, so that Ξ=∑j=1dxj2\Xi = \sum_{j=1}^d x_j^2 has the chi-square distribution with dd degrees of freedom. Then Ξ−1\Xi^{-1} is integrable and

E[Ξ−1]  =  ∫Rd(∑j=1dxj2)−1 dγd(x)  =  Γ(d/2−1)2 Γ(d/2)  =  1d−2,\mathbb{E}\big[\Xi^{-1}\big] \;=\; \int_{\mathbb{R}^d} \Big(\sum_{j=1}^d x_j^2\Big)^{-1} \, d\gamma_d(x) \;=\; \frac{\Gamma(d/2 - 1)}{2\,\Gamma(d/2)} \;=\; \frac{1}{d-2},

where γd\gamma_d is the standard Gaussian measure on Rd\mathbb{R}^d.

This one-dimensional density computation supplies the constant 1/(k−r−1)1/(k-r-1) in the formula E(GG⊤)−1=I/(k−r−1)\mathbb{E}(GG^\top)^{-1} = I/(k-r-1) for an r×kr \times k standard Gaussian matrix, applied with d=k−r+1d = k - r + 1 degrees of freedom.

Formalization Note. Since Lean's 0−1=00^{-1} = 0, the integrand is defined everywhere; the event Ξ=0\Xi = 0 is Gaussian-null anyway. The hypothesis d≥3d \ge 3 is sharp: for d≤2d \le 2 the integral diverges.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem inv_chi_square_moment {d : ℕ} (hd : 3 ≤ d) :
    Integrable (fun x : Fin d → ℝ => (∑ j, x j ^ 2)⁻¹)
        (Measure.pi fun _ : Fin d => gaussianReal 0 1) ∧
    ∫ x, (∑ j, x j ^ 2)⁻¹ ∂(Measure.pi fun _ : Fin d => gaussianReal 0 1) = 1 / ((d : ℝ) - 2) := by sorry

end GaussianMatrix
Source
N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness, SIAM Review 53(2), 2011, Proposition A.8 (and the proof of Proposition A.5).

View graph