TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Known-covariance GLS is BLUE

Statement

Let the linear mixed model have fixed design $X \in R^{n \times p}$ of full column rank and known marginal covariance $V = Cov (Y) ≻ 0$ . Then ${\hat{β}}_{G L S} = (X^{T} V^{- 1} X)^{- 1} X^{T} V^{- 1} Y$ is unbiased for $β$ , has covariance $(X^{T} V^{- 1} X)^{- 1}$ , and is BLUE: for every linear unbiased estimator $\tilde{β}$ and every $c \in R^{p}$ , $Var (c^{T} {\hat{β}}_{G L S}) \leq Var (c^{T} \tilde{β}) .$ Only the fixed-design mean and covariance are used; Gaussianity is not assumed.

Facts & Assumptions

Given: The fixed-design mixed model, full-column-rank $X$ , known $V ≻ 0$ , and the estimator defined in Generalized least-squares estimator for known covariance.

[F1]

The fixed-design mean is $E_{β} Y = X β$ . Fixed-design linear regression model.

[F2]

The marginal covariance in the moment model is $V = Z G Z^{T} + R = Cov (Y)$ . Marginal covariance of the linear mixed model.

[F3]

A positive-definite $V$ has a Cholesky factorization $V = L L^{T}$ with $L$ invertible. A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique.

[F4]

In a full-rank fixed-design model with covariance $σ^{2} I$ for $σ^{2} > 0$ , OLS is unbiased and BLUE for every estimable contrast, without Gaussianity. Gauss–Markov theorem for estimable contrasts.

[F5]

Covariance is bilinear in finite linear combinations. Covariance is symmetric and bilinear in finite linear combinations.

[F6]

Expectation is linear on finite sums of integrable random variables. The Lebesgue integral is linear on $L^{1} (μ)$ .

[F7]

Finite-dimensional linear maps are continuous and preserve Borel measurability of random vectors. Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ , A continuous map has Borel preimages of Borel sets.

[A1]

$X$ has full column rank, and $V$ is the same known symmetric positive-definite covariance under each $P_{β}$ .

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F5F6F7algebra

Choose $L$ from [F3] and set $\tilde{Y} = L^{- 1} Y$ and $\tilde{X} = L^{- 1} X$ . The transformed response is Borel by [F7]. Linearity [F6] and [F1] give $E_{β} \tilde{Y} = \tilde{X} β$ , and covariance bilinearity [F5] with [F2] gives ${Cov}_{β} (\tilde{Y}) = L^{- 1} V L^{- T} = I_{n}$ . Since $L$ is invertible, $\tilde{X}$ has full column rank.

2.1A1F3F4step 1.1algebra

OLS on the transformed model is $({\tilde{X}}^{T} \tilde{X})^{- 1} {\tilde{X}}^{T} \tilde{Y} = (X^{T} V^{- 1} X)^{- 1} X^{T} V^{- 1} Y = {\hat{β}}_{G L S},$ because $L^{- T} L^{- 1} = V^{- 1}$ . The transformed model meets every hypothesis of [F4], so this estimator is unbiased and each of its linear contrasts has minimum variance among linear unbiased contrasts.

2.2F1F2F5F6step 1.1algebra

Put $C = (X^{T} V^{- 1} X)^{- 1}$ and $A = C X^{T} V^{- 1}$ . Then $A X = I_{p}$ , so linearity [F6] and [F1] give $E_{β} [A Y] = β$ . By [F5] and [F2], ${Cov}_{β} (A Y) = A V A^{T} = C X^{T} V^{- 1} V V^{- 1} X C = C .$ Here $C$ is symmetric because $X^{T} V^{- 1} X$ is symmetric positive definite.

3.1F4step 1.1step 2.1step 2.2∎

Let $\tilde{β}$ be any linear unbiased estimator. For each $c$ , $c^{T} \tilde{β}$ is a linear unbiased estimator of $c^{T} β$ in the transformed model of step 1.1. By [F4] and step 2.1 its variance is at least that of $c^{T} {\hat{β}}_{G L S}$ . This holds for every $c \in R^{p}$ , so the covariance difference is positive semidefinite and GLS is BLUE.

Depends on

Used by

Known-covariance BLUP and its prediction-error covariance Theorem

Dependency tree · two levels

50 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Fan Li, STA610 Lecture 2: Two Solutions—GLS and Cluster-Robust Standard Errors, PDF pp. 1–2 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.5.1 (standard reference, not scraped)