Reference · Finite types, distributions and Markov chains

rainbow.math.finite.matrix

Finite types, distributions and Markov chainssrc/rainbow/math/finite/matrix.clj1 definitions, 3 theorems

Finite signed-rational matrices and their native action on vectors. A matrix is a List of signed-rational row vectors. Matrix-vector multiplication maps the existing exact dot product over those rows: matrix/vector-multiply rows values = map (dot _ values) rows The first laws establish the operator interface needed by finite-dimensional OR: a zero-like input maps to a zero-like output, equivalent inputs map to equivalent outputs, and the operator preserves same-shaped vector addition. Native and axiom-free on D63.

Depends onalgorithms.proofs.counterfactual-distance-laws

matrix/vector-multiply :
  (x₁ : List (List ℚ)) (x₂ : List ℚ)
  → List ℚ

matrix/vector-multiply-zero-like :
  (rows : List (List ℚ)) (values : List ℚ)
  → vector/equivalent (multiply) (vector/zero-like (matrix/vector-multiply rows values))
  where multiply := matrix/vector-multiply rows (vector/zero-like values)

matrix/vector-multiply-respects-equivalence :
  (rows : List (List ℚ)) (left right : List ℚ) (same : vector/equivalent left right)
  → vector/equivalent (matrix/vector-multiply rows left) (matrix/vector-multiply rows right)

matrix/vector-multiply-additive :
  (rows : List (List ℚ)) (left right : List ℚ) (shape : vector/same-shape left right)
  → vector/equivalent (multiply) (add)
  where add := vector/add (matrix/vector-multiply rows left) (matrix/vector-multiply rows right)
  where multiply := matrix/vector-multiply rows (vector/add left right)