Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayes-theorem

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

AHoF Bayes' Theorem: invert a conditional probability to obtain the posterior belief in a hypothesis H after observing evidence E, posterior likelihood prior evidence = (likelihood * prior) / evidence i.e. P(H|E) = P(E|H) P(H) / P(E), the foundation of Bayesian inference, diagnosis, and spam filtering. Proved native and axiom-free: the posterior as the normalized product of likelihood and prior (composing nnrat/multiply and exact rational division); a worked posterior (stated as rational equivalence via the cross-product certificate, since the quotient is not in lowest terms); and that when likelihood equals evidence the posterior equals the prior (the evidence is uninformative). The likelihood, prior, and marginal-evidence estimates are executable; what is proved is the posterior combination. Requires nnrat/multiply, nnrat/divide (rational-division capability, composed here), nnrat/equivalent, and the D63 checkpoint. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.bayes-theorem` prints this classification.

Depends onmath.rational.division

bayes/posterior :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

bayes/posterior-example :
  → bayes/posterior 3/4 1/2 3/8 = 1

bayes/uninformative-evidence :
  → bayes/posterior 1/2 3/4 1/2 = 3/4