Reference · Matrices

rainbow.math.linear.matrix.positive-action

Matricessrc/rainbow/math/linear/matrix/positive_action.clj0 definitions, 7 theorems

Positive dot products and monotone native matrix-vector action. A dot product is monotone in either argument when the fixed argument is entrywise nonnegative, hence two nonnegative vectors have a nonnegative dot. Rowwise lifting proves that matrix-vector action is nonnegative and monotone in its matrix, vector, or both inputs under the corresponding zero lower bounds. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-sign

vector/dot-left-monotone :
  (left right weights : List ℚ) (ordered : vector/at-most left right)
  (weights-positive : vector/at-most (vector/zero-like weights) weights)
  → vector/dot left weights ≤ vector/dot right weights

vector/dot-right-monotone :
  (weights left right : List ℚ)
  (weights-positive : vector/at-most (vector/zero-like weights) weights)
  (ordered : vector/at-most left right)
  → vector/dot weights left ≤ vector/dot weights right

vector/dot-nonnegative :
  (left right : List ℚ) (left-positive : vector/at-most (vector/zero-like left) left)
  (right-positive : vector/at-most (vector/zero-like right) right)
  → 0 ≤ vector/dot left right

matrix/vector-multiply-nonnegative :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (values-positive : vector/at-most (vector/zero-like values) values)
  → vector/at-most (vector/zero-like (matrix/vector-multiply rows values)) (matrix/vector-multiply rows values)

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

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

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