cfcAux_id — Mathlib

English

For a Hermitian matrix A, applying the functional calculus to the identity function on its spectrum recovers A itself.

Русский

Для эрмитовой матрицы A применение непрерывного функционального калькулятора к тождественной функции на спектре возвращает саму A.

LaTeX

$$IsHermitian(A) ⇒ cfcAux( restrict(spectrum ℝ A) id ) = A$$

Lean4

theorem cfcAux_id : hA.cfcAux (.restrict (spectrum ℝ A) (.id ℝ)) = A :=
  by
  conv_rhs => rw [hA.spectral_theorem]
  congr!

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