Prove2Me

Eq. (B.2) claim — the weight W=C−1W=C^{-1} gives the lowest variance

Proved
LocalDistanceNetwork.optimal_weight_inverse_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, let the data covariance C∈Rm×mC\in\mathbb R^{m\times m} be symmetric positive definite, and let W∈Rm×mW\in\mathbb R^{m\times m} be any symmetric positive-definite weight matrix. Write LW=(ATWA)−1ATWL_W=(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W for the minimizer of the quadratic form (B.2) with weight WW. Then

LW C LWT−LC−1 C LC−1T  is positive semidefinite.L_W\,C\,L_W^{\mathsf T}-L_{C^{-1}}\,C\,L_{C^{-1}}^{\mathsf T}\ \text{ is positive semidefinite.}

In words: among all weighted least-squares solutions, the one weighted by the inverse covariance matrix has the smallest covariance (in the Loewner order), which justifies using the χ2\chi^2 of Eq. (B.1) rather than any other weighting.

Preamble
import Mathlib
import Definitions.Def_LocalDistanceNetwork_GLS

open Matrix
Formal statement
namespace LocalDistanceNetwork
theorem optimal_weight_inverse_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)
    (W : Matrix m m ℝ) (hW : W.PosDef) :
    (linearEstimatorCov (glsEstimatorMatrix A W) C
      - linearEstimatorCov (glsEstimatorMatrix A C⁻¹) C).PosSemidef := 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