Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.smc

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

AHoF V30 Sequential Monte Carlo: propagate and resample a weighted particle set over time; the filtered estimate is the normalized weighted mean of the particles, estimate w0 x0 w1 x1 = w0*x0 + w1*x1. Balanced weights on particles 1/2 and 3/4 give 5/8; weight on the first particle only gives 1/2. Proved native and axiom-free (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.smc` prints this classification.

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

smc/balanced :
  → ℚ≥0

smc/single :
  → ℚ≥0

smc/estimate-unfold :
  (w0 x0 w1 x1 : ℚ≥0)
  → qmdp/value w0 x0 w1 x1 = w0 · x0 + w1 · x1

smc/balanced-is-five-eighths :
  → smc/balanced = 5/8

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

smc/combined :
  → proposition/conjunction (smc/balanced = 5/8) (smc/single = 1/2)