QR Decomposition

  1. Divasón Mallagaray, José
  2. Aransay Azofra, Jesús María
Revista:
Archive of Formal Proofs

ISSN: 2150-914X

Año de publicación: 2015

Volumen: 2015

Páginas: 1-101

Tipo: Artículo

Otras publicaciones en: Archive of Formal Proofs

Resumen

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