Theorems · Inductive type · functional analysis

ContinuousFunctionalCalculus

(R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [IsTopologicalSemiring R] →
              [ContinuousStar R] → [inst_5 : Ring A] → [StarRing A] → [TopologicalSpace A] → [Algebra R A] → Prop

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

Cited by

331 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 155 definitions · uses no axioms

Assumes

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarRingStarRingTopologicalSpaceAlgebra