Reference · Vectors

rainbow.math.linear.vector.row-sum-lipschitz

Vectorssrc/rainbow/math/linear/vector/row_sum_lipschitz.clj1 definitions, 3 theorems

Nonnegative row-sum Lipschitz bounds for signed dot products. `vector/sum` specializes the existing polymorphic signed map-sum to a signed vector. Componentwise nonnegativity makes that mass nonnegative. Combining the component multiplication-distance bound with the maximum component distance and distributivity proves dot-distance-sum(row,x,y) <= sum(row) * sup-distance(x,y). The previously established dot-distance theorem then yields the same bound for the actual dot products. Equal input shape is explicit because dot and sup distance both truncate lists. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.signed.list-summath.linear.vector.pointwise-ordermath.rational.signed.distance-multiply-nonnegativemath.rational.signed.multiply-monotonemath.rational.signed.multiply-ordermath.rational.signed.distributivemath.rational.signed.vector-sup-distancemath.linear.vector.dot-distance-bound

vector/sum :
  (x₁ : List ℚ)
  → ℚ

vector/sum-nonnegative :
  (values : List ℚ) (positive : vector/at-most (vector/zero-like values) values)
  → 0 ≤ vector/sum values

vector/dot-distance-sum-bounded-by-row-sum :
  (weights left right : List ℚ)
  (weights-positive : vector/at-most (vector/zero-like weights) weights)
  (shape : vector/same-shape left right)
  → vector/dot-distance-sum weights left right ≤ vector/sum weights · vector/sup-distance left right

vector/dot-distance-bounded-by-row-sum :
  (weights left right : List ℚ)
  (weights-positive : vector/at-most (vector/zero-like weights) weights)
  (shape : vector/same-shape left right)
  → signed/distance (vector/dot weights left) (vector/dot weights right) ≤ vector/sum weights · vector/sup-distance left right