Reference · Matrices

rainbow.math.linear.matrix.signed-scale-positive

Matricessrc/rainbow/math/linear/matrix/signed_scale_positive.clj0 definitions, 6 theorems

Zero-value and nonnegativity laws for signed module scaling. Every signed factor sends scalar zero, vector zero-like, and matrix zero-like to zero up to the appropriate quotient equivalence. Combined with nonnegative-factor monotonicity, this proves that signed scaling preserves scalar and entrywise vector/matrix zero lower bounds. Native and axiom-free on D63.

Depends onmath.linear.matrix.add-order

signed/scale-difference-zero-value :
  (factor : ℚ)
  → signed/scale (signed/positive factor) 0 - signed/scale (signed/negative factor) 0 = 0

vector/signed-scale-zero-like :
  (factor : ℚ) (values : List ℚ)
  → vector/equivalent (scale) (vector/zero-like values)
  where scale := vector/signed-scale factor (vector/zero-like values)

matrix/signed-scale-zero-like :
  (factor : ℚ) (rows : List (List ℚ))
  → matrix/equivalent (scale) (matrix/zero-like rows)
  where scale := matrix/signed-scale factor (matrix/zero-like rows)

signed/scale-difference-nonnegative :
  (factor value : ℚ)
  (factor-nonnegative : 0 ≤ factor)
  (value-nonnegative : 0 ≤ value)
  → 0 ≤ signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value

vector/signed-scale-nonnegative :
  (factor : ℚ) (values : List ℚ)
  (factor-nonnegative : 0 ≤ factor)
  (values-nonnegative : vector/at-most (vector/zero-like values) values)
  → vector/at-most (vector/zero-like values) (vector/signed-scale factor values)

matrix/signed-scale-nonnegative :
  (factor : ℚ) (rows : List (List ℚ))
  (factor-nonnegative : 0 ≤ factor)
  (rows-nonnegative : matrix/at-most (matrix/zero-like rows) rows)
  → matrix/at-most (matrix/zero-like rows) (matrix/signed-scale factor rows)