Gaussian process regression

DefinitionKernel matrix#✓fully proved

For a kernel \(k : X \times X \to \mathbb{R}\) and two families of inputs \(a = (a_i)_{i \in \alpha}\) and \(b = (b_j)_{j \in \beta}\) in \(X\), the kernel (Gram) matrix \(K(a, b)\) is the \(\alpha \times \beta\) real matrix with entries \(K(a, b)_{ij} = k(a_i, b_j)\).

def kernelMatrix (k : X → X → ℝ) {α β : Type*} (a : α → X) (b : β → X) : Matrix α β ℝ :=
  Matrix.of fun i j => k (a i) (b j)

Used by 11

Used byThe Gaussian-process posterior · Regularized kernel matrices are invertible · Joint prior covariance in Gaussian-process regression · The joint covariance as a kernel matrix plus noise · The joint covariance is positive semidefinite · Training blocks of positive semidefinite kernel matrices · The GBLUP posterior · GP posterior mean = GBLUP · GP posterior mean = RR-BLUP · Kernel matrix of the marker kernel · Positive semidefiniteness of the marker kernel matrix

DefinitionJoint prior covariance in Gaussian-process regression#✓fully proved

The joint prior covariance of the test values f(x*) and the noisy training targets y = f(x) + ε, ε ~ N(0, σ² I): [[K(x*, x*), K(x*, x)], [K(x, x*), K(x, x) + σ² I]].

def jointCov (k : X → X → ℝ) (σ2 : ℝ) (xt : τ → X) (xs : ν → X) :
    Matrix (τ ⊕ ν) (τ ⊕ ν) ℝ :=
  fromBlocks (kernelMatrix k xt xt) (kernelMatrix k xt xs) (kernelMatrix k xs xt)
    (kernelMatrix k xs xs + σ2 • 1)

Uses 1 · Used by 4

Statement usesKernel matrix

Used byThe Gaussian-process posterior · The joint covariance as a kernel matrix plus noise · The joint covariance is positive semidefinite · The GBLUP posterior

DefinitionTest-value projection#✓fully proved

For finite index sets \(\tau\) (test inputs) and \(\nu\) (training inputs), the test-value projection is the \(\tau \times (\tau \sqcup \nu)\) real matrix with the identity matrix on the columns indexed by \(\tau\) and a zero block on the columns indexed by \(\nu\). It sends a joint vector \((u, y)\) with \(u \in \mathbb{R}^{\tau}\) and \(y \in \mathbb{R}^{\nu}\) to its block of test values \(u\).

noncomputable def testPart : Matrix τ (τ ⊕ ν) ℝ := blockRow 1 0

Uses 1 · Used by 2

Statement usesHorizontal block matrix

Used byThe Gaussian-process posterior · The GBLUP posterior

DefinitionTraining-target projection#✓fully proved

For finite index sets \(\tau\) (test inputs) and \(\nu\) (training inputs), the training-target projection is the \(\nu \times (\tau \sqcup \nu)\) real matrix with a zero block on the columns indexed by \(\tau\) and the identity matrix on the columns indexed by \(\nu\). It sends a joint vector \((u, y)\) with \(u \in \mathbb{R}^{\tau}\) and \(y \in \mathbb{R}^{\nu}\) to its block of training targets \(y\).

noncomputable def targetPart : Matrix ν (τ ⊕ ν) ℝ := blockRow 0 1

Uses 1 · Used by 2

Statement usesHorizontal block matrix

Used byThe Gaussian-process posterior · The GBLUP posterior

TheoremRegularized kernel matrices are invertible#✓fully proved

Let \(k : X \times X \to \mathbb{R}\) be a kernel and \(x = (x_j)_{j \in \nu}\) a finite family of inputs whose kernel matrix \(K = (k(x_i, x_j))_{i, j \in \nu}\) is positive semidefinite. Then for every \(\sigma^2 > 0\) the matrix \(K + \sigma^2 I\) has nonzero determinant, so it is invertible.

theorem isUnit_det_kernelMatrix_add (k : X → X → ℝ) (xs : ν → X)
    (hK : (kernelMatrix k xs xs).PosSemidef)
    {σ2 : ℝ} (hσ : 0 < σ2) : IsUnit (kernelMatrix k xs xs + σ2 • 1).det

Uses 1 · Used by 1

Statement usesKernel matrix

Used byThe Gaussian-process posterior

TheoremThe joint covariance as a kernel matrix plus noise#✓fully proved

For a kernel \(k : X \times X \to \mathbb{R}\), a real number \(\sigma^2\), test inputs \(x^* = (x^*_i)_{i \in \tau}\) and training inputs \(x = (x_j)_{j \in \nu}\), the joint covariance of \(k\), \(\sigma^2\), \(x^*\) and \(x\) equals \(K + D\), where \(K\) is the kernel matrix of the combined family \((x^*, x)\) indexed by \(\tau \sqcup \nu\) and \(D\) is the diagonal matrix with entry \(0\) at each test index and \(\sigma^2\) at each training index.

theorem jointCov_eq_add (k : X → X → ℝ) (σ2 : ℝ) (xt : τ → X) (xs : ν → X) :
    jointCov k σ2 xt xs = kernelMatrix k (Sum.elim xt xs) (Sum.elim xt xs) +
      diagonal (Sum.elim 0 fun _ => σ2)

