Linear mixed models and BLUP

11 fully proved

Mixed-model equations

DefinitionPhenotypic covariance of a linear mixed model#✓fully proved

The phenotypic covariance V = Z G Zᵀ + R of the linear mixed model y = X b + Z u + e with Cov u = G, Cov e = R.

def phenCov (Z : Matrix n q ℝ) (G : Matrix q q ℝ) (R : Matrix n n ℝ) : Matrix n n ℝ :=
  Z * G * Zᵀ + R

Used by 6

Used byBLUP as a conditional law · BLUP is the conditional expectation · Henderson's mixed-model equations · The MME solution is the GLS estimate and the BLUP · Positive definiteness of the phenotypic covariance · Henderson's mixed-model equations give the GLS estimator and the BLUP

DefinitionSolution of Henderson's mixed-model equations#✓fully proved

Henderson's mixed-model equations for y = X b + Z u + e, Cov u = G, Cov e = R: [Xᵀ R⁻¹ X, Xᵀ R⁻¹ Z; Zᵀ R⁻¹ X, Zᵀ R⁻¹ Z + G⁻¹] [b; u] = [Xᵀ R⁻¹ y; Zᵀ R⁻¹ y].

def IsMMESolution (X : Matrix n p ℝ) (Z : Matrix n q ℝ) (G : Matrix q q ℝ) (R : Matrix n n ℝ)
    (y : n → ℝ) (b : p → ℝ) (u : q → ℝ) : Prop :=
  (Xᵀ * R⁻¹ * X) *ᵥ b + (Xᵀ * R⁻¹ * Z) *ᵥ u = (Xᵀ * R⁻¹) *ᵥ y ∧
    (Zᵀ * R⁻¹ * X) *ᵥ b + (Zᵀ * R⁻¹ * Z + G⁻¹) *ᵥ u = (Zᵀ * R⁻¹) *ᵥ y

Used by 4

Used byHenderson's mixed-model equations · The MME solution is the GLS estimate and the BLUP · Solution of Henderson's mixed-model equations · Henderson's mixed-model equations give the GLS estimator and the BLUP

TheoremPositive definiteness of the phenotypic covariance#✓fully proved

V = Z G Zᵀ + R is positive definite.

theorem posDef_phenCov [Finite n] (hG : G.PosDef) (hR : R.PosDef) : (phenCov Z G R).PosDef

Uses 1 · Used by 2

Statement usesPhenotypic covariance of a linear mixed model

Used byBLUP as a conditional law · Henderson's mixed-model equations

TheoremHenderson's mixed-model equations#✓fully proved

Henderson's mixed-model equations (Henderson 1975; Robinson 1991): for positive definite G and R and V = Z G Zᵀ + R, (b, u) solves the mixed-model equations if and only if b solves the generalized least-squares normal equations Xᵀ V⁻¹ X b = Xᵀ V⁻¹ y and u = G Zᵀ V⁻¹ (y - X b).

theorem isMMESolution_iff (hG : G.PosDef) (hR : R.PosDef) (y : n → ℝ) (b : p → ℝ)
    (u : q → ℝ) :
    IsMMESolution X Z G R y b u ↔
      (Xᵀ * (phenCov Z G R)⁻¹ * X) *ᵥ b = (Xᵀ * (phenCov Z G R)⁻¹) *ᵥ y ∧
        u = (G * Zᵀ * (phenCov Z G R)⁻¹) *ᵥ (y - X *ᵥ b)

Uses 3 · Used by 1

Statement usesSolution of Henderson's mixed-model equations · Phenotypic covariance of a linear mixed model

Proof usesPositive definiteness of the phenotypic covariance

Used byThe MME solution is the GLS estimate and the BLUP

TheoremThe MME solution is the GLS estimate and the BLUP#✓fully proved

The MME solution is the GLS estimate and the BLUP (Henderson 1975): if moreover Xᵀ V⁻¹ X is invertible, the mixed-model equations have the unique solution b̂ = (Xᵀ V⁻¹ X)⁻¹ Xᵀ V⁻¹ y (the GLS estimate) and û = G Zᵀ V⁻¹ (y - X b̂).

