Documentation

Mathlib.Analysis.CstarAlgebra.ContinuousFunctionalCalculus.NonUnital

The continuous functional calculus for non-unital algebras #

This file defines a generic API for the continuous functional calculus in non-unital algebras which is suitable in a wide range of settings. The design is intended to match as closely as possible that for unital algebras in Mathlib.Analysis.CstarAlgebra.ContinuousFunctionalCalculus.Unital. Changes to either file should be mirrored in its counterpart whenever possible. The underlying reasons for the design decisions in the unital case apply equally in the non-unital case. See the module documentation in that file for more information.

A continuous functional calculus for an element a : A in a non-unital topological R-algebra is a continuous extension of the polynomial functional calculus (i.e., Polynomial.aeval) for polynomials with no constant term to continuous R-valued functions on quasispectrum R a which vanish at zero. More precisely, it is a continuous star algebra homomorphism C(quasispectrum R a, R)₀ →⋆ₙₐ[R] A that sends (ContinuousMap.id R).restrict (quasispectrum R a) to a. In all cases of interest (e.g., when quasispectrum R a is compact and R is ℝ≥0, , or ), this is sufficient to uniquely determine the continuous functional calculus which is encoded in the UniqueNonUnitalContinuousFunctionalCalculus class.

Main declarations #

Main theorems #

A non-unital 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 non-unital star algebra homomorphism cfcₙHom : C(quasispectrum R a, R)₀ →⋆ₙₐ[R] A sending the (restriction of) the identity map to a.
  • cfcₙHom is a closed embedding for which the quasispectrum of the image of function f is its range.
  • cfcₙHom preserves the property p.

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.

