Reference · Matrices

rainbow.math.linear.matrix.affine-sign

Matricessrc/rainbow/math/linear/matrix/affine_sign.clj0 definitions, 6 theorems

Cone preservation for vector addition and signed affine matrix action. Truncated pointwise vector addition preserves both the nonnegative and nonpositive cones. Combining those generic lemmas with the four matrix action sign cases proves every affine sign combination in which the offset and linear image share a sign. In particular, nonnegative Bellman data map nonnegative values back into the nonnegative cone. Theorem-only and axiom-free on D63.

Depends onmath.linear.matrix.affine-order

vector/add-nonnegative :
  (left right : List ℚ) (left-sign : vector/at-most (vector/zero-like left) left)
  (right-sign : vector/at-most (vector/zero-like right) right)
  → vector/at-most (vector/zero-like (vector/add left right)) (vector/add left right)

vector/add-nonpositive :
  (left right : List ℚ) (left-sign : vector/at-most left (vector/zero-like left))
  (right-sign : vector/at-most right (vector/zero-like right))
  → vector/at-most (vector/add left right) (vector/zero-like (vector/add left right))

matrix/affine-action-nonnegative :
  (rows : List (List ℚ)) (offset values : List ℚ)
  (offset-sign : vector/at-most (vector/zero-like offset) offset)
  (rows-sign : matrix/at-most (matrix/zero-like rows) rows)
  (values-sign : vector/at-most (vector/zero-like values) values)
  → vector/at-most (vector/zero-like (matrix/affine-action rows offset values)) (matrix/affine-action rows offset values)

matrix/affine-action-nonpositive-rows :
  (rows : List (List ℚ)) (offset values : List ℚ)
  (offset-sign : vector/at-most offset (vector/zero-like offset))
  (rows-sign : matrix/at-most rows (matrix/zero-like rows))
  (values-sign : vector/at-most (vector/zero-like values) values)
  → vector/at-most (matrix/affine-action rows offset values) (vector/zero-like (matrix/affine-action rows offset values))

matrix/affine-action-nonpositive-values :
  (rows : List (List ℚ)) (offset values : List ℚ)
  (offset-sign : vector/at-most offset (vector/zero-like offset))
  (rows-sign : matrix/at-most (matrix/zero-like rows) rows)
  (values-sign : vector/at-most values (vector/zero-like values))
  → vector/at-most (matrix/affine-action rows offset values) (vector/zero-like (matrix/affine-action rows offset values))

matrix/affine-action-nonnegative-both-nonpositive :
  (rows : List (List ℚ)) (offset values : List ℚ)
  (offset-sign : vector/at-most (vector/zero-like offset) offset)
  (rows-sign : matrix/at-most rows (matrix/zero-like rows))
  (values-sign : vector/at-most values (vector/zero-like values))
  → vector/at-most (vector/zero-like (matrix/affine-action rows offset values)) (matrix/affine-action rows offset values)