eigenvalues_antitone — Mathlib

English

The sequence of eigenvalues of a self-adjoint operator is decreasing when indexed in the natural order after sorting by decreasing values.

Русский

Последовательность собственных значений самосопряжённого оператора упорядочена по убыванию.

LaTeX

$$$$ \text{If } h_T, \; (\lambda_i) \text{ are eigenvalues sorted in decreasing order, then } (\lambda_i) \text{ is antitone.} $$$$

Lean4

/-- Eigenvalues are sorted in decreasing order. -/
theorem eigenvalues_antitone (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : Antitone (hT.eigenvalues hn) :=
  by
  rw [eigenvalues_def, ← Function.comp_assoc]
  refine Monotone.comp_antitone ?_ ?_
  · apply Tuple.monotone_sort
  intro _ _ h
  exact Fin.rev_le_rev.mpr h

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