noncomputable def
symmetric_eigenvalue_function
{n : ℕ}
(X : ↥(selfAdjoint.submodule ℝ (Matrix (Fin n) (Fin n) ℝ)))
:
Fin n → ℝ
Definition 7.10: the eigenvalue function λ : 𝕊^n → ℝ^n sends a real symmetric matrix to its
eigenvalues listed in weakly decreasing order.
Instances For
@[simp]
theorem
symmetric_eigenvalue_function_apply
{n : ℕ}
(X : ↥(selfAdjoint.submodule ℝ (Matrix (Fin n) (Fin n) ℝ)))
(i : Fin n)
:
symmetric_eigenvalue_function X i = ⋯.eigenvalues₀ (Fin.cast ⋯ i)
The i-th coordinate of symmetric_eigenvalue_function X is the i-th ordered eigenvalue of
X.
theorem
symmetric_eigenvalue_function_antitone
{n : ℕ}
(X : ↥(selfAdjoint.submodule ℝ (Matrix (Fin n) (Fin n) ℝ)))
:
Antitone (symmetric_eigenvalue_function X)
The coordinates of symmetric_eigenvalue_function X are weakly decreasing along the natural
order on Fin n.