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 / a / ii

Set $y=P^{T}x$. Because $P$ is an orthogonal matrix, $x=Py$ and $x=0$ exactly when $y=0$. The preceding diagonalization givesConsequently $x^{T}Ax\ge 0$, with equality only when $x=0$. The matrix is a symmetric positive-definite matrix, not merely positive semidefinite. In the original coordinates the same identity iswhich also makes positivity transparent.