Reference · Vectors

rainbow.math.linear.vector.dot-scale

Vectorssrc/rainbow/math/linear/vector/dot_scale.clj0 definitions, 5 theorems

Homogeneity of the native vector dot product in its first argument. signed/scale-zero signed/scale-multiply signed/scale-respects-equivalence vector/dot-scale-left vector/dot-scale-right The scalar laws are semiring identities checked through the verified nnrat ring normalizer. Dot homogeneity is then one List induction, combining the scalar product law, the tail hypothesis, and signed scale additivity.

Depends onmath.linear.vector.dot-bilinear

signed/scale-zero :
  (rate : ℚ≥0)
  → signed/scale rate 0 = 0

signed/scale-multiply :
  (rate : ℚ≥0) (value multiplier : ℚ)
  → signed/scale rate value · multiplier = signed/scale rate (value · multiplier)

signed/scale-respects-equivalence :
  (rate : ℚ≥0) (left right : ℚ)
  (same : left = right)
  → signed/scale rate left = signed/scale rate right

vector/dot-scale-left :
  (rate : ℚ≥0) (values weights : List ℚ)
  → vector/dot (vector/scale rate values) weights = signed/scale rate (vector/dot values weights)

vector/dot-scale-right :
  (rate : ℚ≥0) (values weights : List ℚ)
  → vector/dot values (vector/scale rate weights) = signed/scale rate (vector/dot values weights)