English
The basis vectors are eigenvectors with the corresponding eigenvalues.
Русский
Базисные векторы являются собственными векторами с соответствующими собственными значениями.
LaTeX
$$$$ T v_i = \lambda_i v_i, \quad i=1,\dots,n. $$$$
Lean4
/-- *Diagonalization theorem*, *spectral theorem*; version 2: A self-adjoint operator `T` on a
finite-dimensional inner product space `E` acts diagonally on the identification of `E` with
Euclidean space induced by an orthonormal basis of eigenvectors of `T`. -/
theorem eigenvectorBasis_apply_self_apply (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (v : E) (i : Fin n) :
(hT.eigenvectorBasis hn).repr (T v) i = hT.eigenvalues hn i * (hT.eigenvectorBasis hn).repr v i :=
by
suffices
∀ w : EuclideanSpace 𝕜 (Fin n),
T ((hT.eigenvectorBasis hn).repr.symm w) = (hT.eigenvectorBasis hn).repr.symm fun i => hT.eigenvalues hn i * w i
by
simpa [OrthonormalBasis.sum_repr_symm] using
congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i) (this ((hT.eigenvectorBasis hn).repr v))
intro w
simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, map_smul, apply_eigenvectorBasis]
apply Fintype.sum_congr
intro a
rw [smul_smul, mul_comm]
