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

• NonUnitalContinuousFunctionalCalculus R (p : A → Prop): a class stating that every a : A satisfying p a has a non-unital star algebra homomorphism from the continuous R-valued functions on the R-quasispectrum of a vanishing at zero into the algebra A. This map is a closed embedding, and satisfies the spectral mapping theorem.
• cfcₙHom : p a → C(quasispectrum R a, R)₀ →⋆ₐ[R] A: the underlying non-unital star algebra homomorphism for an element satisfying property p.
• cfcₙ : (R → R) → A → A: an unbundled version of cfcₙHom which takes the junk value 0 when cfcₙHom is not defined.

Main theorems

• cfcₙ_comp : cfcₙ (x ↦ g (f x)) a = cfcₙ g (cfcₙ f a)

class NonUnitalContinuousFunctionalCalculus (R : Type u_1) {A : Type u_2} (p : outParam (A → Prop)) [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] : Prop

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.

• predicate_zero : p 0
• compactSpace_quasispectrum (a : A) : CompactSpace ↑(quasispectrum R a)
• exists_cfc_of_predicate (a : A) : p a → ∃ (φ : ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A), Topology.IsClosedEmbedding ⇑φ ∧ φ { 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)

class UniqueNonUnitalContinuousFunctionalCalculus (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] : Prop

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.

• eq_of_continuous_of_map_id (s : Set R) [CompactSpace ↑s] [Zero ↑s] (h0 : ↑0 = 0) (φ ψ : 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 }) : φ = ψ
• compactSpace_quasispectrum (a : A) : CompactSpace ↑(quasispectrum R a)

theorem NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) : IsCompact (quasispectrum R a)

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) (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] 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

• cfcₙHom ha = ⋯.choose

