LemmaStatement: 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.

Marginal covariance of the linear mixed model

Statement

For the moment model $Y = X β + Z b + ε$ of Finite-dimensional linear mixed model with explicit longitudinal roles, the marginal covariance is $Cov (Y) = V : = Z G Z^{T} + R .$ This identity uses only the stated means, covariances, and independence; it does not require Gaussianity.

Facts & Assumptions

Given: The finite-dimensional linear mixed model and its finite second moments.

[F1]

$Y = X β + Z b + ε$ , $E b = E ε = 0$ , $Cov (b) = G$ , $Cov (ε) = R$ , and $b$ and $ε$ are independent. Finite-dimensional linear mixed model with explicit longitudinal roles.

[F2]

Covariance is bilinear in finite linear combinations of square-integrable real random variables. Covariance is symmetric and bilinear in finite linear combinations.

[F3]

Measurable coordinate functions of independent random elements remain independent. Measurable coordinatewise functions preserve independence.

[F4]

Expectations of products of independent integrable real random variables factor. Expectations factor over finite products of independent random variables.

[F5]

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

Proof

Given: A fixed $β$ , finite matrices $X, Z$ , and random vectors $b, ε$ satisfying [F1].

1.1F1F5algebra

Since $E b = E ε = 0$ , linearity [F5] gives $E Y = X β$ and $Y - E Y = Z b + ε$ .

2.1F1F2step 1.1algebra

By [F2], each covariance entry of $Z b + ε$ is the sum of the entries from $Z b$ and $ε$ and the two cross-covariance entries. The first two matrices are $Z G Z^{T}$ and $R$ by [F1] and finite matrix multiplication.

3.1F1F2F3F4step 2.1algebra∎

For each coordinate pair $b_{k}, ε_{ℓ}$ , [F3] gives independence and [F4] gives $E [b_{k} ε_{ℓ}] = E [b_{k}] E [ε_{ℓ}] = 0$ . Both means vanish by [F1], so every cross-covariance entry is zero. The remaining covariance matrix is therefore $Z G Z^{T} + R$ .

Depends on

Used by

A mixed-model covariance does not imply MAR dropout Counterexample
Two visits can alias random-slope and residual variance components Counterexample
Random-intercept covariance and intraclass correlation Example
A Gaussian error contrast has the induced multivariate-normal law Lemma
Conditional Gaussian law of random effects Theorem
Known-covariance BLUP and its prediction-error covariance Theorem
Known-covariance GLS is BLUE Theorem

Dependency tree · two levels

27 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 6: Linear Mixed-Effects Models, PDF pp. 8–9 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.4.1 (standard reference, not scraped)