Data.NumIdr.Matrix

Reexports

Definitions

Matrix : Nat -> Nat -> Type -> Type

  A matrix is a rank-2 array.

Totality: total
Visibility: public export

Matrix' : Nat -> Type -> Type

  A synonym for a square matrix with dimensions of length `n`.

Totality: total
Visibility: public export

matrix : {default B rep : Rep} -> RepConstraint rep a => Vect m (Vect n a) -> Matrix m n a

  Construct a matrix with the given order and elements.

Totality: total
Visibility: export

repeatDiag : {default B rep : Rep} -> RepConstraint rep a => a -> a -> Matrix m n a

  Construct a matrix with a specific value along the diagonal.
  
  @ diag  The value to repeat along the diagonal
  @ other The value to repeat elsewhere

Totality: total
Visibility: export

fromDiag : {default B rep : Rep} -> RepConstraint rep a => Vect (minimum m n) a -> a -> Matrix m n a

  Construct a matrix given its diagonal elements.
  
  @ diag  The elements of the matrix's diagonal
  @ other The value to repeat elsewhere

Totality: total
Visibility: export

permuteM : {default B rep : Rep} -> RepConstraint rep a => Num a => Permutation n -> Matrix' n a

  Construct a permutation matrix based on the given permutation.

Totality: total
Visibility: export

scale : {default B rep : Rep} -> RepConstraint rep a => Num a => a -> Matrix' n a

  Construct the matrix that scales a vector by the given value.

Totality: total
Visibility: export

rotate2D : {default B rep : Rep} -> RepConstraint rep Double => Double -> Matrix' 2 Double

  Construct a 2D rotation matrix that rotates by the given angle (in radians).

Totality: total
Visibility: export

rotate3DX : {default B rep : Rep} -> RepConstraint rep Double => Double -> Matrix' 3 Double

  Construct a 3D rotation matrix around the x-axis.

Totality: total
Visibility: export

rotate3DY : {default B rep : Rep} -> RepConstraint rep Double => Double -> Matrix' 3 Double

  Construct a 3D rotation matrix around the y-axis.

Totality: total
Visibility: export

rotate3DZ : {default B rep : Rep} -> RepConstraint rep Double => Double -> Matrix' 3 Double

  Construct a 3D rotation matrix around the z-axis.

Totality: total
Visibility: export

reflect : {default B rep : Rep} -> RepConstraint rep a => Neg a => Fin n -> Matrix' n a

Totality: total
Visibility: export

reflectX : {default B rep : Rep} -> RepConstraint rep a => Neg a => Matrix' (1 + n) a

Totality: total
Visibility: export

reflectY : {default B rep : Rep} -> RepConstraint rep a => Neg a => Matrix' (2 + n) a

Totality: total
Visibility: export

reflectZ : {default B rep : Rep} -> RepConstraint rep a => Neg a => Matrix' (3 + n) a

Totality: total
Visibility: export

index : Fin m -> Fin n -> Matrix m n a -> a

  Index the matrix at the given coordinates.

Totality: total
Visibility: export

indexNB : Nat -> Nat -> Matrix m n a -> Maybe a

  Index the matrix at the given coordinates, returning `Nothing` if the
  coordinates are out of bounds.

Totality: total
Visibility: export

getRow : Fin m -> Matrix m n a -> Vector n a

  Return a row of the matrix as a vector.

Totality: total
Visibility: export

getColumn : Fin n -> Matrix m n a -> Vector m a

  Return a column of the matrix as a vector.

Totality: total
Visibility: export

diagonal' : Matrix m n a -> Vector (minimum m n) a

  Return the diagonal elements of the matrix as a vector.

Totality: total
Visibility: export

diagonal : Matrix' n a -> Vector n a

  Return the diagonal elements of the matrix as a vector.

Totality: total
Visibility: export

minor : Fin (S m) -> Fin (S n) -> Matrix (S m) (S n) a -> Matrix m n a

  Return a minor of the matrix, i.e. the matrix formed by removing a
  single row and column.

Totality: total
Visibility: export

upperTriangle : Num a => Matrix m n a -> Matrix m n a

Totality: total
Visibility: export

lowerTriangle : Num a => Matrix m n a -> Matrix m n a

Totality: total
Visibility: export

upperTriangleStrict : Num a => Matrix m n a -> Matrix m n a

Totality: total
Visibility: export

lowerTriangleStrict : Num a => Matrix m n a -> Matrix m n a

