Reference · Matrices

rainbow.math.linear.matrix.mixed-sign-multiply

Matricessrc/rainbow/math/linear/matrix/mixed_sign_multiply.clj0 definitions, 5 theorems

Mixed-sign laws for native finite matrix multiplication. Column insertion and total transpose preserve entrywise nonpositivity. The mixed-sign matrix-action laws then lift rowwise to products: a nonpositive factor times a nonnegative factor is entrywise nonpositive in either factor order, while two nonpositive factors yield an entrywise nonnegative product. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.mixed-sign-action

matrix/prepend-column-nonpositive :
  (values : List ℚ) (columns : List (List ℚ))
  (values-negative : vector/at-most values (vector/zero-like values))
  (columns-negative : matrix/at-most columns (matrix/zero-like columns))
  → matrix/at-most (matrix/prepend-column values columns) (matrix/zero-like (matrix/prepend-column values columns))

matrix/transpose-nonpositive :
  (rows : List (List ℚ)) (negative : matrix/at-most rows (matrix/zero-like rows))
  → matrix/at-most (matrix/transpose rows) (matrix/zero-like (matrix/transpose rows))

matrix/multiply-nonpositive-left :
  (left right : List (List ℚ))
  (left-negative : matrix/at-most left (matrix/zero-like left))
  (right-positive : matrix/at-most (matrix/zero-like right) right)
  → matrix/at-most (matrix/multiply left right) (matrix/zero-like (matrix/multiply left right))

matrix/multiply-nonpositive-right :
  (left right : List (List ℚ))
  (left-positive : matrix/at-most (matrix/zero-like left) left)
  (right-negative : matrix/at-most right (matrix/zero-like right))
  → matrix/at-most (matrix/multiply left right) (matrix/zero-like (matrix/multiply left right))

matrix/multiply-nonnegative-both-nonpositive :
  (left right : List (List ℚ))
  (left-negative : matrix/at-most left (matrix/zero-like left))
  (right-negative : matrix/at-most right (matrix/zero-like right))
  → matrix/at-most (matrix/zero-like (matrix/multiply left right)) (matrix/multiply left right)