Generalized least squares

DefinitionGeneralized least-squares matrix#✓fully proved

The generalized least-squares matrix (Xᵀ V⁻¹ X)⁻¹ Xᵀ V⁻¹; glsMatrix X V *ᵥ y is the GLS estimate of b in y = X b + e with Cov e = V.

noncomputable def glsMatrix (X : Matrix m k ℝ) (V : Matrix m m ℝ) : Matrix k m ℝ :=
  (Xᵀ * V⁻¹ * X)⁻¹ * Xᵀ * V⁻¹

Used by 5

Used byThe MME solution is the GLS estimate and the BLUP · Henderson's mixed-model equations give the GLS estimator and the BLUP · Aitken's theorem · Covariance of the generalized least-squares estimator · Unbiasedness of the generalized least-squares estimator

TheoremUnbiasedness of the generalized least-squares estimator#✓fully proved

The GLS estimator is unbiased: B X = 1 when Xᵀ V⁻¹ X is invertible.

theorem glsMatrix_mul_self (hX : IsUnit (Xᵀ * V⁻¹ * X)) : glsMatrix X V * X = 1

Uses 1 · Used by 1

Statement usesGeneralized least-squares matrix

Used byAitken's theorem

TheoremCovariance of the generalized least-squares estimator#✓fully proved

The covariance of the GLS estimator: B V Bᵀ = (Xᵀ V⁻¹ X)⁻¹.

theorem glsMatrix_mul_mul_transpose (hV : V.PosDef) (hX : IsUnit (Xᵀ * V⁻¹ * X)) :
    glsMatrix X V * V * (glsMatrix X V)ᵀ = (Xᵀ * V⁻¹ * X)⁻¹

Uses 1

Statement usesGeneralized least-squares matrix

TheoremAitken's theorem#✓fully proved

The GLS estimator has minimal covariance among linear unbiased estimators: for every A with A X = 1, A V Aᵀ - B V Bᵀ is positive semidefinite, where B = glsMatrix X V.

theorem aitken (hV : V.PosDef) (hX : IsUnit (Xᵀ * V⁻¹ * X)) (A : Matrix k m ℝ)
    (hA : A * X = 1) :
    (A * V * Aᵀ - glsMatrix X V * V * (glsMatrix X V)ᵀ).PosSemidef

Uses 2

Statement usesGeneralized least-squares matrix

Proof usesUnbiasedness of the generalized least-squares estimator

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.