### 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.

BSD License### Change history

#### June 18, 2015

The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces.### Topics

### Theories of QR_Decomposition

- Miscellaneous_QR
- Projections
- Gram_Schmidt
- QR_Decomposition
- Least_Squares_Approximation
- Examples_QR_Abstract_Float
- Examples_QR_Abstract_Symbolic
- IArray_Addenda_QR
- Matrix_To_IArray_QR
- Gram_Schmidt_IArrays
- QR_Decomposition_IArrays
- Examples_QR_IArrays_Float
- Examples_QR_IArrays_Symbolic
- Generalizations2
- QR_Efficient