trace_eq_sum_inner — Mathlib

English

If T is a symmetric linear operator on a finite-dimensional inner product space, then the trace of T equals the sum of its eigenvalues (counted with multiplicity).

Русский

Если T — симметричный линейный оператор в конечномерном внутреннем произведении, то след T равен сумме его собственных значений (с учётом кратностей).

LaTeX

$$Tr(T) = \sum_i λ_i, where λ_i are eigenvalues of T$$

Lean4

theorem trace_eq_sum_inner (T : E →ₗ[𝕜] E) (b : OrthonormalBasis ι 𝕜 E) : T.trace 𝕜 E = ∑ i, ⟪b i, T (b i)⟫_𝕜 := by
  classical
  rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]
  apply Fintype.sum_congr
  intro i
  rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply, b.repr_apply_apply]

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