 ## LinearAlgebraTraits_d

### Definition

The data type LinearAlgebraTraits_d encapsulates two classes Matrix, Vector and many functions of basic linear algebra. An instance of data type Matrix is a matrix of variables of type NT. Accordingly, Vector implements vectors of variables of type NT. Most functions of linear algebra are checkable, i.e., the programs can be asked for a proof that their output is correct. For example, if the linear system solver declares a linear system A x = b unsolvable it also returns a vector c such that cT A = 0 and cT b 0.

### Types

 LinearAlgebraTraits_d::NT the number type of the components. LinearAlgebraTraits_d::Vector the vector type. LinearAlgebraTraits_d::Matrix the matrix type.

### Operations

static Matrix LA.transpose ( Matrix M)
returns MT (a M.column_dimension()  × M.column_dimension() - matrix).

static bool LA.inverse ( Matrix M, Matrix& I, NT& D, Vector& c)
determines whether M has an inverse. It also computes either the inverse as (1/D) · I or when no inverse exists, a vector c such that cT · M = 0 .
Precondition: M is square.

static Matrix LA.inverse ( Matrix M, NT& D)
returns the inverse matrix of M. More precisely, 1/D times the matrix returned is the inverse of M.

Precondition: determinant(M) != 0.
Precondition: M is square.

static NT
 LA.determinant ( Matrix M, Matrix& L, Matrix& U, std::vector& q, Vector& c)
returns the determinant D of M and sufficient information to verify that the value of the determinant is correct. If the determinant is zero then c is a vector such that cT · M = 0. If the determinant is non-zero then L and U are lower and upper diagonal matrices respectively and q encodes a permutation matrix Q with Q(i,j) = 1 iff i = q(j) such that L · M · Q = U, L(0,0) = 1, L(i,i) = U(i - 1,i - 1) for all i, 1 i < n, and D = s · U(n - 1,n - 1) where s is the determinant of Q.
Precondition: M is square.

static bool
 LA.verify_determinant ( Matrix M, NT D, Matrix& L, Matrix& U, std::vector q, Vector& c)
verifies the conditions stated above.

static NT LA.determinant ( Matrix M)
returns the determinant of M.
Precondition: M is square.

static int LA.sign_of_determinant ( Matrix M)
returns the sign of the determinant of M.
Precondition: M is square.

static bool
 LA.linear_solver ( Matrix M, Vector b, Vector& x, NT& D, Matrix& spanning_vectors, Vector& c)
determines the complete solution space of the linear system M · x = b. If the system is unsolvable then cT · M = 0 and cT · b 0. If the system is solvable then (1/D) x is a solution, and the columns of spanning_vectors are a maximal set of linearly independent solutions to the corresponding homogeneous system.
Precondition: M.row_dimension() = b.dimension().

static bool
 LA.linear_solver ( Matrix M, Vector b, Vector& x, NT& D, Vector& c)
determines whether the linear system M · x = b is solvable. If yes, then (1/D) x is a solution, if not then cT · M = 0 and cT · b 0.
Precondition: M.row_dimension() = b.dimension().

static bool
 LA.linear_solver ( Matrix M, Vector b, Vector& x, NT& D)
as above, but without the witness c
Precondition: M.row_dimension() = b.dimension().

static bool LA.is_solvable ( Matrix M, Vector b)
determines whether the system M · x = b is solvable

Precondition: M.row_dimension() = b.dimension().

static bool LA.homogeneous_linear_solver ( Matrix M, Vector& x)
determines whether the homogeneous linear system M · x = 0 has a non - trivial solution. If yes, then x is such a solution.

static int
 LA.homogeneous_linear_solver ( Matrix M, Matrix& spanning_vecs)
determines the solution space of the homogeneous linear system M · x = 0. It returns the dimension of the solution space. Moreover the columns of spanning_vecs span the solution space.

static int
 LA.independent_columns ( Matrix M, std::vector& columns)
returns the indices of a maximal subset of independent columns of M.

static int LA.rank ( Matrix M)
returns the rank of matrix M