Kernel ridge regression and GBLUP

TheoremPositive definiteness of the GBLUP matrix#✓fully proved

For λ > 0 the GBLUP matrix ZZᵀ + λI is positive definite.

theorem posDef_mul_transpose_add (Z : Matrix (Fin m) ι ℝ) {lam : ℝ} (hlam : 0 < lam) :
    (Z * Zᵀ + lam • (1 : Matrix (Fin m) (Fin m) ℝ)).PosDef

Used by 2

Used byGP posterior mean = GBLUP · Push-through identity for ridge regression

TheoremPush-through identity for ridge regression#✓fully proved

The push-through identity (ZᵀZ + λI)⁻¹ Zᵀ = Zᵀ (ZZᵀ + λI)⁻¹ for λ > 0.

theorem transpose_mul_add_inv_mul_transpose (Z : Matrix (Fin m) ι ℝ) {lam : ℝ} (hlam : 0 < lam) :
    (Zᵀ * Z + lam • (1 : Matrix ι ι ℝ))⁻¹ * Zᵀ =
      Zᵀ * (Z * Zᵀ + lam • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹

Uses 2 · Used by 2

Proof usesPositive definiteness of the GBLUP matrix · The ridge matrix is positive definite

Used byRR-BLUP = GBLUP · Ridge marker effects are back-solved from GBLUP

TheoremRR-BLUP = GBLUP#✓fully proved

RR-BLUP = GBLUP (fitted values): Z (ZᵀZ + λI)⁻¹ Zᵀ = ZZᵀ (ZZᵀ + λI)⁻¹ for λ > 0.

theorem mul_ridgeHat_eq_gblupHat (Z : Matrix (Fin m) ι ℝ) {lam : ℝ} (hlam : 0 < lam) :
    Z * (Zᵀ * Z + lam • (1 : Matrix ι ι ℝ))⁻¹ * Zᵀ =
      Z * Zᵀ * (Z * Zᵀ + lam • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹

Uses 1

Proof usesPush-through identity for ridge regression

TheoremRidge marker effects are back-solved from GBLUP#✓fully proved

The ridge marker effects are back-solved from GBLUP: (ZᵀZ + λI)⁻¹ Zᵀ y = Zᵀ (ZZᵀ + λI)⁻¹ y.

theorem ridgeEstimate_eq (Z : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) {lam : ℝ} (hlam : 0 < lam) :
    ridgeEstimate Z y lam =
      Zᵀ *ᵥ ((Z * Zᵀ + lam • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹ *ᵥ y)

Uses 2 · Used by 1

Statement usesRidge estimate

Proof usesPush-through identity for ridge regression

Used byRR-BLUP = GBLUP

TheoremRR-BLUP = GBLUP#✓fully proved

RR-BLUP = GBLUP (predictions): for any genotypes Z' (training or new individuals), Z' β̂ = Z' Zᵀ (ZZᵀ + λI)⁻¹ y.

theorem mulVec_ridgeEstimate {τ : Type*} (Z' : Matrix τ ι ℝ)
    (Z : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) {lam : ℝ} (hlam : 0 < lam) :
    Z' *ᵥ ridgeEstimate Z y lam =
      (Z' * Zᵀ * (Z * Zᵀ + lam • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹) *ᵥ y

Uses 2 · Used by 2

Statement usesRidge estimate

Proof usesRidge marker effects are back-solved from GBLUP

Used byGP posterior mean = RR-BLUP · Kernel ridge regression = GBLUP = RR-BLUP

13 fully proved

The Gaussian-process view

DefinitionLinear marker kernel on genotype vectors#✓fully proved

The linear marker kernel k(a, b) = s ⟪a, b⟫ = s ∑ⱼ aⱼ bⱼ on genotype vectors: the covariance of genetic values aᵀβ and bᵀβ when the marker effects β are independent with variance s.

noncomputable def markerKernel (s : ℝ) (a b : ι → ℝ) : ℝ :=
  s * (a ⬝ᵥ b)

Used by 6

Used byThe GBLUP posterior · GP posterior mean = GBLUP · GP posterior mean = RR-BLUP · Kernel matrix of the marker kernel · Positive semidefiniteness of the marker kernel matrix · Formula for the linear marker kernel

TheoremFormula for the linear marker kernel#✓fully proved

Unfolding markerKernel.

theorem markerKernel_apply (s : ℝ) (a b : ι → ℝ) : markerKernel s a b = s * (a ⬝ᵥ b)

Uses 1

Statement usesLinear marker kernel on genotype vectors

TheoremKernel matrix of the marker kernel#✓fully proved

The kernel matrix of the marker kernel between genotypes Z' and Z is s Z' Zᵀ.

theorem kernelMatrix_markerKernel {τ ν : Type*} (s : ℝ) (Z' : Matrix τ ι ℝ) (Z : Matrix ν ι ℝ) :
    kernelMatrix (markerKernel s) Z' Z = s • (Z' * Zᵀ)

Uses 2 · Used by 3

Statement usesLinear marker kernel on genotype vectors · Kernel matrix

Used byThe GBLUP posterior · GP posterior mean = GBLUP · Positive semidefiniteness of the marker kernel matrix

TheoremPositive semidefiniteness of the marker kernel matrix#✓fully proved

For s ≥ 0 the marker kernel is a covariance kernel: its kernel matrix on any inputs is positive semidefinite.

theorem kernelMatrix_markerKernel_posSemidef {ν : Type*} [Finite ν] {s : ℝ} (hs : 0 ≤ s)
    (Z : Matrix ν ι ℝ) : (kernelMatrix (markerKernel s) Z Z).PosSemidef

Uses 3 · Used by 1

Statement usesLinear marker kernel on genotype vectors · Kernel matrix

Proof usesKernel matrix of the marker kernel

Used byThe GBLUP posterior

TheoremGP posterior mean = GBLUP#✓fully proved

For the marker kernel with variance s > 0 and noise variance σ² > 0, the predictive-mean matrix K(Z', Z) (K(Z, Z) + σ² I)⁻¹ of Gaussian-process regression is Z' Zᵀ (ZZᵀ + (σ²/s) I)⁻¹.

theorem gpMean_markerKernel {τ : Type*} {s σ2 : ℝ} (hs : 0 < s) (hσ : 0 < σ2)
    (Z' : Matrix τ ι ℝ) (Z : Matrix (Fin m) ι ℝ) :
    kernelMatrix (markerKernel s) Z' Z *
        (kernelMatrix (markerKernel s) Z Z + σ2 • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹ =
      Z' * Zᵀ * (Z * Zᵀ + (σ2 / s) • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹

Uses 4 · Used by 2

Statement usesLinear marker kernel on genotype vectors · Kernel matrix

Proof usesKernel matrix of the marker kernel · Positive definiteness of the GBLUP matrix

Used byThe GBLUP posterior · GP posterior mean = RR-BLUP

TheoremGP posterior mean = RR-BLUP#✓fully proved

With the marker kernel, the GP predictive mean at genotypes Z' is Z' β̂ for the ridge marker effects β̂ with λ = σ²/s.

theorem gpMean_markerKernel_mulVec {τ : Type*} {s σ2 : ℝ} (hs : 0 < s)
    (hσ : 0 < σ2) (Z' : Matrix τ ι ℝ) (Z : Matrix (Fin m) ι ℝ) (y : Fin m → ℝ) :
    (kernelMatrix (markerKernel s) Z' Z *
        (kernelMatrix (markerKernel s) Z Z + σ2 • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹) *ᵥ y =
      Z' *ᵥ ridgeEstimate Z y (σ2 / s)

Uses 5

Statement usesLinear marker kernel on genotype vectors · Kernel matrix · Ridge estimate

Proof usesGP posterior mean = GBLUP · RR-BLUP = GBLUP

TheoremThe GBLUP posterior#✓fully proved

If the genetic values Z' β of individuals with genotypes Z' and the phenotypes y = Z β + ε of the training individuals are jointly Gaussian with the covariance of the marker kernel (marker-effect variance s > 0, residual variance σ² > 0), then given y the genetic values are Gaussian with mean Z' Zᵀ (ZZᵀ + (σ²/s) I)⁻¹ y, which is the RR-BLUP prediction Z' β̂ (gpMean_markerKernel_mulVec), and covariance s (Z' Z'ᵀ - Z' Zᵀ (ZZᵀ + (σ²/s) I)⁻¹ Z Z'ᵀ).

theorem condDistrib_markerKernel {s σ2 : ℝ} (hs : 0 < s) (hσ : 0 < σ2) (Z' : Matrix τ ι ℝ)
    (Z : Matrix (Fin m) ι ℝ) {V : Ω → EuclideanSpace ℝ (τ ⊕ Fin m)} (hV : Measurable V)
    (hlaw : P.map V = multivariateGaussian 0 (jointCov (markerKernel s) σ2 Z' Z)) :
    ∀ᵐ y ∂P.map (fun ω => toEuclideanLin (targetPart (τ := τ)) (V ω)),
      condDistrib (fun ω => toEuclideanLin (testPart (ν := Fin m)) (V ω))
          (fun ω => toEuclideanLin (targetPart (τ := τ)) (V ω)) P y =
        multivariateGaussian
          (toEuclideanLin (Z' * Zᵀ * (Z * Zᵀ + (σ2 / s) • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹) y)
          (s • (Z' * Z'ᵀ - Z' * Zᵀ * (Z * Zᵀ + (σ2 / s) • (1 : Matrix (Fin m) (Fin m) ℝ))⁻¹ *
            (Z * Z'ᵀ)))

Uses 9

Statement usesLinear marker kernel on genotype vectors · Joint prior covariance in Gaussian-process regression · Training-target projection · Test-value projection

Proof usesGP posterior mean = GBLUP · Kernel matrix of the marker kernel · Positive semidefiniteness of the marker kernel matrix · The Gaussian-process posterior · Kernel matrix

The RKHS view

TheoremKernel ridge regression = GBLUP = RR-BLUP#✓fully proved

In a real RKHS whose kernel has Gram matrix ZZᵀ at the training inputs, the kernel ridge fit (the minimizer of ∑ᵢ (yᵢ - f xᵢ)² + λ ‖f‖², kernelRidgeRisk_kernelRidgeFit_le) has fitted values Z β̂.

theorem kernelRidgeFit_eq_mulVec_ridgeEstimate {X H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] (x : Fin m → X)
    (Z : Matrix (Fin m) ι ℝ) (hK : kernelGram H x = Z * Zᵀ) (y : Fin m → ℝ) {lam : ℝ}
    (hlam : 0 < lam) (j : Fin m) :
    kernelRidgeFit H x y lam (x j) = (Z *ᵥ ridgeEstimate Z y lam) j

Uses 5

Statement usesRidge estimate · Kernel Gram matrix · Kernel ridge regression fit

Proof usesRR-BLUP = GBLUP · Fitted values of kernel ridge regression

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.