trace_eq_sum_eigenvalues — Mathlib

English

If T is symmetric, then the real part of tr(T) equals the sum of its eigenvalues.

Русский

Если T симметричен, то вещественная часть следа T равна сумме его собственных значений.

LaTeX

$$Re(Tr(T)) = \sum_i λ_i$$

Lean4

theorem trace_eq_sum_eigenvalues {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : T.trace 𝕜 E = ∑ i, hT.eigenvalues hn i :=
  by
  let b := hT.eigenvectorBasis hn
  rw [T.trace_eq_sum_inner b, RCLike.ofReal_sum]
  apply Fintype.sum_congr
  intro i
  rw [hT.apply_eigenvectorBasis, inner_smul_real_right, inner_self_eq_norm_sq_to_K, b.norm_eq_one]
  simp [RCLike.ofReal_alg]

Похожие утверждения