Reference · Vectors

rainbow.math.linear.vector.norm-zero-reflection

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

Zero squared norm reflects componentwise zero for finite signed vectors. norm/equivalent-zero-like-of-norm-squared-zero norm/equivalent-zero-like-of-is-norm-zero The conclusion uses vector/zero-like, not the empty vector: it preserves the input dimension and vector/equivalent proves every component equivalent to signed zero. List induction splits each zero sum into the nonnegative head square and tail squared norm, reflects the head square, and recurses. Native and axiom-free.

Depends onmath.linear.vector.norm-nonnegative

norm/equivalent-zero-like-of-norm-squared-zero :
  (values : List ℚ)
  (norm-zero : norm/norm-squared values = 0)
  → vector/equivalent values (vector/zero-like values)

norm/equivalent-zero-like-of-is-norm-zero :
  (values : List ℚ) (zero-is-norm : norm/is-norm values 0)
  → vector/equivalent values (vector/zero-like values)