Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.particle-filter-pf

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

AHoF D70 Particle Filter: approximate the posterior by a weighted particle set; the state estimate is the weighted mean estimate w0 x0 w1 x1 = w0*x0 + w1*x1. Proved native and axiom-free (worked values by cross-product equivalence). 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.particle-filter-pf` prints this classification.

pfilter/estimate :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

pfilter/balanced :
  → ℚ≥0

pfilter/single :
  → ℚ≥0

pfilter/estimate-unfold :
  (w0 x0 w1 x1 : ℚ≥0)
  → ekf/update w0 x0 w1 x1 = w0 · x0 + w1 · x1

pfilter/balanced-is-five-eighths :
  → gp/balanced-mean = 5/8

pfilter/single-is-first :
  → pfilter/single = 1/2

pfilter/combined :
  → proposition/conjunction (gp/balanced-mean = 5/8) (pfilter/single = 1/2)