Reference · Vectors

rainbow.math.linear.vector.norm-witness-laws

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

Transformation laws for exact native norm witnesses. signed/scale-square norm/is-norm-negate-vector norm/is-norm-scale Scaling a signed value by a nonnegative rate scales its square by rate^2. Consequently, exact perfect-square norm witnesses transport through vector scaling. They also transport through vector negation because squared norm is invariant under componentwise negation.

Depends onmath.linear.vector.norm-laws

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

norm/is-norm-negate-vector :
  (values : List ℚ) (candidate : ℚ) (witness : norm/is-norm values candidate)
  → norm/is-norm (vector/negate values) candidate

norm/is-norm-scale :
  (rate : ℚ≥0) (values : List ℚ) (candidate : ℚ)
  (witness : norm/is-norm values candidate)
  → norm/is-norm (vector/scale rate values) (signed/scale rate candidate)