Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayesian-model-estimation

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

AHoF D59 Bayesian Model Estimation: score candidate models by their posterior probability, which is proportional to the data likelihood under the model times the model prior: posterior-score likelihood prior = likelihood * prior. A model with likelihood 1/2 and prior 1/4 scores 1/8; a worse-fitting model (likelihood 1/4, prior 1/4) scores 1/16, so posterior mass concentrates on better-fitting models. 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-model-estimation` prints this classification.

model-est/posterior-score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

model-est/good-model :
  → ℚ≥0

model-est/poor-model :
  → ℚ≥0

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

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

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

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