Prove2Me

For g∼N(0,Ik)g\sim\mathcal{N}(0,I_k) and fixed full-row-rank HH, HgHg is independent of the squared residual ∥(I−PH)g∥2\|(I-P_H)g\|^2

Proved
GaussianMatrix.regression_residual_indep

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

chi-squaregaussianindependenceprobabilityrandom-matrices

Let H∈Rn×kH \in \mathbb{R}^{n\times k} be a fixed matrix with rank⁡H=n\operatorname{rank} H = n, so that HH⊤HH^\top is invertible, and let g∼N(0,Ik)g \sim \mathcal{N}(0, I_k) have independent standard normal coordinates. Define the squared residual

QH(g)  =  g⊤g−(Hg)⊤(HH⊤)−1(Hg)  =  ∥(I−PH) g∥22,PH=H⊤(HH⊤)−1H.Q_H(g) \;=\; g^\top g - (Hg)^\top (HH^\top)^{-1}(Hg) \;=\; \|(I-P_H)\,g\|_2^2, \qquad P_H = H^\top(HH^\top)^{-1}H.

Then the random vector Hg∈RnHg \in \mathbb{R}^n and the random variable QH(g)Q_H(g) are independent.

Indeed, if the columns of V∈Rk×(k−n)V\in\mathbb{R}^{k\times(k-n)} form an orthonormal basis of ker⁡H\ker H, then QH(g)=∥V⊤g∥2Q_H(g) = \|V^\top g\|^2, and the jointly Gaussian vectors HgHg and V⊤gV^\top g are uncorrelated because HV=0HV = 0, hence independent. In the analysis of an inverse Wishart matrix this makes the regression coefficients (HH⊤)−1Hg(HH^\top)^{-1}Hg of one row on the others independent of its residual, conditionally on the other rows.

Formalization Note. Independence is ProbabilityTheory.IndepFun with respect to the product measure Measure.pi fun _ => gaussianReal 0 1 on Fin k → ℝ.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem regression_residual_indep {n k : ℕ} (H : Matrix (Fin n) (Fin k) ℝ) (hH : H.rank = n) :
    IndepFun (fun g : Fin k → ℝ => H *ᵥ g)
      (fun g : Fin k → ℝ => g ⬝ᵥ g - (H *ᵥ g) ⬝ᵥ ((H * Hᵀ)⁻¹ *ᵥ (H *ᵥ g)))
      (Measure.pi fun _ : Fin k => gaussianReal 0 1) := by sorry

end GaussianMatrix
Source
standard fact: uncorrelated components of a Gaussian vector are independent; for g∼N(0,Ik)g \sim N(0,I_k) and a matrix VV with orthonormal columns spanning ker⁡H\ker H, Cov⁡(Hg,V⊤g)=HV=0\operatorname{Cov}(Hg, V^\top g) = HV = 0; see R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley 1982, Ch. 1 (multivariate normal distribution: independence of uncorrelated normal subvectors) [section from memory].

View graph