instNonUnitalContinuousFunctionalCalculus

English

There exists a canonical nonunital continuous functional calculus for Real A given IsSelfAdjoint.

Русский

Существует канонический ненулевой непрерывный функциональный калькулятор для Real A при условии IsSelfAdjoint.

LaTeX

$$$$ \\text{instNonUnitalContinuousFunctionalCalculus } 𝕁 $$$$

Lean4

instance instNonUnitalContinuousFunctionalCalculus : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint :=
  QuasispectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
    Complex.isometry_ofReal.isUniformEmbedding (.zero _)
    (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts)

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