Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.simplex-interpolation

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

AHoF D28 Simplex Interpolation: interpolate a value function over a simplicial grid using barycentric coordinates. A query point inside a simplex is a convex combination of the simplex vertices with barycentric weights lambda_i summing to one; the interpolated value is the same convex combination of the vertex values: interpolate l1 v1 l2 v2 l3 v3 = l1*v1 + l2*v2 + l3*v3 over exact nonnegative rationals (a 2-simplex / triangle; a d-simplex folds over d+1 vertices). Proved native and axiom-free: the barycentric combination and worked instances that reduce by reflexivity. The simplex location (which simplex contains the query) and the barycentric-coordinate solve are executable concerns; the weights and vertex values are supplied rationals. What is proved here is the deterministic interpolation arithmetic. Requires nnrat/add and nnrat/multiply (in the D63 checkpoint). Scope (measured by the kernel): this module has 2 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.simplex-interpolation` prints this classification.

simplex-interpolation/interpolate :
  (x₁ x₂ x₃ x₄ x₅ x₆ : ℚ≥0)
  → ℚ≥0

simplex-interpolation/interpolate-unfold :
  (l1 v1 l2 v2 l3 v3 : ℚ≥0)
  → simplex-interpolation/interpolate l1 v1 l2 v2 l3 v3 = l1 · v1 + l2 · v2 + l3 · v3

simplex-interpolation/interpolate-example :
  → simplex-interpolation/interpolate 2 3 1 4 3 1 = 13

simplex-interpolation/interpolate-at-vertex :
  → simplex-interpolation/interpolate 1 3 0 4 0 1 = 3