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.

Conditional Gaussian law of random effects

Statement

Assume AC and the Gaussian branch of the finite-dimensional mixed model. Let $V = Z G Z^{T} + R$ be positive definite. With conditional expectation taken componentwise given $σ (Y)$ , and conditional covariance defined entrywise by conditional expectations of centered products, one has $E [b ∣ Y] = G Z^{T} V^{- 1} (Y - X β), Cov (b ∣ Y) = G - G Z^{T} V^{- 1} Z G .$ The latent covariance $G$ may be singular.

Facts & Assumptions

Given: The Gaussian mixed model, AC, and $V ≻ 0$ .

[F1]

$Y = X β + Z b + ε$ , with centered independent $b, ε$ and covariance matrices $G, R$ ; these are finite-second-moment covariances. Finite-dimensional linear mixed model with explicit longitudinal roles, Moments, variance, and covariance on a probability space.

[F2]

The marginal covariance is $V = Z G Z^{T} + R$ . Marginal covariance of the linear mixed model.

[F3]

Under AC, $(b, ε)$ is jointly multivariate normal with covariance $diag (G, R)$ . Gaussian branch of the linear mixed model, Multivariate normal law, including singular covariance.

[F4]

Jointly Gaussian coordinate blocks with zero cross-covariance are independent, including when either covariance is singular. Jointly Gaussian blocks with zero cross-covariance are independent, including singular blocks.

[F5]

Independence of random elements means independence of their generated sigma-algebras. Independent random elements.

[F6]

A conditional-expectation version is characterized by its integrals on every event in the conditioning sigma-algebra. Conditional expectation given a sigma algebra.

[F7]

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

[F8]

Products of square-integrable variables are integrable by Cauchy–Schwarz. Cauchy-Schwarz inequality for $L^{2}$ .

[F9]

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

[F10]

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

[F11]

Finite-dimensional linear maps are continuous, and continuous maps between Euclidean spaces have Borel preimages of Borel sets. 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]

AC holds, $V$ is symmetric positive definite, and all variables have the finite second moments stated in [F1]. The Axiom of Choice.

Proof

Given: The Gaussian branch with $V ≻ 0$ and AC.

1.1A1F1F2F5F7F9F10algebra

Put $Y_{c} = Y - X β$ . Linearity [F10] and [F1] give $E Y = X β$ , so centering by this deterministic vector leaves covariance unchanged; [F2] gives $Cov (Y_{c}) = V$ . Coordinatewise independence of $b$ and $ε$ gives $Cov (b, ε) = 0$ by [F5] and [F7], so bilinearity [F9] gives $Cov (b, Y_{c}) = Cov (b, Z b) = G Z^{T}$ . Since $V$ is invertible by [A1], set $H = G Z^{T} V^{- 1}$ and $U = b - H Y_{c}$ . Bilinearity yields $Cov (U, Y_{c}) = G Z^{T} - H V = 0$ , and expectation linearity [F10] gives $E U = 0$ .

2.1A1F3F4F11step 1.1

The vectors $U$ and $Y_{c}$ are Borel random vectors by [F11]. For any coefficient vectors $s, t$ , the scalar $s^{T} U + t^{T} Y_{c}$ is a linear combination of the coordinates of $(b, ε)$ , so it is normal by the projection definition in [F3]. Thus $(U, Y_{c})$ is jointly multivariate normal. Its covariance is block diagonal by step 1.1, so [F4] implies that $U$ and $Y_{c}$ are independent.

3.1A1F5F6F7F10step 1.1step 2.1

By step 2.1 and [F5], $U$ and $Y_{c}$ generate independent sigma-algebras. For every event $E \in σ (Y_{c})$ , [F7] applied to $U_{k}$ and $1_{E}$ gives $E [U_{k} 1_{E}] = E [U_{k}] P (E) = 0$ . Since $H Y_{c}$ is square-integrable and $σ (Y_{c})$ -measurable, [F10] gives $E [b_{k} 1_{E}] = E [(H Y_{c})_{k} 1_{E}]$ for every such event; [F6] identifies $H Y_{c}$ as a version of $E [b ∣ Y_{c}]$ . Finally, $σ (Y_{c}) = σ (Y)$ , so the stated conditional-mean formula follows.

4.1F6F7F8step 1.1step 2.1step 3.1algebra

For each coordinate pair $k, ℓ$ , $U_{k} U_{ℓ}$ is integrable by [F8]. As a measurable function of $U$ , it is independent of $Y_{c}$ by [F7] and step 2.1. For every $E \in σ (Y_{c})$ , factorization gives $E [U_{k} U_{ℓ} 1_{E}] = E [U_{k} U_{ℓ}] P (E)$ , so [F6] yields $E [U_{k} U_{ℓ} ∣ Y_{c}] = E [U_{k} U_{ℓ}]$ . Together with the conditional mean from step 3.1, step 1.1, and $σ (Y_{c}) = σ (Y)$ , the defined entrywise conditional covariance of $b = H Y_{c} + U$ is $Cov (U)$ .

5.1F1F2F9step 1.1step 3.1step 4.1algebra∎

Expanding $Cov (U) = Cov (b - H Y_{c})$ by [F9] and [F1]–[F2] yields $Cov (U) = G - G Z^{T} V^{- 1} Z G - G Z^{T} V^{- 1} Z G + G Z^{T} V^{- 1} V V^{- 1} Z G = G - G Z^{T} V^{- 1} Z G .$ Together with steps 3.1–4.1 this proves both formulas. No inverse of $G$ is used, so singular $G$ is allowed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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. 11–12 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.4.3 and Appendix D (standard reference, not scraped)