Reference · Matrices

rainbow.math.linear.matrix.affine-order

Matricessrc/rainbow/math/linear/matrix/affine_order.clj1 definitions, 16 theorems

Order and interval laws for signed affine finite-matrix action. `matrix/affine-action rows offset values` is the Bellman-shaped map `offset + rows·values`. Translation preserves pointwise order, so the matrix-action monotone, antitone, joint, and interval laws lift to this affine map without hidden shape assumptions. Native and axiom-free on D63.

Depends onmath.linear.matrix.interval-order

matrix/affine-action :
  (x₁ : List (List ℚ)) (x₂ x₃ : List ℚ)
  → List ℚ

matrix/affine-action-unfold :
  (rows : List (List ℚ)) (offset values : List ℚ)
  → vector/equivalent (matrix/affine-action rows offset values) (add)
  where add := vector/add offset (matrix/vector-multiply rows values)

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

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

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

matrix/affine-action-antitone-rows :
  (left right : List (List ℚ)) (offset values : List ℚ)
  (ordered : matrix/at-most left right)
  (values-negative : vector/at-most values (vector/zero-like values))
  → vector/at-most (action) (matrix/affine-action left offset values)
  where action := matrix/affine-action right offset values

matrix/affine-action-monotone-offset :
  (rows : List (List ℚ)) (left right values : List ℚ)
  (ordered : vector/at-most left right)
  → vector/at-most (matrix/affine-action rows left values) (matrix/affine-action rows right values)

matrix/affine-action-monotone-offset-values :
  (rows : List (List ℚ))
  (source-offset destination-offset source-values destination-values : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (offset-ordered : vector/at-most source-offset destination-offset)
  (values-ordered : vector/at-most source-values destination-values)
  → vector/at-most (action₁) (action)
  where action := matrix/affine-action rows destination-offset destination-values
  where action₁ := matrix/affine-action rows source-offset source-values

matrix/affine-action-monotone-offset-rows :
  (source-rows destination-rows : List (List ℚ))
  (source-offset destination-offset values : List ℚ)
  (values-positive : vector/at-most (vector/zero-like values) values)
  (rows-ordered : matrix/at-most source-rows destination-rows)
  (offset-ordered : vector/at-most source-offset destination-offset)
  → vector/at-most (action₁) (action)
  where action := matrix/affine-action destination-rows destination-offset values
  where action₁ := matrix/affine-action source-rows source-offset values

matrix/affine-action-monotone :
  (source-rows destination-rows : List (List ℚ))
  (offset source-values destination-values : List ℚ)
  (destination-rows-positive : matrix/at-most (matrix/zero-like destination-rows) destination-rows)
  (source-values-positive : vector/at-most (vector/zero-like source-values) source-values)
  (rows-ordered : matrix/at-most source-rows destination-rows)
  (values-ordered : vector/at-most source-values destination-values)
  → vector/at-most (action₁) (action)
  where action := matrix/affine-action destination-rows offset destination-values
  where action₁ := matrix/affine-action source-rows offset source-values

matrix/affine-action-antitone :
  (source-rows destination-rows : List (List ℚ))
  (offset 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 (action) (action₁)
  where action := matrix/affine-action destination-rows offset destination-values
  where action₁ := matrix/affine-action source-rows offset source-values

matrix/affine-action-monotone-all :
  (source-rows destination-rows : List (List ℚ))
  (source-offset destination-offset source-values destination-values : List ℚ)
  (destination-rows-positive : matrix/at-most (matrix/zero-like destination-rows) destination-rows)
  (source-values-positive : vector/at-most (vector/zero-like source-values) source-values)
  (rows-ordered : matrix/at-most source-rows destination-rows)
  (offset-ordered : vector/at-most source-offset destination-offset)
  (values-ordered : vector/at-most source-values destination-values)
  → vector/at-most (action₁) (action)
  where action := matrix/affine-action destination-rows destination-offset destination-values
  where action₁ := matrix/affine-action source-rows source-offset source-values

matrix/affine-action-bounds-offset :
  (rows : List (List ℚ)) (lower value upper values : List ℚ)
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most (matrix/affine-action rows lower values) (matrix/affine-action rows value values)
  where most₁ := vector/at-most (matrix/affine-action rows value values) (matrix/affine-action rows upper values)

matrix/affine-action-bounds-nonnegative-rows :
  (rows : List (List ℚ)) (offset lower value upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most (matrix/affine-action rows offset lower) (matrix/affine-action rows offset value)
  where most₁ := vector/at-most (matrix/affine-action rows offset value) (matrix/affine-action rows offset upper)

matrix/affine-action-bounds-nonpositive-rows :
  (rows : List (List ℚ)) (offset lower value upper : List ℚ)
  (rows-negative : matrix/at-most rows (matrix/zero-like rows))
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (most₁) (most)
  where most := vector/at-most (matrix/affine-action rows offset value) (matrix/affine-action rows offset lower)
  where most₁ := vector/at-most (matrix/affine-action rows offset upper) (matrix/affine-action rows offset value)

matrix/affine-action-bounds-nonnegative-values :
  (lower value upper : List (List ℚ)) (offset values : List ℚ)
  (values-positive : vector/at-most (vector/zero-like values) values)
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most (matrix/affine-action lower offset values) (matrix/affine-action value offset values)
  where most₁ := vector/at-most (matrix/affine-action value offset values) (matrix/affine-action upper offset values)

matrix/affine-action-bounds-nonpositive-values :
  (lower value upper : List (List ℚ)) (offset values : List ℚ)
  (values-negative : vector/at-most values (vector/zero-like values))
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most (matrix/affine-action upper offset values) (matrix/affine-action value offset values)
  where most₁ := vector/at-most (matrix/affine-action value offset values) (matrix/affine-action lower offset values)