GLS estimator is linear and unbiased: $(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W\,A=I$

Proved

LocalDistanceNetwork.gls_unbiased

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

least-squareslinear-algebrastatistics

Let $A\in\mathbb R^{m\times n}$ have full column rank and let $W\in\mathbb R^{m\times m}$ be symmetric positive definite. Then the GLS estimator matrix $L_W=(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W$ is a left inverse of $A$ :

L_W\,A=I_n .

Consequently, if the data satisfy $Y=AX_0+\varepsilon$ with $\mathbb E[\varepsilon]=0$ , then $\mathbb E[L_WY]=X_0$ : the GLS estimator is a linear unbiased estimator, one half of the "Best Linear Unbiased Estimator" property invoked in Appendix B.

Preamble

import Mathlib
import Definitions.Def_LocalDistanceNetwork_GLS

open Matrix

Formal statement

namespace LocalDistanceNetwork
theorem gls_unbiased {m n : Type*} [Fintype m] [Fintype n] [DecidableEq n]
    (A : Matrix m n ℝ) (hA : Function.Injective A.mulVec)
    (W : Matrix m m ℝ) (hW : W.PosDef) :
    glsEstimatorMatrix A W * A = 1 := 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

GLS estimator is linear and unbiased: (ATWA)−1ATW A=I(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W\,A=I(ATWA)−1ATWA=I

GLS estimator is linear and unbiased: $(A^{\mathsf T}WA)^{-1}A^{\mathsf T}W\,A=I$