QR Decomposition

Title:	QR Decomposition
Authors:	Jose Divasón and Jesús Aransay
Submission date:	2015-02-12
Abstract:	QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a side-product, the Gram-Schmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry "Implementing field extensions of the form Q[sqrt(b)]" by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.
Change history:	[2015-06-18]: The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces.
BibTeX:	@article{QR_Decomposition-AFP, author = {Jose Divasón and Jesús Aransay}, title = {QR Decomposition}, journal = {Archive of Formal Proofs}, month = feb, year = 2015, note = {\url{http://isa-afp.org/entries/QR_Decomposition.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Gauss_Jordan, Rank_Nullity_Theorem, Real_Impl, Sqrt_Babylonian
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.