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

### License

BSD License

### History

June 18, 2015
  The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces.

### Topics

- Computer science/Algorithms/Mathematical
- Mathematics/Algebra

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

### Depends on

- Gauss-Jordan Algorithm and Its Applications
- Rank-Nullity Theorem in Linear Algebra
- Implementing field extensions of the form Q[sqrt(b)]
- Computing N-th Roots using the Babylonian Method

### Auto-related entries

- Echelon Form
- Finger Trees

## Cite

×

QR_Decomposition-AFP

    @article{QR_Decomposition-AFP,
      author  = {Jose Divasón and Jesús Aransay},
      title   = {QR Decomposition},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/QR_Decomposition.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Feb 13, 2015 : Isabelle2014