Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.ukf

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

AHoF D69 Unscented Kalman Filter: propagate a small set of deterministically chosen sigma points through the nonlinear model and recover the posterior mean as their weighted average. With two sigma points the recovered mean is the weighted sum: sigma-mean w0 s0 w1 s1 = w0 * s0 + w1 * s1. Equal weights on sigma points 1/2 and 3/4 give the mean 5/8; weighting only the first sigma point (weights 1, 0) returns it, 1/2. Values 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.ukf` prints this classification.

ukf/sigma-mean :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

ukf/balanced-mean :
  → ℚ≥0

ukf/first-point-only :
  → ℚ≥0

ukf/sigma-mean-unfold :
  (w0 s0 w1 s1 : ℚ≥0)
  → qmdp/value w0 s0 w1 s1 = w0 · s0 + w1 · s1

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

ukf/first-point-is-half :
  → smc/single = 1/2

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