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 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)) [Semifield 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) [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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ₙ_id (R : Type u_1) {A : Type u_2} {p : A → Prop} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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} [Semifield 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_3} {A : Type u_4} {p : A → Prop} [Field 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_3} {A : Type u_4} {p : A → Prop} [Field 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_3} {A : Type u_4} {p : A → Prop} [Field 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_3} {A : Type u_4} {p : A → Prop} [Field 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)