Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.discrete-filter

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

AHoF D66 Discrete State Filter (recursive Bayesian filtering over a finite state space): each step multiplies the prior belief in a state by the measurement likelihood to get the unnormalized posterior weight, then renormalizes: posterior-weight likelihood prior = likelihood * prior. A state with likelihood 1/2 and prior 1/4 gets weight 1/8; a less-likely state (likelihood 1/4, prior 1/4) gets the smaller weight 1/16, so the update concentrates belief on better-explained states. Weights 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.discrete-filter` prints this classification.

discrete-filter/posterior-weight :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

discrete-filter/high-state :
  → ℚ≥0

discrete-filter/low-state :
  → ℚ≥0

discrete-filter/posterior-weight-unfold :
  (likelihood prior : ℚ≥0)
  → baseline/contribution likelihood prior = likelihood · prior

discrete-filter/high-weight-is-one-eighth :
  → model-est/good-model = 1/8

discrete-filter/low-weight-is-one-sixteenth :
  → model-est/poor-model = 1/16

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