Theorems · Definition · functional analysis

continuousFunctionalCalculus

{A : Type u_1} →
  [inst : CStarAlgebra A] →
    (a : A) → [inst_1 : IsStarNormal a] → C(↑(spectrum ℂ a), ℂ) ≃⋆ₐ[ℂ] ↥(StarAlgebra.elemental ℂ a)

Continuous functional calculus. Given a normal element a : A of a unital C⋆-algebra, the continuous functional calculus is a StarAlgEquiv from the complex-valued continuous functions on the spectrum of a to the unital C⋆-subalgebra generated by a. Moreover, this equivalence identifies (ContinuousMap.id ℂ).restrict (spectrum ℂ a)) with a; see continuousFunctionalCalculus_map_id. As such it extends the polynomial functional calculus.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Cited by

2 results in Mathlib

Foundations

Depth 306 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CStarAlgebraIsStarNormal