nonneg_eigenvalues — Mathlib

English

For a finite-dimensional space and a positive symmetric operator T, all eigenvalues are nonnegative.

Русский

Для конечномерного пространства и положительно симметричного оператора T все собственные значения неотрицательны.

LaTeX

$$$$\text{If } T \text{ is positive and symmetric, then } \lambda_i(T) \ge 0 \text{ for all eigenvalues } \lambda_i.$$$$

Lean4

theorem nonneg_eigenvalues [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsPositive)
    (hn : Module.finrank 𝕜 E = n) (i : Fin n) : 0 ≤ hT.isSymmetric.eigenvalues hn i := by
  simpa only [hT.isSymmetric.apply_eigenvectorBasis, inner_smul_real_left, RCLike.smul_re, inner_self_eq_norm_sq,
    OrthonormalBasis.norm_eq_one, one_pow, mul_one] using hT.right (hT.isSymmetric.eigenvectorBasis hn i)

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