theorem cfcₙHom_isClosedEmbedding {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : Topology.IsClosedEmbedding ⇑(cfcₙHom ha)

@[deprecated cfcₙHom_isClosedEmbedding]

theorem cfcₙHom_closedEmbedding {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : Topology.IsClosedEmbedding ⇑(cfcₙHom ha)

Alias of cfcₙHom_isClosedEmbedding.

theorem cfcₙHom_continuous {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : Continuous ⇑(cfcₙHom ha)

theorem cfcₙHom_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : (cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := ⋯ } = a

theorem cfcₙHom_map_quasispectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) (f : ContinuousMapZero (↑(quasispectrum R a)) R) : quasispectrum R ((cfcₙHom ha) f) = Set.range ⇑f

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

theorem cfcₙHom_predicate {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : 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 : A → Prop} [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] [instCFCₙ : 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 : A → Prop} [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] [instCFCₙ : 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

noncomputable def cfcₙL {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : ContinuousMapZero (↑(quasispectrum R a)) R →L[R] A

cfcₙHom bundled as a continuous linear map.

Equations

• cfcₙL ha = { toFun := ⇑(cfcₙHom ha), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem cfcₙL_apply {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) (a✝ : ContinuousMapZero (↑(quasispectrum R a)) R) : (cfcₙL ha) a✝ = (cfcₙHom ha) a✝

theorem cfcₙ_def {R : Type u_3} {A : Type u_4} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (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

• 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

theorem cfcₙ_apply {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : 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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {ι : Type u_3} (f : ι → R → R) (a : A) (ha : p a := by cfc_tac) (hf : ∀ (i : ι), ContinuousOn (f i) (quasispectrum R a) := by cfc_cont_tac) (hf0 : ∀ (i : ι), f i 0 = 0 := by cfc_zero_tac) : (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f : R → R} (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f : R → R} (a : A) (ha : ¬p a) : cfcₙ f a = 0

theorem cfcₙ_apply_of_not_continuousOn {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f : R → R} (a : A) (hf : ¬ContinuousOn f (quasispectrum R a)) : cfcₙ f a = 0

theorem cfcₙ_apply_of_not_map_zero {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f : R → R} (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (g : R → R) (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (P : A → Prop) (a : A) (f : R → R) (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ₙ_commute_cfcₙ {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f g : R → R) (a : A) : Commute (cfcₙ f a) (cfcₙ g a)

theorem cfcₙ_id (R : Type u_1) {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : p a := by cfc_tac) : cfcₙ id a = a

theorem cfcₙ_id' (R : Type u_1) {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : p a := by cfc_tac) : cfcₙ (fun (x : R) => x) a = a

theorem cfcₙ_map_quasispectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : quasispectrum R (cfcₙ f a) = f '' quasispectrum R a

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

theorem cfcₙ_predicate_zero (R : Type u_1) {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] : p 0

theorem cfcₙ_predicate {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) : p (cfcₙ f a)

theorem cfcₙ_congr {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f g : R → R} {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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f g : R → R} {a : A} (h : cfcₙ f a = cfcₙ g a) (ha : p a := by cfc_tac) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : Set.EqOn f g (quasispectrum R a)

theorem cfcₙ_eq_cfcₙ_iff_eqOn {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f g : R → R} {a : A} (ha : p a := by cfc_tac) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : cfcₙ f a = cfcₙ g a ↔ Set.EqOn f g (quasispectrum R a)

@[simp]

theorem cfcₙ_zero (R : Type u_1) {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) : cfcₙ 0 a = 0

@[simp]

theorem cfcₙ_const_zero (R : Type u_1) {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) : cfcₙ (fun (x : R) => 0) a = 0

theorem cfcₙ_mul {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f g : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : 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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f g : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : 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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {ι : Type u_3} (f : ι → R → R) (a : A) (s : Finset ι) (hf : ∀ i ∈ s, ContinuousOn (f i) (quasispectrum R a) := by cfc_cont_tac) (hf0 : ∀ i ∈ s, f i 0 = 0 := by cfc_zero_tac) : cfcₙ (∑ i ∈ s, f i) a = ∑ i ∈ s, cfcₙ (f i) a

theorem cfcₙ_sum_univ {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {ι : Type u_3} [Fintype ι] (f : ι → R → R) (a : A) (hf : ∀ (i : ι), ContinuousOn (f i) (quasispectrum R a) := by cfc_cont_tac) (hf0 : ∀ (i : ι), f i 0 = 0 := by cfc_zero_tac) : cfcₙ (∑ i : ι, f i) a = ∑ i : ι, cfcₙ (f i) a

theorem cfcₙ_smul {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {S : Type u_3} [SMulZeroClass S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (h0 : f 0 = 0 := by cfc_zero_tac) : 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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (r : R) (f : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (h0 : f 0 = 0 := by cfc_zero_tac) : cfcₙ (fun (x : R) => r * f x) a = r • cfcₙ f a

theorem cfcₙ_star {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {S : Type u_3} [SMulZeroClass S R] [ContinuousConstSMul S R] [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (a : A) (ha : p a := by cfc_tac) : cfcₙ (fun (x : R) => s • x) a = s • a

theorem cfcₙ_const_mul_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (r : R) (a : A) (ha : p a := by cfc_tac) : cfcₙ (fun (x : R) => r * x) a = r • a

theorem cfcₙ_star_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : p a := by cfc_tac) : cfcₙ (fun (x : R) => star x) a = star a

theorem cfcₙ_comp {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (g f : R → R) (a : A) (hg : ContinuousOn g (f '' quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)

theorem cfcₙ_comp' {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (g f : R → R) (a : A) (hg : ContinuousOn g (f '' quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : 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 : A → Prop} [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] [instCFCₙ : 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 (R → R)] (s : S) (f : R → R) (a : A) (hf : ContinuousOn f ((fun (x : R) => s • x) '' quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : 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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (r : R) (f : R → R) (a : A) (hf : ContinuousOn f ((fun (x : R) => r * x) '' quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : 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 : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) [UniqueNonUnitalContinuousFunctionalCalculus R A] (hf : ContinuousOn f (star '' quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : cfcₙ (fun (x : R) => f (star x)) a = cfcₙ f (star a)

theorem CFC.eq_zero_of_quasispectrum_eq_zero {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (a : A) (h_spec : quasispectrum R a ⊆ {0}) (ha : p a := by cfc_tac) : a = 0

theorem CFC.quasispectrum_zero_eq {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] : quasispectrum R 0 = {0}

@[simp]

theorem cfcₙ_apply_zero {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {f : R → R} : cfcₙ f 0 = 0

@[simp]

instance IsStarNormal.cfcₙ_map {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) : IsStarNormal (cfcₙ f a)

@[simp]

theorem IsSelfAdjoint.cfcₙ {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] [NonUnitalContinuousFunctionalCalculus R IsSelfAdjoint] {f : R → R} {a : A} : IsSelfAdjoint (cfcₙ f a)

@[simp]

theorem cfcₙ_nonneg_of_predicate {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] [PartialOrder A] [NonUnitalContinuousFunctionalCalculus R fun (a : A) => 0 ≤ a] {f : R → R} {a : A} : 0 ≤ cfcₙ f a

theorem cfcₙ_sub {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 g : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : 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 : A → Prop} [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 : R → R) (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 : A → Prop} [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 : p a := by cfc_tac) : cfcₙ (fun (x : R) => -x) a = -a

theorem cfcₙ_comp_neg {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 : R → R) (a : A) [UniqueNonUnitalContinuousFunctionalCalculus R A] (hf : ContinuousOn f ((fun (x : R) => -x) '' quasispectrum R a) := by cfc_cont_tac) (h0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : cfcₙ (fun (x : R) => f (-x)) a = cfcₙ f (-a)

theorem cfcₙHom_mono {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 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 : A → Prop} [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 : A → Prop} [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 g : R → R} {a : A} (h : ∀ x ∈ quasispectrum R a, f x ≤ g x) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : cfcₙ f a ≤ cfcₙ g a

theorem cfcₙ_nonneg_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (h0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : 0 ≤ cfcₙ f a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ f x

theorem StarOrderedRing.nonneg_iff_quasispectrum_nonneg {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 := by cfc_tac) : 0 ≤ a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ x

theorem cfcₙ_nonneg {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 : R → R} {a : A} (h : ∀ x ∈ quasispectrum R a, 0 ≤ f x) : 0 ≤ cfcₙ f a

theorem cfcₙ_nonpos {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 : R → R) (a : A) (h : ∀ x ∈ quasispectrum R a, f x ≤ 0) : cfcₙ f a ≤ 0

theorem cfcₙHom_le_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 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 : A → Prop} [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 g : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hg : ContinuousOn g (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ quasispectrum R a, f x ≤ g x

theorem cfcₙ_nonpos_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [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 : R → R) (a : A) (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (h0 : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : cfcₙ f a ≤ 0 ↔ ∀ x ∈ quasispectrum R a, f x ≤ 0

cfcₙHom on a superset of the quasispectrum

noncomputable def cfcₙHomSuperset {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s) : ContinuousMapZero (↑s) R →⋆ₙₐ[R] A

The composition of cfcₙHom with the natural embedding C(s, R)₀ → C(quasispectrum R a, R)₀ whenever quasispectrum R a ⊆ s.

This is sometimes necessary in order to consider the same continuous functions applied to multiple distinct elements, with the added constraint that cfcₙ does not suffice. This can occur, for example, if it is necessary to use uniqueness of this continuous functional calculus. A practical example can be found in the proof of CFC.posPart_negPart_unique.

Equations

• cfcₙHomSuperset ha hs = (cfcₙHom ha).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R { toFun := Subtype.map id hs, continuous_toFun := ⋯, map_zero' := ⋯ })

@[simp]

theorem cfcₙHomSuperset_apply {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s) (a✝ : ContinuousMapZero (↑s) R) : (cfcₙHomSuperset ha hs) a✝ = (cfcₙHom ha) (a✝.comp { toFun := Subtype.map id hs, continuous_toFun := ⋯, map_zero' := ⋯ })

theorem cfcₙHomSuperset_continuous {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s) : Continuous ⇑(cfcₙHomSuperset ha hs)

theorem cfcₙHomSuperset_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s) : (cfcₙHomSuperset ha hs) { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id R), map_zero' := ⋯ } = a

theorem cfcₙHomSuperset_id' {R : Type u_1} {A : Type u_2} {p : A → Prop} [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] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s) : (cfcₙHomSuperset ha hs) (ContinuousMapZero.id ⋯) = a

this version uses ContinuousMapZero.id.

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 : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] 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

• cfcₙHom_of_cfcHom R ha = (↑(cfcHom ha)).comp ((↑(ContinuousMap.compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp ContinuousMapZero.toContinuousMapHom)

theorem cfcₙHom_of_cfcHom_map_quasispectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] {a : A} (ha : p a) (f : ContinuousMapZero (↑(quasispectrum R a)) R) : quasispectrum R ((cfcₙHom_of_cfcHom R ha) f) = Set.range ⇑f

theorem isClosedEmbedding_cfcₙHom_of_cfcHom {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [CompleteSpace R] {a : A} (ha : p a) : Topology.IsClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)

@[deprecated isClosedEmbedding_cfcₙHom_of_cfcHom]

theorem closedEmbedding_cfcₙHom_of_cfcHom {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [CompleteSpace R] {a : A} (ha : p a) : Topology.IsClosedEmbedding ⇑(cfcₙHom_of_cfcHom R ha)

Alias of isClosedEmbedding_cfcₙHom_of_cfcHom.

instance ContinuousFunctionalCalculus.toNonUnital {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [CompleteSpace R] : NonUnitalContinuousFunctionalCalculus R p

theorem cfcₙHom_eq_cfcₙHom_of_cfcHom {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [CompleteSpace R] [UniqueNonUnitalContinuousFunctionalCalculus R A] {a : A} (ha : p a) : cfcₙHom ha = cfcₙHom_of_cfcHom R ha

theorem cfcₙ_eq_cfc {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R p] [CompleteSpace R] [UniqueNonUnitalContinuousFunctionalCalculus R A] {f : R → R} {a : A} (hf : ContinuousOn f (quasispectrum R a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : cfcₙ f a = cfc f a

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