instContinuousFunctionalCalculus — Mathlib

English

There exists a canonical continuous functional calculus for Real A with IsStarNormal.

Русский

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

LaTeX

$$$$ \\text{instContinuousFunctionalCalculus } 𝕜 A \\; \\Rightarrow \\text{CFC}(A) $$$$

Lean4

instance instContinuousFunctionalCalculus : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint :=
  SpectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM
    Complex.isometry_ofReal.isUniformEmbedding (.zero _)
    (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts)

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