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.Topology.ContinuousFunction.FunctionalCalculus. 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.

• exists_cfc_of_predicate : ∀ (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)

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) [inst : CompactSpace ↑s] [inst : Zero ↑s] (h0 : ↑0 = 0) (φ ψ : ContinuousMapZero (↑s) R →⋆ₙₐ[R] A), Continuous ⇑φ → Continuous ⇑ψ → φ { 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 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 : 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] [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 = Exists.choose ⋯

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] [NonUnitalContinuousFunctionalCalculus R p] {a : A} (ha : p a) : ClosedEmbedding ⇑(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] [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] [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] [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] [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] [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) (ContinuousMapZero.comp g f') = (cfcₙHom ⋯) g

@[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] [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 Topology.ContinuousFunction.FunctionalCalculus.

Equations

• @cfcₙ = wrapped✝.1

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] [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 ⋯) { toContinuousMap := { toFun := Set.restrict (quasispectrum R a) f, continuous_toFun := ⋯ }, map_zero' := ⋯ } else 0

def cfcZeroTac : Lean.ParserDescr

A tactic used to automatically discharge goals relating to the continuous functional calculus, specifically concerning whether f 0 = 0.

Equations

• cfcZeroTac = Lean.ParserDescr.node `cfcZeroTac 1024 (Lean.ParserDescr.nonReservedSymbol "cfc_zero_tac" false)

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] [NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (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) { toContinuousMap := { toFun := Set.restrict (quasispectrum R a) f, continuous_toFun := ⋯ }, map_zero' := hf0 }

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] [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] [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] [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] [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] [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] [NonUnitalContinuousFunctionalCalculus R p] (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0) (haf : ∀ (hf : ContinuousOn f (quasispectrum R a)) (h0 : { toFun := Set.restrict (quasispectrum R a) f, continuous_toFun := ⋯ } 0 = 0) (ha : p a), P ((cfcₙHom ha) { toContinuousMap := { toFun := Set.restrict (quasispectrum R a) f, continuous_toFun := ⋯ }, map_zero' := h0 })) : P (cfcₙ f 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] [NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : 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] [NonUnitalContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : 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] [NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) : quasispectrum R (cfcₙ f a) = f '' quasispectrum R a

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

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] [NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (hf0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) : 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] [NonUnitalContinuousFunctionalCalculus R p] {f : R → R} {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] [NonUnitalContinuousFunctionalCalculus R p] {f : R → R} {g : R → R} {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✝) : 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] [NonUnitalContinuousFunctionalCalculus R p] {f : R → R} {g : R → R} {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✝) : 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] [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] [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] [NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (g : R → R) (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 : 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] [NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (g : R → R) (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ₙ_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] [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 : 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 : 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] [NonUnitalContinuousFunctionalCalculus R p] (r : R) (f : R → R) (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 : 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] [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] [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 : 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 : 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] [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 : 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] [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 : 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] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (g : R → R) (f : R → R) (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 : 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] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (g : R → R) (f : R → R) (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 : 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] [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 : 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 : 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] [NonUnitalContinuousFunctionalCalculus R p] [UniqueNonUnitalContinuousFunctionalCalculus R A] (r : R) (f : R → R) (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 : 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] [NonUnitalContinuousFunctionalCalculus R p] (f : R → R) (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)

theorem 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] [NonUnitalContinuousFunctionalCalculus R p] (a : A) (h_spec : quasispectrum R a ⊆ {0}) (ha : autoParam (p a) _auto✝) : a = 0

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 : R → R) (g : R → R) (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 : 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 : autoParam (p a) _auto✝) : 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 : 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 : 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 : 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 : 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 : R → R} {g : R → R} {a : A} (h : ∀ x ∈ quasispectrum 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 : 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 : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) : 0 ≤ cfcₙ f a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ f 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 : 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 : 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) (g : R → R) (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 ↔ ∀ 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 : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝) (h0 : autoParam (f 0 = 0) _auto✝) (ha : autoParam (p a) _auto✝) : cfcₙ f a ≤ 0 ↔ ∀ x ∈ quasispectrum R a, f x ≤ 0