Reference · Matrices

rainbow.math.linear.matrix.signed-scale-antitone

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

Nonpositive signed factors reverse scalar, vector, and matrix order. Negating a nonpositive factor makes it nonnegative. Monotonicity for that factor, followed by order-reversing negation and the checked multiplication negation law, yields scalar multiplication antitonicity on both sides. The scale-difference bridge and structural pointwise lifts extend the result to native vectors and matrices. Native and axiom-free on D63.

Depends onmath.linear.matrix.pointwise-order-laws

signed/multiply-left-antitone :
  (factor left right : ℚ)
  (factor-nonpositive : factor ≤ 0)
  (ordered : left ≤ right)
  → factor · right ≤ factor · left

signed/multiply-right-antitone :
  (factor left right : ℚ)
  (factor-nonpositive : factor ≤ 0)
  (ordered : left ≤ right)
  → right · factor ≤ left · factor

signed/scale-difference-antitone :
  (factor left right : ℚ)
  (factor-nonpositive : factor ≤ 0)
  (ordered : left ≤ right)
  → signed/scale (signed/positive factor) right - signed/scale (signed/negative factor) right ≤ signed/scale (signed/positive factor) left - signed/scale (signed/negative factor) left

vector/signed-scale-antitone :
  (factor : ℚ) (left right : List ℚ)
  (factor-nonpositive : factor ≤ 0)
  (ordered : vector/at-most left right)
  → vector/at-most (vector/signed-scale factor right) (vector/signed-scale factor left)

matrix/signed-scale-antitone :
  (factor : ℚ) (left right : List (List ℚ))
  (factor-nonpositive : factor ≤ 0)
  (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/signed-scale factor right) (matrix/signed-scale factor left)