Alphabeta Math
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 BLUP and its prediction-error covariance

Statement

In the moment-only linear mixed model, suppose X has full column rank and the known marginal covariance V=ZGZT+R is positive definite. Define b^=GZTV−1(Y−Xβ^GLS),β^GLS=(XTV−1X)−1XTV−1Y. Here best linear unbiased predictor (BLUP) means that b^ is unbiased for Eb=0 for every fixed β and its prediction-error covariance is minimal in positive-semidefinite order among all affine linear predictors a+BY with that same unbiasedness property. Then b^ is a BLUP and Cov⁡(b−b^)=G−GZTV−1ZG+GZTV−1X(XTV−1X)−1XTV−1ZG. No Gaussianity or Axiom of Choice is assumed. The covariance formula treats G and R as known; it does not cover the extra uncertainty from estimating variance components.

Facts & Assumptions

Given: The moment-only mixed model, full-column-rank X, known V≻0, and the GLS estimator.

[F1]

Y=Xβ+Zb+ε, with centered independent b,ε, covariance matrices G,R, and finite second moments. Finite-dimensional linear mixed model with explicit longitudinal roles.

[F2]

The marginal covariance is V=ZGZT+R. Marginal covariance of the linear mixed model.

[F3]

The best affine L2 predictor has an intercept fixed by means and coefficients satisfying covariance normal equations; singular predictor covariance is allowed. Normal equations for best affine L2 prediction.

[F4]

The GLS estimator is β^GLS=(XTV−1X)−1XTV−1Y, is unbiased, and has covariance C=(XTV−1X)−1. Generalized least-squares estimator for known covariance, Known-covariance GLS is BLUE.

[F5]

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

[F6]

Variance and covariance are defined by centered second moments. Moments, variance, and covariance on a probability space.

[F7]

Measurable coordinate functions preserve independence, and integrable products of independent coordinates factor. Measurable coordinatewise functions preserve independence, Expectations factor over finite products of independent random variables.

[F8]

Expectation is linear on finite sums of integrable random variables. The Lebesgue integral is linear on L1(μ).

[F9]

Finite-dimensional linear maps are continuous and preserve Borel measurability of random vectors. Every Euclidean linear map has a unique matrix and satisfies ∥Lh∥2≤K∥h∥2 for some K≥0, A continuous map has Borel preimages of Borel sets.

[A1]

X has full column rank, the random vectors are square-integrable, b is independent of ε, and the known covariance V is positive definite.

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F5F7F8F9algebra

Put Yc=Y−Xβ. By [F1], each pair of coordinates bk,εℓ is independent; since both are centered, factorization in [F7] gives Cov⁡(b,ε)=0. Bilinearity [F5] then gives Cov⁡(b,Yc)=GZT, while [F2] gives Cov⁡(Yc)=V. The affine predictor is a Borel random vector by [F9]. For fixed β, apply [F3] coordinatewise to predict b affinely from Y: the covariance normal equations have the unique solution H=GZTV−1 because V is invertible by [A1]. The intercept is Eb−HEY=−HXβ by [F8] and [F1]. Thus H(Y−Xβ) is the best affine L2 predictor when β is treated as known.

2.1A1F1F8F9step 1.1algebra

Write C=(XTV−1X)−1 and P=H(I−XCXTV−1). Then b^=PY and PX=0, because CXTV−1X=Ip. By [F9], b^ is Borel; by [F8] and [F1], Eβb^=PXβ=0=Eb for every β. Every affine linear predictor a+BY unbiased for b for every β must have a=0 and BX=0.

3.1F1F2F4F5F6step 1.1step 2.1algebra

Let Yc=Y−Xβ and u=b−HYc. By step 1.1, bilinearity gives Cov⁡(u,Yc)=GZT−HV=0 and Cov⁡(u)=G−GZTV−1ZG−GZTV−1ZG+GZTV−1VV−1ZG=G−GZTV−1ZG. Also β^GLS−β=CXTV−1Yc, so its covariance is C by [F4], and its covariance with u is zero because step 1.1 gives Cov⁡(u,Yc)=0. Since b−b^=u+HX(β^GLS−β), the error covariance is G−GZTV−1ZG+HXCXTHT, which is the displayed matrix after substituting H and C.

4.1A1F1F2F4F5step 1.1step 2.1step 3.1givenalgebra∎

Let BY be any other affine linear predictor unbiased for b for every β. By step 2.1 its intercept is zero and BX=0. Put D=B−P, so DX=0 and the competing prediction error is (b−PY)−DY. Since PV=GZT−HXCXT, one has Cov⁡(b−PY,Y)=GZT−PV=HXCXT. Therefore Cov⁡(b−PY,DY)=HXCXTDT=HXC(DX)T=0. Expanding the competing error covariance now gives Cov⁡(b−BY)=Cov⁡(b−PY)+DVDT⪰Cov⁡(b−PY). This is exactly the stated BLUP criterion.

Remarks

If variance components are estimated and substituted into this expression, the result is an empirical BLUP (eBLUP). This theorem supplies no exact prediction-error covariance for that plug-in estimator.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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