Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof resit / 6 / b / i / Solution

The normal equations for linear least squares areThe supplied QR decomposition gives full column rank because $R$ is invertible and $Q^{T}Q=I$. Hence, for every nonzero $u$, $u^T{A}^{T}Au=\Vert Au{\Vert }_2^2>0$. Thus $A^{T}A$ is a symmetric positive-definite matrix and the displayed square system is nonsingular.