Instances
    theorem NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate {R : Type u_1} {A : Type u_2} {p : outParam (AProp)} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [self : NonUnitalContinuousFunctionalCalculus R p] (a : A) :
    p a∃ (φ : ContinuousMapZero ((quasispectrum R a)) R →⋆ₙₐ[R] A), ClosedEmbedding φ φ { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := } = a (∀ (f : ContinuousMapZero ((quasispectrum R a)) R), quasispectrum R (φ f) = Set.range f) ∀ (f : ContinuousMapZero ((quasispectrum R a)) R), p (φ f)

    A class guaranteeing that the non-unital continuous functional calculus is uniquely determined by the properties that it is a continuous non-unital star algebra homomorphism mapping the (restriction of) the identity to a. This is the necessary tool used to establish cfcₙHom_comp and the more common variant cfcₙ_comp.

    This class will have instances in each of the common cases , and ℝ≥0 as a consequence of the Stone-Weierstrass theorem.

    Instances
      theorem UniqueNonUnitalContinuousFunctionalCalculus.eq_of_continuous_of_map_id {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [self : UniqueNonUnitalContinuousFunctionalCalculus R A] (s : Set R) [CompactSpace s] [Zero s] (h0 : 0 = 0) (φ : ContinuousMapZero (s) R →⋆ₙₐ[R] A) (ψ : ContinuousMapZero (s) R →⋆ₙₐ[R] A) (hφ : Continuous φ) (hψ : Continuous ψ) (h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id R), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id R), map_zero' := h0 }) :
      φ = ψ
      theorem NonUnitalStarAlgHom.ext_continuousMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [UniqueNonUnitalContinuousFunctionalCalculus R A] (a : A) (φ : ContinuousMapZero ((quasispectrum R a)) R →⋆ₙₐ[R] A) (ψ : ContinuousMapZero ((quasispectrum R a)) R →⋆ₙₐ[R] A) (hφ : Continuous φ) (hψ : Continuous ψ) (h : φ { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := } = ψ { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := }) :
      φ = ψ
      noncomputable def cfcₙHom {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) :

      The non-unital star algebra homomorphism underlying a instance of the continuous functional calculus for non-unital algebras; a version for continuous functions on the quasispectrum.

      In this case, the user must supply the fact that a satisfies the predicate p.

      While NonUnitalContinuousFunctionalCalculus is stated in terms of these homomorphisms, in practice the user should instead prefer cfcₙ over cfcₙHom.

      Equations
      Instances For
        theorem cfcₙHom_id {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) :
        (cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := } = a

        The spectral mapping theorem for the non-unital continuous functional calculus.

        theorem cfcₙHom_predicate {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) (f : ContinuousMapZero ((quasispectrum R a)) R) :
        p ((cfcₙHom ha) f)
        theorem cfcₙHom_eq_of_continuous_of_map_id {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) [UniqueNonUnitalContinuousFunctionalCalculus R A] (φ : ContinuousMapZero ((quasispectrum R a)) R →⋆ₙₐ[R] A) (hφ₁ : Continuous φ) (hφ₂ : φ { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := } = a) :
        cfcₙHom ha = φ
        theorem cfcₙHom_comp {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) [UniqueNonUnitalContinuousFunctionalCalculus R A] (f : ContinuousMapZero ((quasispectrum R a)) R) (f' : ContinuousMapZero (quasispectrum R a) (quasispectrum R ((cfcₙHom ha) f))) (hff' : ∀ (x : (quasispectrum R a)), f x = (f' x)) (g : ContinuousMapZero ((quasispectrum R ((cfcₙHom ha) f))) R) :
        (cfcₙHom ha) (g.comp f') = (cfcₙHom ) g
        theorem cfcₙ_def {R : Type u_3} {A : Type u_4} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) :
        cfcₙ f a = if h : p a ContinuousOn f (quasispectrum R a) f 0 = 0 then (cfcₙHom ) { toFun := (quasispectrum R a).restrict f, continuous_toFun := , map_zero' := } else 0
        @[irreducible]
        noncomputable def cfcₙ {R : Type u_3} {A : Type u_4} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) :
        A

        This is the continuous functional calculus of an element a : A in a non-unital algebra 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 quasispectrum of a or f 0 ≠ 0, then cfcₙ f a returns the junk value 0.

        This is the primary declaration intended for widespread use of the continuous functional calculus for non-unital algebras, and all the API applies to this declaration. For more information, see the module documentation for Analysis.CstarAlgebra.ContinuousFunctionalCalculus.Unital.

        Equations
        Instances For
          theorem cfcₙ_apply {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ f a = (cfcₙHom ha) { toFun := (quasispectrum R a).restrict f, continuous_toFun := , map_zero' := hf0 }
          theorem cfcₙ_apply_pi {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {ι : Type u_3} (f : ιRR) (a : A) (ha : autoParam (p a) _auto✝) (hf : autoParam (∀ (i : ι), ContinuousOn (f i) (quasispectrum R a)) _auto✝) (hf0 : autoParam (∀ (i : ι), f i 0 = 0) _auto✝) :
          (fun (i : ι) => cfcₙ (f i) a) = fun (i : ι) => (cfcₙHom ha) { toFun := (quasispectrum R a).restrict (f i), continuous_toFun := , map_zero' := }
          theorem cfcₙ_apply_of_not_and_and {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} (a : A) (ha : ¬(p a ContinuousOn f (quasispectrum R a) f 0 = 0)) :
          cfcₙ f a = 0
          theorem cfcₙ_apply_of_not_predicate {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} (a : A) (ha : ¬p a) :
          cfcₙ f a = 0
          theorem cfcₙ_apply_of_not_map_zero {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} (a : A) (hf : ¬f 0 = 0) :
          cfcₙ f a = 0
          theorem cfcₙHom_eq_cfcₙ_extend {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (g : RR) (ha : p a) (f : ContinuousMapZero ((quasispectrum R a)) R) :
          (cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (f) g) a
          theorem cfcₙ_cases {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (P : AProp) (a : A) (f : RR) (h₀ : P 0) (haf : ∀ (hf : ContinuousOn f (quasispectrum R a)) (h0 : { toFun := (quasispectrum R a).restrict f, continuous_toFun := } 0 = 0) (ha : p a), P ((cfcₙHom ha) { toFun := (quasispectrum R a).restrict f, continuous_toFun := , map_zero' := h0 })) :
          P (cfcₙ f a)
          theorem cfcₙ_id' (R : Type u_1) {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => x) a = a

          The spectral mapping theorem for the non-unital continuous functional calculus.

          theorem cfcₙ_predicate {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) :
          p (cfcₙ f a)
          theorem cfcₙ_congr {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} {g : RR} {a : A} (hfg : Set.EqOn f g (quasispectrum R a)) :
          cfcₙ f a = cfcₙ g a
          theorem eqOn_of_cfcₙ_eq_cfcₙ {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} {g : RR} {a : A} (h : cfcₙ f a = cfcₙ g a) (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) :
          theorem cfcₙ_eq_cfcₙ_iff_eqOn {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} {g : RR} {a : A} (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) :
          @[simp]
          @[simp]
          theorem cfcₙ_const_zero (R : Type u_1) {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (a : A) :
          cfcₙ (fun (x : R) => 0) a = 0
          theorem cfcₙ_mul {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (g : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) :
          cfcₙ (fun (x : R) => f x * g x) a = cfcₙ f a * cfcₙ g a
          theorem cfcₙ_add {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (g : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) :
          cfcₙ (fun (x : R) => f x + g x) a = cfcₙ f a + cfcₙ g a
          theorem cfcₙ_sum {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {ι : Type u_3} (f : ιRR) (a : A) (s : Finset ι) (hf : autoParam (is, ContinuousOn (f i) (quasispectrum R a)) _auto✝) (hf0 : autoParam (is, f i 0 = 0) _auto✝) :
          cfcₙ (is, f i) a = is, cfcₙ (f i) a
          theorem cfcₙ_sum_univ {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {ι : Type u_3} [Fintype ι] (f : ιRR) (a : A) (hf : autoParam (∀ (i : ι), ContinuousOn (f i) (quasispectrum R a)) _auto✝) (hf0 : autoParam (∀ (i : ι), f i 0 = 0) _auto✝) :
          cfcₙ (i : ι, f i) a = i : ι, cfcₙ (f i) a
          theorem cfcₙ_smul {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {S : Type u_3} [SMulZeroClass S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (RR)] (s : S) (f : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) :
          cfcₙ (fun (x : R) => s f x) a = s cfcₙ f a
          theorem cfcₙ_const_mul {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (r : R) (f : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) :
          cfcₙ (fun (x : R) => r * f x) a = r cfcₙ f a
          theorem cfcₙ_star {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) :
          cfcₙ (fun (x : R) => star (f x)) a = star (cfcₙ f a)
          theorem cfcₙ_smul_id {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {S : Type u_3} [SMulZeroClass S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (RR)] (s : S) (a : A) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => s x) a = s a
          theorem cfcₙ_const_mul_id {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (r : R) (a : A) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => r * x) a = r a
          theorem cfcₙ_star_id {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => star x) a = star a
          theorem cfcₙ_comp {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (g : RR) (f : RR) (a : A) (hg : autoParam (ContinuousOn g (f '' quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ (g f) a = cfcₙ g (cfcₙ f a)
          theorem cfcₙ_comp' {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (g : RR) (f : RR) (a : A) (hg : autoParam (ContinuousOn g (f '' quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => g (f x)) a = cfcₙ g (cfcₙ f a)
          theorem cfcₙ_comp_smul {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] {S : Type u_3} [SMulZeroClass S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (RR)] (s : S) (f : RR) (a : A) (hf : autoParam (ContinuousOn f ((fun (x : R) => s x) '' quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => f (s x)) a = cfcₙ f (s a)
          theorem cfcₙ_comp_const_mul {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (r : R) (f : RR) (a : A) (hf : autoParam (ContinuousOn f ((fun (x : R) => r * x) '' quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => f (r * x)) a = cfcₙ f (r a)
          theorem cfcₙ_comp_star {R : Type u_1} {A : Type u_2} {p : AProp} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) [UniqueNonUnitalContinuousFunctionalCalculus R A] (hf : autoParam (ContinuousOn f (star '' quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => f (star x)) a = cfcₙ f (star a)
          @[simp]
          theorem cfcₙ_sub {R : Type u_1} {A : Type u_2} {p : AProp} [CommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (g : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) :
          cfcₙ (fun (x : R) => f x - g x) a = cfcₙ f a - cfcₙ g a
          theorem cfcₙ_neg {R : Type u_1} {A : Type u_2} {p : AProp} [CommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) :
          cfcₙ (fun (x : R) => -f x) a = -cfcₙ f a
          theorem cfcₙ_neg_id {R : Type u_1} {A : Type u_2} {p : AProp} [CommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => -x) a = -a
          theorem cfcₙ_comp_neg {R : Type u_1} {A : Type u_2} {p : AProp} [CommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) [UniqueNonUnitalContinuousFunctionalCalculus R A] (hf : autoParam (ContinuousOn f ((fun (x : R) => -x) '' quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ (fun (x : R) => f (-x)) a = cfcₙ f (-a)
          theorem cfcₙHom_mono {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) {f : ContinuousMapZero ((quasispectrum R a)) R} {g : ContinuousMapZero ((quasispectrum R a)) R} (hfg : f g) :
          (cfcₙHom ha) f (cfcₙHom ha) g
          theorem cfcₙHom_nonneg_iff {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : ContinuousMapZero ((quasispectrum R a)) R} :
          0 (cfcₙHom ha) f 0 f
          theorem cfcₙ_mono {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} {g : RR} {a : A} (h : xquasispectrum R a, f x g x) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) :
          cfcₙ f a cfcₙ g a
          theorem cfcₙ_nonneg_iff {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          0 cfcₙ f a xquasispectrum R a, 0 f x
          theorem cfcₙ_nonneg {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] {f : RR} {a : A} (h : xquasispectrum R a, 0 f x) :
          0 cfcₙ f a
          theorem cfcₙ_nonpos {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] (f : RR) (a : A) (h : xquasispectrum R a, f x 0) :
          cfcₙ f a 0
          theorem cfcₙHom_le_iff {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : ContinuousMapZero ((quasispectrum R a)) R} {g : ContinuousMapZero ((quasispectrum R a)) R} :
          (cfcₙHom ha) f (cfcₙHom ha) g f g
          theorem cfcₙ_le_iff {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : RR) (g : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (hg0 : autoParam (g 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ f a cfcₙ g a xquasispectrum R a, f x g x
          theorem cfcₙ_nonpos_iff {R : Type u_1} {A : Type u_2} {p : AProp} [OrderedCommRing R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing (ContinuousMapZero α R)] [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : RR) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) :
          cfcₙ f a 0 xquasispectrum R a, f x 0

          Obtain a non-unital continuous functional calculus from a unital one #

          noncomputable def cfcₙHom_of_cfcHom (R : Type u_1) {A : Type u_2} {p : AProp} [Field R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] {a : A} (ha : p a) :

          The non-unital continuous functional calculus obtained by restricting a unital calculus to functions that map zero to zero. This is an auxiliary definition and is not intended for use outside this file. The equality between the non-unital and unital calculi in this case is encoded in the lemma cfcₙ_eq_cfc.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem closedEmbedding_cfcₙHom_of_cfcHom {R : Type u_1} {A : Type u_2} {p : AProp} [Field R] [StarRing R] [MetricSpace R] [CompleteSpace R] [TopologicalRing R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [h_cpct : ∀ (a : A), CompactSpace (spectrum R a)] {a : A} (ha : p a) :
            theorem cfcₙ_eq_cfc {R : Type u_1} {A : Type u_2} {p : AProp} [Field R] [StarRing R] [MetricSpace R] [CompleteSpace R] [TopologicalRing R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [h_cpct : ∀ (a : A), CompactSpace (spectrum R a)] [UniqueNonUnitalContinuousFunctionalCalculus R A] {f : RR} {a : A} (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) :
            cfcₙ f a = cfc f a

            When cfc is applied to a function that maps zero to zero, it is equivalent to using cfcₙ.