diagonalization_symm_apply — Mathlib

English

The diagonalization map is compatible with multiplication by eigenvalues on the eigenbasis, i.e., the symmetrized decomposition respects the eigenvalues.

Русский

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

LaTeX

$$$$ h_T.diagonalization \cdot \bigl( T v \bigr) = \underbrace{(\mu v)}_{\text{on } \mathrm{Eig}(T,\mu)}. $$$$

Lean4

@[simp]
theorem diagonalization_symm_apply (hT : T.IsSymmetric) (w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ) :
    hT.diagonalization.symm w = ∑ μ, w μ :=
  hT.direct_sum_isInternal.isometryL2OfOrthogonalFamily_symm_apply hT.orthogonalFamily_eigenspaces' w

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