Prove2Me

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

Proved
GaussianMatrix.inv_sq_chi_square_moment

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

chi-squaregaussianmomentsprobability

Let d≥5d \ge 5 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 Ξ−2\Xi^{-2} is integrable and

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

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

This is the second inverse moment of the chi-square law. Applied with d=k−r+1d = k-r+1 degrees of freedom it yields E[((GG⊤)−1)ii2]=1/((k−r−1)(k−r−3))\mathbb{E}\big[((GG^\top)^{-1})_{ii}^2\big] = 1/((k-r-1)(k-r-3)) for an r×kr\times k standard Gaussian matrix GG, the diagonal ingredient of the second moments of the inverse Wishart matrix.

Formalization Note. The integrand is written ((∑ j, x j ^ 2)⁻¹) ^ 2; with Lean's convention 0−1=00^{-1} = 0 it is defined everywhere (the event Ξ=0\Xi = 0 is null). The hypothesis d≥5d \ge 5 is sharp: for d≤4d \le 4 the integral diverges.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

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

end GaussianMatrix
Source
standard fact: for Ξ∼χd2\Xi \sim \chi^2_d and s<d/2s < d/2, E[Ξ−s]=Γ(d/2−s)/(2s Γ(d/2))\mathbb{E}[\Xi^{-s}] = \Gamma(d/2 - s)/(2^s\,\Gamma(d/2)); see N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, Vol. 1, 2nd ed., Wiley 1994, Ch. 18 (moments of the chi-square distribution) [chapter cited from memory]; the case s=1s=1 is Halko–Martinsson–Tropp, SIAM Review 53(2), 2011, Appendix A.

View graph