Reference · Vectors

rainbow.math.linear.vector.norm-nonnegative

Vectorssrc/rainbow/math/linear/vector/norm_nonnegative.clj0 definitions, 3 theorems

Constructive nonnegativity of signed squares and native squared norms. signed/add-nonnegative signed/square-nonnegative norm/norm-squared-nonnegative A signed square is nonnegative by case-splitting the computable comparison with zero: either both factors are nonpositive or both are nonnegative. Signed addition preserves componentwise nonnegativity by nnrat add monotonicity. Squared-norm nonnegativity is then one List induction over the sum of component squares.

Depends onmath.rational.signed.multiply-order

signed/add-nonnegative :
  (left right : ℚ) (left-nonnegative : signed/nonnegative left)
  (right-nonnegative : signed/nonnegative right)
  → signed/nonnegative (left + right)

signed/square-nonnegative :
  (value : ℚ)
  → signed/nonnegative (value · value)

norm/norm-squared-nonnegative :
  (values : List ℚ)
  → signed/nonnegative (norm/norm-squared values)