theorem isMMESolution_iff_gls (hG : G.PosDef) (hR : R.PosDef)
    (hX : IsUnit (Xᵀ * (phenCov Z G R)⁻¹ * X)) (y : n → ℝ) (b : p → ℝ) (u : q → ℝ) :
    IsMMESolution X Z G R y b u ↔
      b = glsMatrix X (phenCov Z G R) *ᵥ y ∧
        u = (G * Zᵀ * (phenCov Z G R)⁻¹) *ᵥ (y - X *ᵥ b)

Uses 4 · Used by 1

Statement usesSolution of Henderson's mixed-model equations · Phenotypic covariance of a linear mixed model · Generalized least-squares matrix

Proof usesHenderson's mixed-model equations

Used byHenderson's mixed-model equations give the GLS estimator and the BLUP

Gaussian

TheoremBLUP as a conditional law#✓fully proved

BLUP as a conditional law (Henderson 1975; Robinson 1991): in the Gaussian mixed model y = X b + Z u + e with fixed effects b, random effects u ~ N(0, G) and residuals e ~ N(0, R) independent, G and R positive definite, the conditional law of u given y is N(G Zᵀ V⁻¹ (y - X b), G - G Zᵀ V⁻¹ Z G) with V = Z G Zᵀ + R (for almost every y).

theorem condDistrib_mixedModel {u : Ω → EuclideanSpace ℝ q} {e : Ω → EuclideanSpace ℝ n}
    (hu : Measurable u) (he : Measurable e) (hind : IndepFun u e P) {G : Matrix q q ℝ}
    {R : Matrix n n ℝ} (hG : G.PosDef) (hR : R.PosDef)
    (hul : P.map u = multivariateGaussian 0 G) (hel : P.map e = multivariateGaussian 0 R)
    (X : Matrix n p ℝ) (Z : Matrix n q ℝ) (b : EuclideanSpace ℝ p) :
    ∀ᵐ y ∂P.map (fun ω => toEuclideanLin X b + toEuclideanLin Z (u ω) + e ω),
      condDistrib u (fun ω => toEuclideanLin X b + toEuclideanLin Z (u ω) + e ω) P y =
        multivariateGaussian
          (toEuclideanLin (G * Zᵀ * (phenCov Z G R)⁻¹) (y - toEuclideanLin X b))
          (G - G * Zᵀ * (phenCov Z G R)⁻¹ * (Z * G))

Uses 10 · Used by 1

Statement usesPhenotypic covariance of a linear mixed model

Proof usesPositive definiteness of the phenotypic covariance · Horizontal block matrix · Gaussian conditioning (Schur complement) · Block-triangular congruence of a block-diagonal matrix · Translating a multivariate Gaussian · Concatenation of independent Gaussian random vectors · Linear images of multivariate Gaussians · The joint covariance of a linear-Gaussian model is positive semidefinite · Block-diagonal matrices with positive semidefinite blocks

Used byBLUP is the conditional expectation

TheoremBLUP is the conditional expectation#✓fully proved

BLUP is the conditional expectation in the Gaussian mixed model: 𝔼[u | y] = G Zᵀ V⁻¹ (y - X b) almost surely.

theorem condExp_mixedModel {u : Ω → EuclideanSpace ℝ q} {e : Ω → EuclideanSpace ℝ n}
    (hu : Measurable u) (he : Measurable e) (hind : IndepFun u e P) {G : Matrix q q ℝ}
    {R : Matrix n n ℝ} (hG : G.PosDef) (hR : R.PosDef)
    (hul : P.map u = multivariateGaussian 0 G) (hel : P.map e = multivariateGaussian 0 R)
    (X : Matrix n p ℝ) (Z : Matrix n q ℝ) (b : EuclideanSpace ℝ p) :
    P[u | MeasurableSpace.comap (fun ω => toEuclideanLin X b + toEuclideanLin Z (u ω) + e ω)
        inferInstance] =ᵐ[P]
      fun ω => toEuclideanLin (G * Zᵀ * (phenCov Z G R)⁻¹)
        (toEuclideanLin Z (u ω) + e ω)

Uses 2

Statement usesPhenotypic covariance of a linear mixed model

Proof usesBLUP as a conditional law

LDpred

TheoremThe LDpred-inf posterior#✓fully proved

The LDpred-inf posterior (Vilhjálmsson et al. 2015; the likelihood β̂ | β ~ N(R β, R / N) of Zhu and Stephens 2017): with M markers, N individuals, heritability h² > 0, effects β ~ N(0, h² / M · I), an LD matrix R that is positive definite, and marginal estimates β̂ = R β + ε with ε ~ N(0, R / N) independent of β, the posterior law of β given β̂ is N((R + M / (N h²) · I)⁻¹ β̂, (1 / N) (R + M / (N h²) · I)⁻¹). In particular 𝔼[β | β̂] = (R + M / (N h²) · I)⁻¹ β̂.

