Reference · Matrices

rainbow.math.linear.matrix.positive-multiply

Matricessrc/rainbow/math/linear/matrix/positive_multiply.clj0 definitions, 4 theorems

Nonnegativity and monotonicity of native finite matrix multiplication. Transpose turns a nonnegative right matrix into nonnegative columns, so the positive matrix-action laws lift rowwise to products. Multiplication is monotone in its left factor when the fixed right factor is nonnegative, in its right factor when the fixed left factor is nonnegative, and jointly monotone under the exact source/destination positivity premises needed by the two-step order path. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-order

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

matrix/multiply-monotone-left :
  (left right factor : List (List ℚ))
  (factor-positive : matrix/at-most (matrix/zero-like factor) factor)
  (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/multiply left factor) (matrix/multiply right factor)

matrix/multiply-monotone-right :
  (factor left right : List (List ℚ))
  (factor-positive : matrix/at-most (matrix/zero-like factor) factor)
  (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/multiply factor left) (matrix/multiply factor right)

matrix/multiply-monotone :
  (source-left destination-left source-right destination-right : List (List ℚ))
  (destination-left-positive : matrix/at-most (matrix/zero-like destination-left) destination-left)
  (source-right-positive : matrix/at-most (matrix/zero-like source-right) source-right)
  (left-ordered : matrix/at-most source-left destination-left)
  (right-ordered : matrix/at-most source-right destination-right)
  → matrix/at-most (multiply₁) (multiply)
  where multiply := matrix/multiply destination-left destination-right
  where multiply₁ := matrix/multiply source-left source-right