
QR
Decomposition
Title: 
QR Decomposition 
Authors:

Jose Divasón and
Jesús Aransay

Submission date: 
20150212 
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 sideproduct, the GramSchmidt 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: 
[20150618]: The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces. 
BibTeX: 
@article{QR_DecompositionAFP,
author = {Jose Divasón and Jesús Aransay},
title = {QR Decomposition},
journal = {Archive of Formal Proofs},
month = feb,
year = 2015,
note = {\url{http://isaafp.org/entries/QR_Decomposition.html},
Formal proof development},
ISSN = {2150914x},
}

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.

