Reference · Matrices

rainbow.math.linear.matrix.action-associative

Matricessrc/rainbow/math/linear/matrix/action_associative.clj0 definitions, 6 theorems

Finite matrix action is adjoint to native transpose. dot (matrix/vector-multiply (transpose rows) coefficients) values ~ dot coefficients (matrix/vector-multiply rows values) Coefficients must have one component per row and every row must match the value vector. Empty, singleton, and multirow cases are separate opaque boundaries so the small kernel need not normalize transpose, column insertion, dot, and nested List recursors simultaneously. Native and axiom-free on D63.

Depends onmath.linear.matrix.action-prepend

vector/dot-cons-singleton :
  (coefficient : ℚ) (coefficient-tail : List ℚ) (value : ℚ)
  → vector/dot (cons) [value] = coefficient · value
  where cons := data/cons ℚ coefficient coefficient-tail

matrix/vector-action-associative-empty :
  (coefficients values : List ℚ)
  → vector/dot (multiply) values = vector/dot coefficients (matrix/vector-multiply [] values)
  where multiply := matrix/vector-multiply (matrix/transpose []) coefficients

matrix/vector-action-associative-single :
  (row : List ℚ) (coefficient : ℚ) (coefficient-tail values : List ℚ)
  → vector/dot (multiply) values = vector/dot (data/cons ℚ coefficient coefficient-tail) (matrix/vector-multiply [row] values)
  where multiply := matrix/vector-multiply (matrix/transpose [row]) (data/cons ℚ coefficient coefficient-tail)

matrix/vector-action-associative-cons-cons :
  (row second : List ℚ) (rest : List (List ℚ)) (coefficient : ℚ)
  (coefficient-tail values : List ℚ)
  (rows-compatible : matrix/compatible (data/cons (List ℚ) row (data/cons (List ℚ) second rest)) values)
  (tail-associative : vector/dot (multiply₁) values = vector/dot coefficient-tail (multiply₃))
  → vector/dot (multiply) values = vector/dot (data/cons ℚ coefficient coefficient-tail) (multiply₂)
  where multiply := matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) row (data/cons (List ℚ) second rest))) (data/cons ℚ coefficient coefficient-tail)
  where multiply₁ := matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) second rest)) coefficient-tail
  where multiply₂ := matrix/vector-multiply (data/cons (List ℚ) row (data/cons (List ℚ) second rest)) values
  where multiply₃ := matrix/vector-multiply (data/cons (List ℚ) second rest) values

matrix/vector-action-associative-cons :
  (row : List ℚ) (tail : List (List ℚ))
  (tail-law : ∀ (coefficients : List ℚ), ∀ (values : List ℚ), ∀ (coefficient-shape : vector/same-shape coefficients (matrix/column-shape tail)), ∀ (rows-compatible : matrix/compatible tail values), vector/dot (matrix/vector-multiply (matrix/transpose tail) coefficients) values = vector/dot coefficients (matrix/vector-multiply tail values))
  (coefficients values : List ℚ)
  (coefficient-shape : vector/same-shape coefficients (matrix/column-shape (data/cons (List ℚ) row tail)))
  (rows-compatible : matrix/compatible (data/cons (List ℚ) row tail) values)
  → vector/dot (multiply) values = vector/dot coefficients (multiply₁)
  where multiply := matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) row tail)) coefficients
  where multiply₁ := matrix/vector-multiply (data/cons (List ℚ) row tail) values

matrix/vector-action-associative :
  (rows : List (List ℚ)) (coefficients values : List ℚ)
  (coefficient-shape : vector/same-shape coefficients (matrix/column-shape rows))
  (rows-compatible : matrix/compatible rows values)
  → vector/dot (multiply) values = vector/dot coefficients (matrix/vector-multiply rows values)
  where multiply := matrix/vector-multiply (matrix/transpose rows) coefficients