Reference · Algorithm guarantees

rainbow.algorithms.proofs.bayesian-learning

Algorithm guaranteessrc/rainbow/algorithms/proofs/bayesian_learning.clj2 definitions, 2 theorems

Bayesian parameter learning over exact rationals. The posterior mass of a parameter is its prior mass folded through the data: each datum multiplies the running mass by that datum's likelihood, so `posterior = prior * L1 * L2 * ...` (up to normalization). This is the sequential Bayesian update (AHoF D11) -- `(reduce bayesian-update prior data)` -- where a single update multiplies the current mass by a likelihood. Scope (measured by the kernel): this module has 2 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.bayesian-learning` prints this classification.

estimation/bayesian-update :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

estimation/bayesian-posterior :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

estimation/bayesian-update-unfold :
  (mass likelihood : ℚ≥0)
  → estimation/bayesian-update mass likelihood = mass · likelihood

estimation/bayesian-posterior-unfold :
  (prior likelihood-a likelihood-b : ℚ≥0)
  → estimation/bayesian-posterior prior likelihood-a likelihood-b = estimation/bayesian-update (update) likelihood-b
  where update := estimation/bayesian-update prior likelihood-a