Totality: total
Visibility: export

vconcat : Matrix m n a -> Matrix m' n a -> Matrix (m + m') n a

  Concatenate two matrices vertically.

Totality: total
Visibility: export

hconcat : Matrix m n a -> Matrix m n' a -> Matrix m (n + n') a

  Concatenate two matrices horizontally.

Totality: total
Visibility: export

vstack : Vect m (Vector n a) -> Matrix m n a

  Stack row vectors to form a matrix.

Totality: total
Visibility: export

hstack : Vect n (Vector m a) -> Matrix m n a

  Stack column vectors to form a matrix.

Totality: total
Visibility: export

swapRows : Fin m -> Fin m -> Matrix m n a -> Matrix m n a

  Swap two rows of a matrix.

Totality: total
Visibility: export

swapColumns : Fin n -> Fin n -> Matrix m n a -> Matrix m n a

  Swap two columns of a matrix.

Totality: total
Visibility: export

permuteRows : Permutation m -> Matrix m n a -> Matrix m n a

  Permute the rows of a matrix.

Totality: total
Visibility: export

permuteColumns : Permutation n -> Matrix m n a -> Matrix m n a

  Permute the columns of a matrix.

Totality: total
Visibility: export

outer : Num a => Vector m a -> Vector n a -> Matrix m n a

  Calculate the outer product of two vectors as a matrix.

Totality: total
Visibility: export

trace : Num a => Matrix m n a -> a

  Calculate the trace of a matrix, i.e. the sum of its diagonal elements.

Totality: total
Visibility: export

reflectNormal : (Neg a, Fractional a) => Vector n a -> Matrix' n a

  Construct a matrix that reflects a vector along a hyperplane of the
  given normal vector. The input does not have to be a unit vector.

Totality: total
Visibility: export

record DecompLU : Matrix m n a -> Type

  The LU decomposition of a matrix.
  
  LU decomposition factors a matrix A into two matrices: a lower triangular
  matrix L, and an upper triangular matrix U, such that A = LU.

Totality: total
Visibility: export
Constructor: 

MkLU : Matrix m n a -> DecompLU mat

Projections:

.lower : Num a => DecompLU mat -> Matrix m (minimum m n) a

  The lower triangular matrix L of the LU decomposition.

.lower' : Num a => DecompLU mat -> Matrix' n a

  The lower triangular matrix L of the LU decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

.lu : DecompLU mat -> Matrix m n a

.upper : Num a => DecompLU mat -> Matrix (minimum m n) n a

  The upper triangular matrix U of the LU decomposition.

.upper' : Num a => DecompLU mat -> Matrix' n a

  The upper triangular matrix U of the LU decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

lower : Num a => DecompLU mat -> Matrix m (minimum m n) a

  The lower triangular matrix L of the LU decomposition.

Totality: total
Visibility: export

.lower : Num a => DecompLU mat -> Matrix m (minimum m n) a

  The lower triangular matrix L of the LU decomposition.

Totality: total
Visibility: export

lower' : Num a => DecompLU mat -> Matrix' n a

  The lower triangular matrix L of the LU decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

.lower' : Num a => DecompLU mat -> Matrix' n a

  The lower triangular matrix L of the LU decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

upper : Num a => DecompLU mat -> Matrix (minimum m n) n a

  The upper triangular matrix U of the LU decomposition.

Totality: total
Visibility: export

.upper : Num a => DecompLU mat -> Matrix (minimum m n) n a

  The upper triangular matrix U of the LU decomposition.

Totality: total
Visibility: export

upper' : Num a => DecompLU mat -> Matrix' n a

  The upper triangular matrix U of the LU decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

.upper' : Num a => DecompLU mat -> Matrix' n a

  The upper triangular matrix U of the LU decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

decompLU : Field a => (mat : Matrix m n a) -> Maybe (DecompLU mat)

  Calculate the LU decomposition of a matrix, returning `Nothing` if one
  does not exist.

Totality: total
Visibility: export

record DecompLUP : Matrix m n a -> Type

  The LUP decomposition of a matrix.
  
  LUP decomposition is similar to LU decomposition, but the matrix may have
  its rows permuted before being factored. More formally, an LUP decomposition
  of a matrix A consists of a lower triangular matrix L, an upper triangular
  matrix U, and a permutation matrix P, such that PA = LU.

Totality: total
Visibility: export
Constructor: 

