Reference · Matrices

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

Matrices src/rainbow/math/linear/matrix/signed_scale_order.clj1 definitions, 6 theorems

Pointwise matrix order and monotonicity of signed module scaling. `matrix/at-most` is length-sensitive at both dimensions: corresponding rows must be pointwise ordered vectors and row counts must agree. A nonnegative signed factor preserves scalar scale-difference order, and structural lifts preserve vector and matrix pointwise order. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-subtract

matrix/at-most

DefinitionSource, line 89

matrix/at-most :
  (x₁ x₂ : List (List ℚ))
  → Prop

List = data/Listℚ = signed/SignedRational

signed/scale-difference-monotone

TheoremFor all inputsNo axiomsSource, line 131

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

- = signed/subtract0 = signed/zeroℚ = signed/SignedRational≤ = signed/at-most

vector/signed-scale-monotone

TheoremFor all inputsNo axiomsSource, line 167

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

0 = signed/zeroList = data/Listℚ = signed/SignedRational≤ = signed/at-most

matrix/at-most-empty

TheoremWorked exampleNo axiomsSource, line 272

matrix/at-most-empty :
  → matrix/at-most [] []

matrix/at-most-cons

TheoremFor all inputsNo axiomsSource, line 277

matrix/at-most-cons :
  (left-row right-row : List ℚ) (left-tail right-tail : List (List ℚ))
  (row-ordered : vector/at-most left-row right-row)
  (tail-ordered : matrix/at-most left-tail right-tail)
  → matrix/at-most (data/cons (List ℚ) left-row left-tail) (data/cons (List ℚ) right-row right-tail)

List = data/Listℚ = signed/SignedRational

matrix/at-most-reflexive

TheoremFor all inputsNo axiomsSource, line 299

matrix/at-most-reflexive :
  (rows : List (List ℚ))
  → matrix/at-most rows rows

List = data/Listℚ = signed/SignedRational

matrix/signed-scale-monotone

TheoremFor all inputsNo axiomsSource, line 323

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

0 = signed/zeroList = data/Listℚ = signed/SignedRational≤ = signed/at-most