LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

The GLS information matrix is positive definite

Statement

If $X \in R^{n \times p}$ has full column rank and $V \in R^{n \times n}$ is symmetric positive definite, then $X^{T} V^{- 1} X$ is symmetric positive definite. In particular it is invertible.

Facts & Assumptions

Given: The full-column-rank design $X$ and known positive-definite covariance $V$ in Generalized least-squares estimator for known covariance.

[F1]

Every real symmetric positive-definite matrix 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.

[A1]

$X$ has full column rank, and $V$ is symmetric positive definite.

Proof

Given: $X \in R^{n \times p}$ has full column rank and $V$ is positive definite.

1.1A1F1algebra

By [A1] and [F1], write $V = L L^{T}$ with $L$ invertible. Hence $V^{- 1} = L^{- T} L^{- 1}$ and $V^{- 1}$ is symmetric.

2.1A1step 1.1algebra∎

For any nonzero $c \in R^{p}$ , full column rank gives $X c \neq 0$ , so $L^{- 1} X c \neq 0$ . Therefore $c^{T} X^{T} V^{- 1} X c = (L^{- 1} X c)^{T} (L^{- 1} X c) > 0$ . The matrix is symmetric by step 1.1, proving positive definiteness and invertibility.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Generalized least-squares estimator for known covariance.

Dependency tree · two levels

13 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 p. 2 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.5.1 (standard reference, not scraped)