Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayesian-param

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

AHoF V2 Bayesian Parameter Learning: infer model parameters by their posterior, which is proportional to the data likelihood under the parameter times the parameter prior: posterior-score likelihood prior = likelihood * prior. A parameter with likelihood 1/2 and prior 1/4 scores 1/8; a worse-fitting parameter (likelihood 1/4, prior 1/4) scores 1/16, concentrating posterior mass on better-fitting parameters. Scores 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.bayesian-param` prints this classification.

bayes-param/posterior-score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

bayes-param/good-param :
  → ℚ≥0

bayes-param/poor-param :
  → ℚ≥0

bayes-param/posterior-score-unfold :
  (likelihood prior : ℚ≥0)
  → baseline/contribution likelihood prior = likelihood · prior

bayes-param/good-param-scores-one-eighth :
  → model-est/good-model = 1/8

bayes-param/poor-param-scores-one-sixteenth :
  → model-est/poor-model = 1/16

bayes-param/bayesian-param :
  → proposition/conjunction (model-est/good-model = 1/8) (model-est/poor-model = 1/16)