Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.gaussian-process

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/gaussian_process.clj3 definitions, 4 theorems

AHoF O62 Gaussian Process (surrogate model / regression): the GP posterior mean at a query point is a kernel-weighted combination of the observed targets, the weights coming from the covariance between the query and the training points: posterior-mean w0 y0 w1 y1 = w0 * y0 + w1 * y1. Kernel weights 1/2, 1/2 on observations 1/2, 3/4 give the posterior mean 5/8; a query co-located with the first observation (weights 1, 0) returns it, 1/2. Values are proved by cross-product equivalence. Proved native and axiom-free. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.gaussian-process` prints this classification.

gp/posterior-mean :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

gp/balanced-mean :
  → ℚ≥0

gp/colocated-mean :
  → ℚ≥0

gp/posterior-mean-unfold :
  (w0 y0 w1 y1 : ℚ≥0)
  → ekf/update w0 y0 w1 y1 = w0 · y0 + w1 · y1

gp/balanced-is-five-eighths :
  → gp/balanced-mean = 5/8

gp/colocated-is-observation :
  → gp/colocated-mean = 1/2

gp/gaussian-process :
  → proposition/conjunction (gp/balanced-mean = 5/8) (gp/colocated-mean = 1/2)