theorem condDistrib_ldpredInf {M N : ℕ} (hM : 0 < M) (hN : 0 < N) {h2 : ℝ} (hh2 : 0 < h2)
    {R : Matrix (Fin M) (Fin M) ℝ} (hR : R.PosDef) {β ε : Ω → EuclideanSpace ℝ (Fin M)}
    (hβ : Measurable β) (hε : Measurable ε) (hind : IndepFun β ε P)
    (hβl : P.map β = multivariateGaussian 0 ((h2 / M) • (1 : Matrix (Fin M) (Fin M) ℝ)))
    (hεl : P.map ε = multivariateGaussian 0 ((1 / N : ℝ) • R)) :
    ∀ᵐ b ∂P.map (fun ω => toEuclideanLin R (β ω) + ε ω),
      condDistrib β (fun ω => toEuclideanLin R (β ω) + ε ω) P b =
        multivariateGaussian (toEuclideanLin (R + (M / (N * h2) : ℝ) • 1)⁻¹ b)
          ((1 / N : ℝ) • (R + (M / (N * h2) : ℝ) • 1)⁻¹)

Uses 1

Proof usesBayes' theorem for a linear-Gaussian observation

Marginal Effects

DefinitionMarginal association estimate of a marker#✓fully proved

The N-normalized marginal association estimate β̂_j = X_jᵀ y / N of marker j for the phenotype y = X β + ε (fixed effects β, noise ε).

noncomputable def marginalEffect (X : Matrix (Fin N) (Fin M) ℝ) (β : Fin M → ℝ)
    (ε : Fin N → Ω → ℝ) (j : Fin M) (ω : Ω) : ℝ :=
  (∑ i, X i j * (∑ k, X i k * β k + ε i ω)) / N

Used by 2

Used byThe mean of the marginal estimates · The raw residual-product second moment of the marginal estimates

TheoremThe mean of the marginal estimates#✓fully proved

The mean of the marginal estimates (Zhu and Stephens 2017): for fixed effects β and noise with mean zero, 𝔼[X_jᵀ y / N] = (R β)_j with R = Xᵀ X / N (ldCorr).

theorem integral_marginalEffect (X : Matrix (Fin N) (Fin M) ℝ) (β : Fin M → ℝ)
    {ε : Fin N → Ω → ℝ} (hε : ∀ i, Integrable (ε i) P) (hmean : ∀ i, ∫ ω, ε i ω ∂P = 0)
    (j : Fin M) :
    ∫ ω, marginalEffect X β ε j ω ∂P = ∑ k, ldCorr X j k * β k

Uses 2

Statement usesNormalized cross product of genotype markers · Marginal association estimate of a marker

TheoremThe raw residual-product second moment of the marginal estimates#✓fully proved

The raw residual-product second moment of the marginal estimates (Zhu and Stephens 2017): if 𝔼[ε_i ε_i'] = σ² [i = i'], then 𝔼[(β̂_j - (R β)_j)(β̂_k - (R β)_k)] = σ² / N · R_jk.

This theorem deliberately assumes neither that P is a probability measure nor that the noise has mean zero, so its conclusion is not by itself a covariance or a Gaussian likelihood. With a probability measure and mean-zero noise, integral_marginalEffect identifies R β as the mean, and this raw second moment is the corresponding covariance.

theorem integral_marginalEffect_sub_mul (X : Matrix (Fin N) (Fin M) ℝ) (β : Fin M → ℝ)
    {ε : Fin N → Ω → ℝ} {σ2 : ℝ} (hε : ∀ i i', Integrable (fun ω => ε i ω * ε i' ω) P)
    (hsecondMoment : ∀ i i', ∫ ω, ε i ω * ε i' ω ∂P = if i = i' then σ2 else 0)
    (j k : Fin M) :
    ∫ ω, (marginalEffect X β ε j ω - ∑ l, ldCorr X j l * β l) *
        (marginalEffect X β ε k ω - ∑ l, ldCorr X k l * β l) ∂P = σ2 / N * ldCorr X j k

Uses 2

Statement usesNormalized cross product of genotype markers · Marginal association estimate of a marker

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.