Reference · Matrices

rainbow.math.linear.matrix.antitone

Matricessrc/rainbow/math/linear/matrix/antitone.clj0 definitions, 8 theorems

Antitonicity of native dot products, matrix action, and multiplication. A fixed entrywise nonpositive vector reverses pointwise order through dot. Rowwise lifting gives antitonicity of matrix-vector action in either input when the other input is nonpositive. Transpose then lifts those laws to multiplication in either factor. Theorem-only, kernel-checked, and axiom-free on D63.

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

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

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

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

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

matrix/vector-multiply-antitone :
  (source-rows destination-rows : List (List ℚ))
  (source-values destination-values : List ℚ)
  (destination-rows-negative : matrix/at-most destination-rows (matrix/zero-like destination-rows))
  (source-values-negative : vector/at-most source-values (vector/zero-like source-values))
  (rows-ordered : matrix/at-most source-rows destination-rows)
  (values-ordered : vector/at-most source-values destination-values)
  → vector/at-most (multiply) (multiply₁)
  where multiply := matrix/vector-multiply destination-rows destination-values
  where multiply₁ := matrix/vector-multiply source-rows source-values

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

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

matrix/multiply-antitone :
  (source-left destination-left source-right destination-right : List (List ℚ))
  (destination-left-negative : matrix/at-most destination-left (matrix/zero-like destination-left))
  (source-right-negative : matrix/at-most source-right (matrix/zero-like 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