Reference · Vectors

rainbow.math.linear.vector.norm-laws

Vectorssrc/rainbow/math/linear/vector/norm_laws.clj0 definitions, 2 theorems

Algebraic laws for the exact signed squared norm. norm/norm-squared-negate norm/norm-squared-scale Negating every component leaves the squared norm equivalent. Scaling every component by a nonnegative rational rate scales the squared norm by rate*rate. Both are theorem-only consequences of native dot bilinearity; they add no numerical square-root assumption.

Depends onmath.linear.vector.dot-negate

norm/norm-squared-negate :
  (values : List ℚ)
  → norm/norm-squared (vector/negate values) = norm/norm-squared values

norm/norm-squared-scale :
  (rate : ℚ≥0) (values : List ℚ)
  → norm/norm-squared (vector/scale rate values) = signed/scale (rate · rate) (norm/norm-squared values)