Prove2Me

Covariance of the χ2\chi^2 estimator is (ATC−1A)−1(A^{\mathsf T}C^{-1}A)^{-1}

Proved
LocalDistanceNetwork.gls_covariance

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

least-squareslinear-algebrastatistics

Let A∈Rm×nA\in\mathbb R^{m\times n} have full column rank and let the data covariance matrix C∈Rm×mC\in\mathbb R^{m\times m} be symmetric positive definite. Let L=(ATC−1A)−1ATC−1L=(A^{\mathsf T}C^{-1}A)^{-1}A^{\mathsf T}C^{-1} be the estimator matrix of the χ2\chi^2 minimization (weight W=C−1W=C^{-1}). Then the covariance matrix of the estimate LYLY is

L C LT=(ATC−1A)−1.L\,C\,L^{\mathsf T}=(A^{\mathsf T}C^{-1}A)^{-1}.

This is the parameter covariance matrix that the solution procedure reports, from which the uncertainty on log⁡10H0\log_{10}H_0 is read off.

Preamble
import Mathlib
import Definitions.Def_LocalDistanceNetwork_GLS

open Matrix
Formal statement
namespace LocalDistanceNetwork
theorem gls_covariance {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (A : Matrix m n ℝ) (hA : Function.Injective A.mulVec)
    (C : Matrix m m ℝ) (hC : C.PosDef) :
    linearEstimatorCov (glsEstimatorMatrix A C⁻¹) C = (Aᵀ * C⁻¹ * A)⁻¹ := by sorry
end LocalDistanceNetwork
Source
H0DN Collaboration (S. Casertano et al.), The Local Distance Network: A community consensus report on the measurement of the Hubble constant at ~1% precision, A&A 708, A166 (2026), https://doi.org/10.1051/0004-6361/202557993, Appendix B (p. 34) and Appendix B.2 (pp. 34-35), Eqs. (B.1)-(B.2)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph