Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.linear-interpolation

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/linear_interpolation.clj4 definitions, 5 theorems

AHoF D27 Linear Interpolation over exact rationals: interpolate between two values a and b with convex weights w0, w1 (summing to one), lerp a b w0 w1 = w0 * a + w1 * b. Interpolating between 1/2 and 3/4: the midpoint (weights 1/2, 1/2) is 5/8; the left endpoint (weights 1, 0) is 1/2; the right endpoint (weights 0, 1) is 3/4. Values are proved by cross-product equivalence. Proved native and axiom-free. Scope (measured by the kernel): this module has 4 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.linear-interpolation` prints this classification.

interp/lerp :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

interp/midpoint :
  → ℚ≥0

interp/left-endpoint :
  → ℚ≥0

interp/right-endpoint :
  → ℚ≥0

interp/lerp-unfold :
  (a b w0 w1 : ℚ≥0)
  → interp/lerp a b w0 w1 = w0 · a + w1 · b

interp/midpoint-is-five-eighths :
  → interp/midpoint = 5/8

interp/left-endpoint-is-a :
  → interp/left-endpoint = 1/2

interp/right-endpoint-is-b :
  → interp/right-endpoint = 3/4

interp/linear-interpolation :
  → proposition/conjunction (interp/midpoint = 5/8) (interp/left-endpoint = 1/2)