Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.gaussian-inference

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/gaussian_inference.clj1 definitions, 3 theorems

AHoF D9 Inference in Gaussian Models: exact closed-form conjugate updates. In the natural (precision) parameterization, conditioning a Gaussian on a Gaussian likelihood ADDS precisions -- the posterior precision is the prior precision plus the likelihood precision: posterior-precision prior likelihood = prior + likelihood over exact nonnegative rationals (precision = 1/variance >= 0). Proved native and axiom-free: the precision update, and the guarantee that observing data never decreases precision (prior-precision <= posterior-precision), i.e. the posterior is at least as certain as the prior. The posterior mean is the precision-weighted average of prior and observation (a division, executable); the variances and their square roots are executable concerns. What is proved here is the additive precision update and its certainty-increase guarantee. Requires nnrat/add, nnrat/at-most, nat/le-add-right (d63 + nat-add-order). Scope (measured by the kernel): this module has 2 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-inference` prints this classification.

gaussian/posterior-precision :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

gaussian/posterior-precision-unfold :
  (prior likelihood : ℚ≥0)
  → astar/f-value prior likelihood = prior + likelihood

gaussian/posterior-precision-example :
  → astar/f-value 2 3 = 5

gaussian/precision-increases :
  → 2 ≤ astar/f-value 2 3