MkLUP : Matrix m n a -> Permutation m -> Nat -> DecompLUP mat

Projections:

.lower : Num a => DecompLUP mat -> Matrix m (minimum m n) a

  The lower triangular matrix L of the LUP decomposition.

.lower' : Num a => DecompLUP mat -> Matrix' n a

  The lower triangular matrix L of the LUP decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

.lu : DecompLUP mat -> Matrix m n a

.p : DecompLUP mat -> Permutation m

.permute : DecompLUP mat -> Permutation m

  The row permutation of the LUP decomposition.

.sw : DecompLUP mat -> Nat

.upper : Num a => DecompLUP mat -> Matrix (minimum m n) n a

  The upper triangular matrix U of the LUP decomposition.

.upper' : Num a => DecompLUP mat -> Matrix' n a

  The upper triangular matrix U of the LUP decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

lower : Num a => DecompLUP mat -> Matrix m (minimum m n) a

  The lower triangular matrix L of the LUP decomposition.

Totality: total
Visibility: export

.lower : Num a => DecompLUP mat -> Matrix m (minimum m n) a

  The lower triangular matrix L of the LUP decomposition.

Totality: total
Visibility: export

lower' : Num a => DecompLUP mat -> Matrix' n a

  The lower triangular matrix L of the LUP decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

.lower' : Num a => DecompLUP mat -> Matrix' n a

  The lower triangular matrix L of the LUP decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

upper : Num a => DecompLUP mat -> Matrix (minimum m n) n a

  The upper triangular matrix U of the LUP decomposition.

Totality: total
Visibility: export

.upper : Num a => DecompLUP mat -> Matrix (minimum m n) n a

  The upper triangular matrix U of the LUP decomposition.

Totality: total
Visibility: export

upper' : Num a => DecompLUP mat -> Matrix' n a

  The upper triangular matrix U of the LUP decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

.upper' : Num a => DecompLUP mat -> Matrix' n a

  The upper triangular matrix U of the LUP decomposition.
  
  This accessor is intended to be used for square matrix decompositions.

Totality: total
Visibility: export

permute : DecompLUP mat -> Permutation m

  The row permutation of the LUP decomposition.

Totality: total
Visibility: export

.permute : DecompLUP mat -> Permutation m

  The row permutation of the LUP decomposition.

Totality: total
Visibility: export

numSwaps : DecompLUP mat -> Nat

  The number of swaps in the permutation of the LUP decomposition.
  
  This is stored along with the permutation in order to increase the
  efficiency of certain algorithms.

Totality: total
Visibility: export

fromLU : DecompLU mat -> DecompLUP mat

  Convert an LU decomposition into an LUP decomposition.

Totality: total
Visibility: export

decompLUP : FieldCmp a => (mat : Matrix m n a) -> DecompLUP mat

  Calculate the LUP decomposition of a matrix.

Totality: total
Visibility: export

detWithLUP : Num a => (mat : Matrix' n a) -> DecompLUP mat -> a

  Calculate the determinant of a matrix given its LUP decomposition.

Totality: total
Visibility: export

det : FieldCmp a => Matrix' n a -> a

  Calculate the determinant of a matrix.

Totality: total
Visibility: export

solveLowerTri : Field a => Matrix' n a -> Vector n a -> Maybe (Vector n a)

  Solve a linear equation, assuming the matrix is lower triangular.
  Any entries other than those below the diagonal are ignored.

Totality: total
Visibility: export

solveUpperTri : Field a => Matrix' n a -> Vector n a -> Maybe (Vector n a)

  Solve a linear equation, assuming the matrix is upper triangular.
  Any entries other than those above the diagonal are ignored.

Totality: total
Visibility: export

solveWithLUP : Field a => (mat : Matrix' n a) -> DecompLUP mat -> Vector n a -> Maybe (Vector n a)

  Solve a linear equation, given a matrix and its LUP decomposition.

Totality: total
Visibility: export

solve : FieldCmp a => Matrix' n a -> Vector n a -> Maybe (Vector n a)

  Solve a linear equation given a matrix.

Totality: total
Visibility: export

invertible : FieldCmp a => Matrix' n a -> Bool

  Determine whether a matrix has an inverse.

Totality: total
Visibility: export

tryInverse : FieldCmp a => Matrix' n a -> Maybe (Matrix' n a)

  Try to invert a square matrix, returning `Nothing` if an inverse
  does not exist.

Totality: total
Visibility: export