Reference · Matrices

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

Matricessrc/rainbow/math/linear/matrix/mixed_sign_action.clj0 definitions, 10 theorems

Mixed-sign laws for signed dot products and native matrix action. Addition preserves upper and lower zero bounds. A nonpositive factor times a nonnegative factor is nonpositive, while two nonpositive factors have a nonnegative product. Structural dot lifts cover the three remaining sign combinations, and rowwise lifting gives the corresponding matrix-vector action laws. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.least-squares-equality

signed/add-preserves-nonnegative-order :
  (left right : ℚ)
  (left-positive : 0 ≤ left)
  (right-positive : 0 ≤ right)
  → 0 ≤ left + right

signed/add-preserves-nonpositive-order :
  (left right : ℚ)
  (left-negative : left ≤ 0)
  (right-negative : right ≤ 0)
  → left + right ≤ 0

signed/multiply-nonpositive-nonnegative-order :
  (left right : ℚ)
  (left-negative : left ≤ 0)
  (right-positive : 0 ≤ right)
  → left · right ≤ 0

signed/multiply-nonpositive-nonpositive-order :
  (left right : ℚ)
  (left-negative : left ≤ 0)
  (right-negative : right ≤ 0)
  → 0 ≤ left · right

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

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

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

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

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

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