Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.ekf

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

AHoF D68 Extended Kalman Filter: the EKF linearizes the nonlinear process and measurement models about the current estimate and applies the standard Kalman measurement update, blending the prediction with the observation by the Kalman gain: update wp prior wm measurement = wp * prior + wm * measurement (with wp + wm = 1 the complementary predict/measurement weights). Blending a prediction 1/2 and a measurement 3/4 with equal weights gives 5/8; trusting the measurement fully (weights 0, 1) gives 3/4. 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.ekf` prints this classification.

ekf/update :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

ekf/balanced-update :
  → ℚ≥0

ekf/measurement-trusting-update :
  → ℚ≥0

ekf/update-unfold :
  (wp prior wm measurement : ℚ≥0)
  → ekf/update wp prior wm measurement = wp · prior + wm · measurement

ekf/balanced-is-five-eighths :
  → ekf/balanced-update = 5/8

ekf/trusting-is-measurement :
  → ekf/measurement-trusting-update = 3/4

ekf/ekf :
  → proposition/conjunction (ekf/balanced-update = 5/8) (ekf/measurement-trusting-update = 3/4)