Theorems · Definition · functional analysis

cfc

{R : Type u_3} →
  {A : Type u_4} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : TopologicalSpace A] →
                  [inst_6 : Ring A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : Algebra R A] → [instCFC : ContinuousFunctionalCalculus R A p] → (R → R) → A → A

This is the continuous functional calculus of an element a : A applied to bare functions. When either a does not satisfy the predicate p (i.e., a is not IsStarNormal, IsSelfAdjoint, or 0 ≤ a when R is ℂ, ℝ, or ℝ≥0, respectively), or when f : R → R is not continuous on the spectrum of a, then cfc f a returns the junk value 0. This is the primary declaration intended for widespread use of the continuous functional calculus, and all the API applies to this declaration. For more information, see the module documentation for Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Cited by

228 results in Mathlib

Foundations

Depth 98 from the axioms, rests on 1,260 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarTopologicalSpaceRingStarRingAlgebraContinuousFunctionalCalculus