Uses 2 · Used by 1

Statement usesJoint prior covariance in Gaussian-process regression · Kernel matrix

Used byThe joint covariance is positive semidefinite

TheoremThe joint covariance is positive semidefinite#✓fully proved

Let \(k : X \times X \to \mathbb{R}\) be a kernel, let \(x^* = (x^*_i)_{i \in \tau}\) and \(x = (x_j)_{j \in \nu}\) be families of test and training inputs, and let \(\sigma^2 \ge 0\). If the kernel matrix of the combined family \((x^*, x)\), indexed by \(\tau \sqcup \nu\), is positive semidefinite, then the joint covariance of \(k\), \(\sigma^2\), \(x^*\) and \(x\) is positive semidefinite.

theorem jointCov_posSemidef (k : X → X → ℝ) {σ2 : ℝ} (hσ : 0 ≤ σ2) (xt : τ → X) (xs : ν → X)
    (hk : (kernelMatrix k (Sum.elim xt xs) (Sum.elim xt xs)).PosSemidef) :
    (jointCov k σ2 xt xs).PosSemidef

Uses 3 · Used by 1

Statement usesJoint prior covariance in Gaussian-process regression · Kernel matrix

Proof usesThe joint covariance as a kernel matrix plus noise

Used byThe Gaussian-process posterior

TheoremTraining blocks of positive semidefinite kernel matrices#✓fully proved

Let \(k : X \times X \to \mathbb{R}\) be a kernel and let \(x^* = (x^*_i)_{i \in \tau}\) and \(x = (x_j)_{j \in \nu}\) be families of inputs. If the kernel matrix of the combined family \((x^*, x)\), indexed by \(\tau \sqcup \nu\), is positive semidefinite, then so is the kernel matrix \((k(x_i, x_j))_{i, j \in \nu}\) of \(x\).

theorem kernelMatrix_posSemidef_train (k : X → X → ℝ) (xt : τ → X) (xs : ν → X)
    (hk : (kernelMatrix k (Sum.elim xt xs) (Sum.elim xt xs)).PosSemidef) :
    (kernelMatrix k xs xs).PosSemidef

Uses 1 · Used by 1

Statement usesKernel matrix

Used byThe Gaussian-process posterior

TheoremThe Gaussian-process posterior#✓fully proved

Let \(k : X \times X \to \mathbb{R}\) be a kernel, let \(x^* = (x^*_i)_{i \in \tau}\) (test inputs) and \(x = (x_j)_{j \in \nu}\) (training inputs) be finite families in \(X\), and write \(K(a, b)\) for the kernel matrix \((k(a_i, b_j))_{i, j}\). Assume that the kernel matrix of the combined family \((x^*, x)\), indexed by \(\tau \sqcup \nu\), is positive semidefinite, and let \(\sigma^2 > 0\). Let \(V\) be a measurable random vector in \(\mathbb{R}^{\tau \sqcup \nu}\) on a probability space whose law is the Gaussian \(N(0, \Sigma)\), where \(\Sigma\) is the joint covariance of \(k\), \(\sigma^2\), \(x^*\) and \(x\), and let \(F\) (the test values) and \(Y\) (the training targets), random vectors in \(\mathbb{R}^{\tau}\) and \(\mathbb{R}^{\nu}\), be the test and training blocks of \(V\). Then for almost every \(y\) with respect to the law of \(Y\), the conditional distribution of \(F\) given \(Y = y\) is the Gaussian with mean \(K(x^*, x) (K(x, x) + \sigma^2 I)^{-1} y\) and covariance \(K(x^*, x^*) - K(x^*, x) (K(x, x) + \sigma^2 I)^{-1} K(x, x^*)\).

theorem condDistrib_test_given_targets (k : X → X → ℝ) {σ2 : ℝ} (hσ : 0 < σ2) (xt : τ → X)
    (xs : ν → X) (hk : (kernelMatrix k (Sum.elim xt xs) (Sum.elim xt xs)).PosSemidef)
    {V : Ω → EuclideanSpace ℝ (τ ⊕ ν)} (hV : Measurable V)
    (hlaw : P.map V = multivariateGaussian 0 (jointCov k σ2 xt xs)) :
    ∀ᵐ y ∂P.map (fun ω => toEuclideanLin (targetPart (τ := τ)) (V ω)),
      condDistrib (fun ω => toEuclideanLin (testPart (ν := ν)) (V ω))
          (fun ω => toEuclideanLin (targetPart (τ := τ)) (V ω)) P y =
        multivariateGaussian
          (toEuclideanLin (kernelMatrix k xt xs * (kernelMatrix k xs xs + σ2 • 1)⁻¹) y)
          (kernelMatrix k xt xt -
            kernelMatrix k xt xs * (kernelMatrix k xs xs + σ2 • 1)⁻¹ * kernelMatrix k xs xt)

Uses 9 · Used by 1

Statement usesJoint prior covariance in Gaussian-process regression · Kernel matrix · Training-target projection · Test-value projection

Proof usesRegularized kernel matrices are invertible · The joint covariance is positive semidefinite · Training blocks of positive semidefinite kernel matrices · Horizontal block matrix · Gaussian conditioning (Schur complement)

Used byThe GBLUP posterior

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.