sharmaeklavya2 / theoremdep-source

Source files for TheoremDep - a theorem dependency tracker
https://sharmaeklavya2.github.io/theoremdep/
19 stars 1 forks source link

slight gap in proof of 'real matrix with real eigenvalues has real eigenvectors' #2

Closed josephpaulmartin closed 1 year ago

josephpaulmartin commented 1 year ago

The proof here doesn't cover the case when $v = u + \overline{u}$ is zero, and eigenvectors are not allowed to be zero. This occurs if and only if all of the components of $u$ are purely imaginary. In this case, $iu$ is a non-zero real eigenvector for $A$.

The following is an example of an amended proof.

If the components of $u$ are all purely imaginary, then $iu$ is a non-zero real eigenvector for $A$ and we're done. Otherwise, assume that at least one of the components of $u$ is not purely imaginary.

$Au = \lambda u$ $\implies$ $\overline{A}\overline{u} = \overline{\lambda} \overline{u}$ $\implies$ $A\overline{u} = \lambda \overline{u}$ $\implies$ $A(u + \overline{u}) = \lambda(u + \overline{u})$

Since at least one of the components of $u$ is not purely imaginary, $u + \overline{u}$ is non-zero. Therefore, $v = u+ \overline{u}$ is an eigenvector of $A$ corresponding to $\lambda$. Also $v = u + \overline{u} = 2\mathrm{Re}(u)$ is real.

sharmaeklavya2 commented 1 year ago

Thanks for finding this error! I have fixed it now. (If you think it's still wrong, feel free to reopen this issue.)