Reference · Matrices

rainbow.math.linear.matrix.shape

Matricessrc/rainbow/math/linear/matrix/shape.clj2 definitions, 7 theorems

Explicit width and rectangularity certificates for nested-List matrices. matrix/compatible rows values says every row has the same shape as `values`. matrix/rectangular rows is true for the empty matrix and, for a nonempty matrix, says every tail row has the same shape as the head row. The accompanying laws expose constructor/destructor APIs, transport compatibility across vector shape equality, show rectangularity is inherited by matrix tails, and recover compatibility with the first row. These types make raggedness explicit before transpose or matrix composition is added. Native and axiom-free on D63.

Depends onmath.finite.matrix

matrix/compatible :
  (x₁ : List (List ℚ)) (x₂ : List ℚ)
  → Prop

matrix/rectangular :
  (x₁ : List (List ℚ))
  → Prop

matrix/compatible-nil :
  (values : List ℚ)
  → matrix/compatible [] values

matrix/compatible-cons :
  (row : List ℚ) (tail : List (List ℚ)) (values : List ℚ)
  (head-shape : vector/same-shape row values)
  (tail-compatible : matrix/compatible tail values)
  → matrix/compatible (data/cons (List ℚ) row tail) values

matrix/compatible-head-shape :
  (row : List ℚ) (tail : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible (data/cons (List ℚ) row tail) values)
  → vector/same-shape row values

matrix/compatible-tail :
  (row : List ℚ) (tail : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible (data/cons (List ℚ) row tail) values)
  → matrix/compatible tail values

matrix/compatible-transport :
  (rows : List (List ℚ)) (left right : List ℚ)
  (reference-shape : vector/same-shape left right)
  (left-compatible : matrix/compatible rows left)
  → matrix/compatible rows right

matrix/rectangular-tail :
  (head : List ℚ) (tail : List (List ℚ))
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) head tail))
  → matrix/rectangular tail

matrix/compatible-with-head-of-rectangular :
  (head : List ℚ) (tail : List (List ℚ))
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) head tail))
  → matrix/compatible (data/cons (List ℚ) head tail) head