diagonalization — Mathlib

English

The operator acts diagonally on the decomposition into eigenspaces: on each eigenspace, it multiplies by the corresponding eigenvalue.

Русский

Оператор действует диагонально на разложении по эйгенпространствам: на каждом эйгенпространстве умножает на соответствующее собственное значение.

LaTeX

$$$$ T|_{\mathrm{Eig}(T,\mu)} = \mu \cdot \mathrm{id}. $$$$

Lean4

/-- Isometry from an inner product space `E` to the direct sum of the eigenspaces of some
self-adjoint operator `T` on `E`. -/
noncomputable def diagonalization (hT : T.IsSymmetric) : E ≃ₗᵢ[𝕜] PiLp 2 fun μ : Eigenvalues T => eigenspace T μ :=
  hT.direct_sum_isInternal.isometryL2OfOrthogonalFamily hT.orthogonalFamily_eigenspaces'

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