Reference · Matrices

rainbow.math.linear.matrix.transpose-order

Matricessrc/rainbow/math/linear/matrix/transpose_order.clj0 definitions, 4 theorems

Pointwise order and nonnegativity for total native matrix transpose. Column insertion preserves entrywise nonnegativity and is jointly monotone in its vector and matrix inputs. Structural lifting through the reducible total transpose then proves that transpose preserves both zero lower bounds and matrix pointwise order, including the established ragged semantics. Native and axiom-free on D63.

Depends onmath.linear.matrix.positive-action

matrix/prepend-column-nonnegative :
  (values : List ℚ) (columns : List (List ℚ))
  (values-positive : vector/at-most (vector/zero-like values) values)
  (columns-positive : matrix/at-most (matrix/zero-like columns) columns)
  → matrix/at-most (matrix/zero-like (matrix/prepend-column values columns)) (matrix/prepend-column values columns)

matrix/prepend-column-monotone :
  (left-values right-values : List ℚ) (left-columns right-columns : List (List ℚ))
  (values-ordered : vector/at-most left-values right-values)
  (columns-ordered : matrix/at-most left-columns right-columns)
  → matrix/at-most (column₁) (column)
  where column := matrix/prepend-column right-values right-columns
  where column₁ := matrix/prepend-column left-values left-columns

matrix/transpose-nonnegative :
  (rows : List (List ℚ)) (positive : matrix/at-most (matrix/zero-like rows) rows)
  → matrix/at-most (matrix/zero-like (matrix/transpose rows)) (matrix/transpose rows)

matrix/transpose-monotone :
  (left right : List (List ℚ)) (ordered : matrix/at-most left right)
  → matrix/at-most (matrix/transpose left) (matrix/transpose right)