English
A Hermitian matrix can be diagonalized by a unitary change of basis: A = U diag(λ) U*.
Русский
Гермитова матрица приводится к диагональному виду при помощи унитарного перехода базиса: A = U diag(λ) U*.
LaTeX
$$$A = (eigenvectorUnitary(h_A)) \; \mathrm{diag}(\lambda_1,\ldots,\lambda_n) \; (eigenvectorUnitary(h_A))^*$$$
Lean4
/-- Unitary diagonalization of a Hermitian matrix. -/
theorem star_mul_self_mul_eq_diagonal :
(star (eigenvectorUnitary hA : Matrix n n 𝕜)) * A * (eigenvectorUnitary hA : Matrix n n 𝕜) =
diagonal (RCLike.ofReal ∘ hA.eigenvalues) :=
by
apply Matrix.toEuclideanLin.injective
apply (EuclideanSpace.basisFun n 𝕜).toBasis.ext
intro i
simp only [toEuclideanLin_apply, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply,
EuclideanSpace.ofLp_single, ← mulVec_mulVec, eigenvectorUnitary_mulVec, ← mulVec_mulVec, mulVec_eigenvectorBasis,
Matrix.diagonal_mulVec_single, mulVec_smul, star_eigenvectorUnitary_mulVec, RCLike.real_smul_eq_coe_smul (K := 𝕜),
WithLp.toLp_smul, EuclideanSpace.toLp_single, Function.comp_apply, mul_one]
apply PiLp.ext
intro j
simp only [PiLp.smul_apply, EuclideanSpace.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]
