Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.kalman

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/kalman.clj2 definitions, 3 theorems

AHoF D-family Kalman Filter: the optimal linear estimator for a Gaussian-linear system, alternating a predict step (propagate mean and variance) and an update step that fuses a noisy measurement. With prior variance P and measurement-noise variance R, the scalar update is governed by the Kalman gain and the posterior variance: kalman-gain P R = P / (P + R) kalman-posterior P R = P * R / (P + R) ( = (1 - gain) * P ) over exact rationals (both defined here). Proved native and axiom-free, as worked instances reducing by reflexivity via exact rational division: a balanced fusion (P = R = 1 gives gain 1/2 and posterior 1/2) and a confident-measurement case (P = 3, R = 1 gives gain 3/4). The filter's optimality, and that the gain grows as R shrinks for all inputs, are classical properties not proved here. The measurement, the process model, and the mean update (which needs signed innovation) are executable. Requires nnrat/divide, nnrat/add, nnrat/multiply (division is the rational-division capability, composed here; the rest are in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.kalman` prints this classification.

Depends onmath.rational.division

kalman/gain :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

kalman/posterior :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

kalman/balanced-gain :
  → kalman/gain 1 1 = 1/2

kalman/balanced-posterior :
  → kalman/posterior 1 1 = 1/2

kalman/confident-measurement-gain :
  → kalman/gain 3 1 = 3/4