Reference · Vectors

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

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

The proved forward zero-characterization for native exact norms. norm/norm-squared-zero-of-equivalent-zero-like norm/is-norm-zero-of-equivalent-zero-like A vector componentwise equivalent to its shape-preserving zero vector has squared norm equivalent to signed zero, and signed zero is an exact norm witness. These are the forward directions; the converses are proved in rainbow.math.linear.vector.norm-zero-reflection.

Depends onmath.linear.vector.dot-zero-laws

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

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