Structures · Analysis

ContinuousFunctionalCalculus

A star R-algebra A has a continuous functional calculus for elements satisfying the property p : A → Prop if + for every such element a : A there is a star algebra homomorphism cfcHom : C(spectrum R a, R) →⋆ₐ[R] A sending the (restriction of) the identity map to a. + cfcHom is continuous and injective and the spectrum of the image of function f is its range. + cfcHom preserves the property p. + p 0 is true, which ensures among other things that p ≠ fun _ ↦ False. The property p is marked as an outParam so that the user need not specify it. In practice, + for R := ℂ, we choose p := IsStarNormal, + for R := ℝ, we choose p := IsSelfAdjoint, + for R := ℝ≥0, we choose p := (0 ≤ ·). Instead of directly providing the data we opt instead for a Prop class. In all relevant cases, the continuous functional calculus is uniquely determined, and utilizing this approach prevents diamonds or problems arising from multiple instances.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Shape

3 explicit arguments · adds predicate_zero, compactSpace_spectrum, spectrum_nonempty, exists_cfc_of_predicate