coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Cholesky diagonalisation in Coq?

From: "Roland Zumkeller" <Roland.Zumkeller AT polytechnique.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]Cholesky diagonalisation in Coq?
Date: Tue, 12 Dec 2006 16:36:53 -0500
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:sender:to:subject:mime-version:content-type:x-google-sender-auth; b=G9EUtMH7o27ykaKz8x5bfbKT88Tfb0/ngUaybWT8AsO3raLONUxEZBfsEc4gw8+hJ7lhUY9jEA8yNbsjD9EPSmxRcQF6BieBCkKDDLG7vzgjmYQJzJ3iYv03HENBN/Xo6SDIOoqSJCIl82T9k04yjbw3qE98XKcd+mkTP2v76P0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

does anyone know of a Coq formalisation of an algorithm that diagonalises matrices?
More specifically I would be interested in the Cholesky decomposition of a symmetric positive definite matrix into LL^T or LDL^T.

Thanks,

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/

[Coq-Club]Cholesky diagonalisation in Coq?, Roland Zumkeller