Reference · Vectors

rainbow.math.linear.vector.dot-distance-bound

Vectorssrc/rainbow/math/linear/vector/dot_distance_bound.clj1 definitions, 2 theorems

Componentwise distance accounting for signed dot products. `vector/dot-distance-sum weights left right` sums the distances between corresponding weighted components. When `left` and `right` have the same shape, paired-addition Lipschitzness proves that the distance between their dot products is below this explicit sum. A second theorem transfers any upper bound on the sum to the dot distance. The shape premise is essential: truncating dot products can otherwise consume different weight prefixes. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.multiply-ringalgorithms.proofs.inner-productmath.rational.signed.distance-additivemath.linear.vector.shape-cancellation

vector/dot-distance-sum :
  (x₁ x₂ x₃ : List ℚ)
  → ℚ

vector/dot-distance-below-sum :
  (weights left right : List ℚ) (shape : vector/same-shape left right)
  → signed/distance (vector/dot weights left) (vector/dot weights right) ≤ vector/dot-distance-sum weights left right

vector/dot-distance-bounded :
  (weights left right : List ℚ) (upper : ℚ) (shape : vector/same-shape left right)
  (sum-bound : vector/dot-distance-sum weights left right ≤ upper)
  → signed/distance (vector/dot weights left) (vector/dot weights right) ≤ upper