Prove2Me

Variance of a linear estimate: Var⁡(vTLY)=vTLCLTv\operatorname{Var}(v^{\mathsf T}LY)=v^{\mathsf T}LCL^{\mathsf T}v

Proved
LocalDistanceNetwork.variance_linear_estimator

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

least-squareslinear-algebrastatistics

Let (Ω,F,μ)(\Omega,\mathcal F,\mu) be a probability space and let ε=(ε1,…,εm)\varepsilon=(\varepsilon_1,\dots,\varepsilon_m) be a random vector whose components are square integrable, with covariances Cov⁡(εi,εj)=Cij\operatorname{Cov}(\varepsilon_i,\varepsilon_j)=C_{ij} for a matrix C∈Rm×mC\in\mathbb R^{m\times m}. Let Y=AX0+εY=AX_0+\varepsilon for a matrix A∈Rm×nA\in\mathbb R^{m\times n} and a vector X0∈RnX_0\in\mathbb R^{n}. Then for every matrix L∈Rn×mL\in\mathbb R^{n\times m} and every vector v∈Rnv\in\mathbb R^{n},

Var⁡(vTLY)=vT (L C LT) v.\operatorname{Var}\big(v^{\mathsf T}LY\big)=v^{\mathsf T}\,\big(L\,C\,L^{\mathsf T}\big)\,v .

This connects the matrix LCLTLCL^{\mathsf T} used in the matrix-form statements with the variance of the random estimate LYLY, so that Loewner-order comparisons of covariance matrices become comparisons of variances.

Preamble
import Mathlib
import Definitions.Def_LocalDistanceNetwork_GLS

open Matrix
open MeasureTheory ProbabilityTheory
Formal statement
namespace LocalDistanceNetwork
theorem variance_linear_estimator {m n : Type*} [Fintype m] [Fintype n]
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (C : Matrix m m ℝ) (ε : Ω → m → ℝ)
    (hε : ∀ i, MemLp (fun ω => ε ω i) 2 μ)
    (hcov : ∀ i j, cov[fun ω => ε ω i, fun ω => ε ω j; μ] = C i j)
    (A : Matrix m n ℝ) (X₀ : n → ℝ) (L : Matrix n m ℝ) (v : n → ℝ) :
    Var[fun ω => v ⬝ᵥ (L *ᵥ (A *ᵥ X₀ + ε ω)); μ] = v ⬝ᵥ (linearEstimatorCov L C *ᵥ v) := 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