English
The eigenvalues of a Hermitian matrix can be computed from eigenvector basis and inner products as real numbers λ_i.
Русский
Собственные значения эрмитовой матрицы можно выразить через базис собственных векторов и скалярные произведения как действительные λ_i.
LaTeX
$$$\text{eigenvalues}_i = \Re\bigl(\langle v_i, A v_i \rangle\bigr)$, где $v_i$ — i-й вектор базиса собственных векторов.$$
Lean4
/-- **Diagonalization theorem**, **spectral theorem** for matrices; A Hermitian matrix can be
diagonalized by a change of basis. For the spectral theorem on linear maps, see
`LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply`. -/
theorem spectral_theorem :
A =
(eigenvectorUnitary hA : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues) *
(star (eigenvectorUnitary hA : Matrix n n 𝕜)) :=
by
rw [← star_mul_self_mul_eq_diagonal, mul_assoc, mul_assoc, (Matrix.mem_unitaryGroup_iff).mp (eigenvectorUnitary hA).2,
mul_one, ← mul_assoc, (Matrix.mem_unitaryGroup_iff).mp (eigenvectorUnitary hA).2, one_mul]
