A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem

Resumen

In this paper we show how a thoughtful reusing of libraries can provide concise proofs of non-trivial mathematical results. Concretely, we formalise in Isabelle/HOL a proof of the Fundamental Theorem of Linear Algebra for vector spaces over inner product spaces, the Gram–Schmidt process of orthogonalising vectors over (Formula presented.), its application to get the (Formula presented.) decomposition of a matrix, and the least squares approximation of systems of linear equations without solution, in a modest number of lines (ca. 2700). This work intensively reuses previous results, such as the Rank–Nullity theorem and various applications of the Gauss–Jordan algorithm. The formalisation is also accompanied by code generation and refinements that enable the execution of the presented algorithms in Isabelle and SML. © 2016 Springer Science+Business Media Dordrecht