Module Posdef

module Posdef: sig .. end

Proving positive definiteness of matrices.

val check_itv : (float * float) array array -> bool

Takes as input a square interval matrix m of size nxn. If it returns true, then all symmetric matrices in this interval are positive definite (otherwise, one of these matrices is either not symmetric positive definite or its smallest eigenvalue is too small for the proof to succeed). If m is not symmetric or one of its elements is not finite, false is returned.

val check : Q.t array array -> bool

Takes as input a square matrix of Q.t of size nxn and returns 1 if it manages to prove that the matrix is symmetric positive definite and 0 otherwise (i.e. the matrix is either not symmetric positive definite or its smallest eigenvalue is too small for the proof to succeed).

val check_complete : Q.t array array -> bool

Same as check but complete (returns true iff the input is positive definite). This is however implemented with rational arithmetic and may be dramatically slower.

val check_PSD : Q.t array array -> bool

Same as check_complete but returns true iff the input is positive *semi*definite (rather than positive definite).

val string_of_float_bin : float -> string