The continuous functional calculus

This file defines a generic API for the continuous functional calculus which is suitable in a wide range of settings.

A continuous functional calculus for an element a : A in a topological R-algebra is a continuous extension of the polynomial functional calculus (i.e., Polynomial.aeval) to continuous R-valued functions on spectrum R a. More precisely, it is a continuous star algebra homomorphism C(spectrum R a, R) →⋆ₐ[R] A that sends (ContinuousMap.id R).restrict (spectrum R a) to a. In all cases of interest (e.g., when spectrum R a is compact and R is ℝ≥0, ℝ, or ℂ), this is sufficient to uniquely determine the continuous functional calculus which is encoded in the UniqueContinuousFunctionalCalculus class.

Although these properties suffice to uniquely determine the continuous functional calculus, we choose to bundle more information into the class itself. Namely, we include that the star algebra homomorphism is a closed embedding, and also that the spectrum of the image of f : C(spectrum R a, R) under this morphism is the range of f. In addition, the class specifies a collection of continuous functional calculi for elements satisfying a given predicate p : A → Prop, and we require that this predicate is preserved by the functional calculus.

Although cfcHom : p a → C(spectrum R a, R) →*ₐ[R] A is a necessity for getting the full power out of the continuous functional calculus, this declaration will generally not be accessed directly by the user. One reason for this is that cfcHom requires a proof of p a (indeed, if the spectrum is empty, there cannot exist a star algebra homomorphism like this). Instead, we provide the completely unbundled cfc : (R → R) → A → A which operates on bare functions and provides junk values when either a does not satisfy the property p, or else when the function which is the argument to cfc is not continuous on the spectrum of a.

This completely unbundled approach may give up some conveniences, but it allows for tremendous freedom. In particular, cfc f a makes sense for any a : A and f : R → R. This is quite useful in a variety of settings, but perhaps the most important is the following. Besides being a star algebra homomorphism sending the identity to a, the key property enjoyed by the continuous functional calculus is the composition property, which guarantees that cfc (g ∘ f) a = cfc g (cfc f a) under suitable hypotheses on a, f and g. Note that this theorem is nearly impossible to state nicely in terms of cfcHom (see cfcHom_comp). An additional advantage of the unbundled approach is that expressions like fun x : R ↦ x⁻¹ are valid arguments to cfc, and a bundled continuous counterpart can only make sense when the spectrum of a does not contain zero and when we have an ⁻¹ operation on the domain.

A reader familiar with C⋆-algebra theory may be somewhat surprised at the level of abstraction here. For instance, why not require A to be an actual C⋆-algebra? Why define separate continuous functional calculi for R := ℂ, ℝ or ℝ≥0 instead of simply using the continuous functional calculus for normal elements? The reason for both can be explained with a simple example, A := Matrix n n ℝ. In Mathlib, matrices are not equipped with a norm (nor even a metric), and so requiring A to be a C⋆-algebra is far too stringent. Likewise, A is not a ℂ-algebra, and so it is impossible to consider the ℂ-spectrum of a : Matrix n n ℝ.

There is another, more practical reason to define separate continuous functional calculi for different scalar rings. It gives us the ability to use functions defined on these types, and the algebra of functions on them. For example, for R := ℝ it is quite natural to consider the functions (·⁺ : ℝ → ℝ) and (·⁻ : ℝ → ℝ) because the functions ℝ → ℝ form a lattice ordered group. If a : A is selfadjoint, and we define a⁺ := cfc (·⁺ : ℝ → ℝ) a, and likewise for a⁻, then the properties a⁺ * a⁻ = 0 = a⁻ * a⁺ and a = a⁺ - a⁻ are trivial consequences of the corresponding facts for functions. In contrast, if we had to do this using functions on ℂ, the proofs of these facts would be much more cumbersome.

Example

The canonical example of the continuous functional calculus is when A := Matrix n n ℂ, R := ℂ and p := IsStarNormal. In this case, spectrum ℂ a consists of the eigenvalues of the normal matrix a : Matrix n n ℂ, and, because this set is discrete, any function is continuous on the spectrum. The continuous functional calculus allows us to make sense of expressions like log a (:= cfc log a), and when 0 ∉ spectrum ℂ a, we get the nice property exp (log a) = a, which arises from the composition property cfc exp (cfc log a) = cfc (exp ∘ log) a = cfc id a = a, since exp ∘ log = id on the spectrum of a. Of course, there are other ways to make sense of exp and log for matrices (power series), and these agree with the continuous functional calculus. In fact, given f : C(spectrum ℂ a, ℂ), cfc f a amounts to diagonalizing a (possible since a is normal), and applying f to the resulting diagonal entries. That is, if a = u * d * star u with u a unitary matrix and d diagonal, then cfc f a = u * d.map f * star u.

In addition, if a : Matrix n n ℂ is positive semidefinite, then the ℂ-spectrum of a is contained in (the range of the coercion of) ℝ≥0. In this case, we get a continuous functional calculus with R := ℝ≥0. From this we can define √a := cfc a NNReal.sqrt, which is also positive semidefinite (because cfc preserves the predicate), and this is truly a square root since

√a * √a = cfc NNReal.sqrt a * cfc NNReal.sqrt a =
  cfc (NNReal.sqrt ^ 2) a = cfc id a = a

The composition property allows us to show that, in fact, this is the unique positive semidefinite square root of a because, if b is any positive semidefinite square root, then

b = cfc id b = cfc (NNReal.sqrt ∘ (· ^ 2)) b =
  cfc NNReal.sqrt (cfc b (· ^ 2)) = cfc NNReal.sqrt a = √a

Main declarations

• ContinuousFunctionalCalculus R (p : A → Prop): a class stating that every a : A satisfying p a has a star algebra homomorphism from the continuous R-valued functions on the R-spectrum of a into the algebra A. This map is a closed embedding, and satisfies the spectral mapping theorem.
• cfcHom : p a → C(spectrum R a, R) →⋆ₐ[R] A: the underlying star algebra homomorphism for an element satisfying property p.
• cfc : (R → R) → A → A: an unbundled version of cfcHom which takes the junk value 0 when cfcHom is not defined.
• cfcUnits: builds a unit from cfc f a when f is nonzero and continuous on the spectrum of a.

Main theorems

• cfc_comp : cfc (x ↦ g (f x)) a = cfc g (cfc f a)
• cfc_polynomial: the continuous functional calculus extends the polynomial functional calculus.

Implementation details

Instead of defining a class depending on a term a : A, we register it for an outParam predicate p : A → Prop, and then any element of A satisfying this predicate has the associated star algebra homomorphism with the specified properties. In so doing we avoid a common pitfall: dependence of the class on a term. This avoids annoying situations where a b : A are propositionally equal, but not definitionally so, and hence Lean would not be able to automatically identify the continuous functional calculi associated to these elements. In order to guarantee the necessary properties, we require that the continuous functional calculus preserves this predicate. That is, p a → p (cfc f a) for any function f continuous on the spectrum of a.

As stated above, the unbundled approach to cfc has its advantages. For instance, given an expression cfc f a, the user is free to rewrite either a or f as desired with no possibility of the expression ceasing to be defined. However, this unbundling also has some potential downsides. In particular, by unbundling, proof requirements are deferred until the user calls the lemmas, most of which have hypotheses both of p a and of ContinuousOn f (spectrum R a).

In order to minimize burden to the user, we provide autoParams in terms of two tactics. Goals related to continuity are dispatched by (a small wrapper around) fun_prop. As for goals involving the predicate p, it should be noted that these will only ever be of the form IsStarNormal a, IsSelfAdjoint a or 0 ≤ a. For the moment we provide a rudimentary tactic to deal with these goals, but it can be modified to become more sophisticated as the need arises.

class ContinuousFunctionalCalculus (R : Type u_1) {A : Type u_2} (p : outParam (A → Prop)) [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] : Prop

A 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 star algebra homomorphism cfcHom : C(spectrum R a, R) →⋆ₐ[R] A sending the (restriction of) the identity map to a.
• cfcHom is a closed embedding for which the spectrum of the image of function f is its range.
• cfcHom preserves the property p.
• p 0 is true, which ensures among other things that p ≠ fun _ ↦ False.

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_spectrum : ∀ (a : A), CompactSpace ↑(spectrum R a)
• spectrum_nonempty : ∀ [inst : Nontrivial A] (a : A), p a → (spectrum R a).Nonempty
• exists_cfc_of_predicate : ∀ (a : A), p a → ∃ (φ : C(↑(spectrum R a), R) →⋆ₐ[R] A), IsClosedEmbedding ⇑φ ∧ φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧ (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)

theorem ContinuousFunctionalCalculus.predicate_zero (R : Type u_1) {A : Type u_2} {p : outParam (A → Prop)} : ∀ {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R} {inst_3 : TopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R p], p 0

theorem ContinuousFunctionalCalculus.compactSpace_spectrum {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} : ∀ {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R} {inst_3 : TopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R p] (a : A), CompactSpace ↑(spectrum R a)

theorem ContinuousFunctionalCalculus.spectrum_nonempty {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} : ∀ {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R} {inst_3 : TopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R p] [inst_9 : Nontrivial A] (a : A), p a → (spectrum R a).Nonempty

theorem ContinuousFunctionalCalculus.exists_cfc_of_predicate {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} : ∀ {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R} {inst_3 : TopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R p] (a : A), p a → ∃ (φ : C(↑(spectrum R a), R) →⋆ₐ[R] A), IsClosedEmbedding ⇑φ ∧ φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧ (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)

class UniqueContinuousFunctionalCalculus (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] : Prop

A class guaranteeing that the continuous functional calculus is uniquely determined by the properties that it is a continuous star algebra homomorphism mapping the (restriction of) the identity to a. This is the necessary tool used to establish cfcHom_comp and the more common variant cfc_comp.

This class has instances, which can be found in Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique, in each of the common cases ℂ, ℝ and ℝ≥0 as a consequence of the Stone-Weierstrass theorem.

This class is separate from ContinuousFunctionalCalculus primarily because we will later use SpectrumRestricts to derive an instance of ContinuousFunctionalCalculus on a scalar subring from one on a larger ring (i.e., to go from a continuous functional calculus over ℂ for normal elements to one over ℝ for selfadjoint elements), and proving this additional property is preserved would be burdensome or impossible.

• eq_of_continuous_of_map_id : ∀ (s : Set R) [inst : CompactSpace ↑s] (φ ψ : C(↑s, R) →⋆ₐ[R] A), Continuous ⇑φ → Continuous ⇑ψ → φ (ContinuousMap.restrict s (ContinuousMap.id R)) = ψ (ContinuousMap.restrict s (ContinuousMap.id R)) → φ = ψ
• compactSpace_spectrum : ∀ (a : A), CompactSpace ↑(spectrum R a)

theorem UniqueContinuousFunctionalCalculus.eq_of_continuous_of_map_id {R : Type u_1} {A : Type u_2} : ∀ {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R} {inst_3 : TopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : UniqueContinuousFunctionalCalculus R A] (s : Set R) [inst_9 : CompactSpace ↑s] (φ ψ : C(↑s, R) →⋆ₐ[R] A), Continuous ⇑φ → Continuous ⇑ψ → φ (ContinuousMap.restrict s (ContinuousMap.id R)) = ψ (ContinuousMap.restrict s (ContinuousMap.id R)) → φ = ψ

theorem UniqueContinuousFunctionalCalculus.compactSpace_spectrum {R : Type u_1} {A : Type u_2} : ∀ {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : MetricSpace R} {inst_3 : TopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A} {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : UniqueContinuousFunctionalCalculus R A] (a : A), CompactSpace ↑(spectrum R a)

theorem ContinuousFunctionalCalculus.isCompact_spectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) : IsCompact (spectrum R a)

theorem StarAlgHom.ext_continuousMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [UniqueContinuousFunctionalCalculus R A] (a : A) (φ : C(↑(spectrum R a), R) →⋆ₐ[R] A) (ψ : C(↑(spectrum R a), R) →⋆ₐ[R] A) (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = ψ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))) : φ = ψ

noncomputable def cfcHom {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : C(↑(spectrum R a), R) →⋆ₐ[R] A

The star algebra homomorphism underlying a instance of the continuous functional calculus; a version for continuous functions on the spectrum.

In this case, the user must supply the fact that a satisfies the predicate p, for otherwise it may be the case that no star algebra homomorphism exists. For instance if R := ℝ and a is an element whose spectrum (in ℂ) is disjoint from ℝ, then spectrum ℝ a = ∅ and so there can be no star algebra homomorphism between these spaces.

While ContinuousFunctionalCalculus is stated in terms of these homomorphisms, in practice the user should instead prefer cfc over cfcHom.

Equations

• cfcHom ha = ⋯.choose

theorem cfcHom_isClosedEmbedding {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : IsClosedEmbedding ⇑(cfcHom ha)

@[deprecated cfcHom_isClosedEmbedding]

theorem cfcHom_closedEmbedding {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : IsClosedEmbedding ⇑(cfcHom ha)

Alias of cfcHom_isClosedEmbedding.

theorem cfcHom_continuous {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : Continuous ⇑(cfcHom ha)

theorem cfcHom_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : (cfcHom ha) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a

theorem cfcHom_map_spectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) (f : C(↑(spectrum R a), R)) : spectrum R ((cfcHom ha) f) = Set.range ⇑f

The spectral mapping theorem for the continuous functional calculus.

theorem cfcHom_predicate {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) (f : C(↑(spectrum R a), R)) : p ((cfcHom ha) f)

theorem cfcHom_eq_of_continuous_of_map_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) [UniqueContinuousFunctionalCalculus R A] (φ : C(↑(spectrum R a), R) →⋆ₐ[R] A) (hφ₁ : Continuous ⇑φ) (hφ₂ : φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a) : cfcHom ha = φ

theorem cfcHom_comp {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) [UniqueContinuousFunctionalCalculus R A] (f : C(↑(spectrum R a), R)) (f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))) (hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)) (g : C(↑(spectrum R ((cfcHom ha) f)), R)) : (cfcHom ha) (g.comp f') = (cfcHom ⋯) g

noncomputable def cfcL {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) : C(↑(spectrum R a), R) →L[R] A

cfcHom bundled as a continuous linear map.

Equations

• cfcL ha = { toFun := ⇑(cfcHom ha), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem cfcL_apply {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a✝) (a : C(↑(spectrum R a✝), R)) : (cfcL ha) a = (cfcHom ha) a

@[irreducible]

noncomputable def cfc {R : Type u_3} {A : Type u_4} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) : A

This is the continuous functional calculus of an element a : A applied to bare functions. When either a does not satisfy the predicate p (i.e., a is not IsStarNormal, IsSelfAdjoint, or 0 ≤ a when R is ℂ, ℝ, or ℝ≥0, respectively), or when f : R → R is not continuous on the spectrum of a, then cfc f a returns the junk value 0.

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

Equations

• @cfc = wrapped✝.1

theorem cfc_def {R : Type u_3} {A : Type u_4} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) : cfc f a = if h : p a ∧ ContinuousOn f (spectrum R a) then (cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } else 0

theorem cfc_apply {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) : cfc f a = (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

theorem cfc_apply_pi {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {ι : Type u_3} (f : ι → R → R) (a : A) (ha : autoParam (p a) _auto✝) (hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) _auto✝) : (fun (i : ι) => cfc (f i) a) = fun (i : ι) => (cfcHom ha) { toFun := (spectrum R a).restrict (f i), continuous_toFun := ⋯ }

theorem cfc_apply_of_not_and {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} (a : A) (ha : ¬(p a ∧ ContinuousOn f (spectrum R a))) : cfc f a = 0

theorem cfc_apply_of_not_predicate {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} (a : A) (hf : ¬ContinuousOn f (spectrum R a)) : cfc f a = 0

theorem cfcHom_eq_cfc_extend {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (g : R → R) (ha : p a) (f : C(↑(spectrum R a), R)) : (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

theorem cfc_eq_cfcL {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} {f : R → R} (ha : p a) (hf : ContinuousOn f (spectrum R a)) : cfc f a = (cfcL ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

theorem cfc_cases {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0) (haf : ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a), P ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })) : P (cfc f a)

theorem cfc_commute_cfc {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => x) a = a

theorem cfc_map_spectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) : spectrum R (cfc f a) = f '' spectrum R a

The spectral mapping theorem for the continuous functional calculus.

theorem cfc_const {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => r) a = (algebraMap R A) r

theorem cfc_predicate_zero (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] : p 0

theorem cfc_predicate {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) : p (cfc f a)

theorem cfc_predicate_algebraMap {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) : p ((algebraMap R A) r)

theorem cfc_predicate_one (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] : p 1

theorem cfc_congr {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} {g : R → R} {a : A} (hfg : Set.EqOn f g (spectrum 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} {g : R → R} {a : A} (h : cfc f a = cfc g a) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : Set.EqOn f g (spectrum R a)

theorem cfc_eq_cfc_iff_eqOn {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} {g : R → R} {a : A} (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) : cfc f a = cfc g a ↔ Set.EqOn f g (spectrum R a)

theorem cfc_one (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : cfc 1 a = 1

theorem cfc_const_one (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => 1) a = 1

@[simp]

theorem cfc_zero (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (g : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) : cfc (fun (x : R) => f x * g x) a = cfc f a * cfc g a

theorem cfc_pow {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (n : ℕ) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f x ^ n) a = cfc f a ^ n

theorem cfc_add {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (f : R → R) (g : R → R) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) : cfc (fun (x : R) => f x + g x) a = cfc f a + cfc g a

theorem cfc_const_add {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => r + f x) a = (algebraMap R A) r + cfc f a

theorem cfc_add_const {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f x + r) a = cfc f a + (algebraMap R A) r

theorem cfc_sum {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {ι : Type u_3} (f : ι → R → R) (a : A) (s : Finset ι) (hf : autoParam (∀ i ∈ s, ContinuousOn (f i) (spectrum R a)) _auto✝) : 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {ι : Type u_3} [Fintype ι] (f : ι → R → R) (a : A) (hf : autoParam (∀ (i : ι), ContinuousOn (f i) (spectrum R a)) _auto✝) : 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {S : Type u_3} [SMul 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 (spectrum R a)) _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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) : cfc (fun (x : R) => star (f x)) a = star (cfc f a)

theorem cfc_pow_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (n : ℕ) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => x ^ n) a = a ^ n

theorem cfc_smul_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {S : Type u_3} [SMul 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => star x) a = star a

theorem cfc_eval_X {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (a : R) => Polynomial.eval a Polynomial.X) a = a

theorem cfc_eval_C {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (a : R) => Polynomial.eval a (Polynomial.C r)) a = (algebraMap R A) r

theorem cfc_map_polynomial {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (q : Polynomial R) (f : R → R) (a : A) (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) : cfc (fun (x : R) => Polynomial.eval (f x) q) a = (Polynomial.aeval (cfc f a)) q

theorem cfc_polynomial {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (q : Polynomial R) (a : A) (ha : autoParam (p a) _auto✝) : cfc (fun (a : R) => Polynomial.eval a q) a = (Polynomial.aeval a) q

theorem cfc_comp {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (g : R → R) (f : R → R) (a : A) (ha : autoParam (p a) _auto✝) (hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (g : R → R) (f : R → R) (a : A) (hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => g (f x)) a = cfc g (cfc f a)

theorem cfc_comp_pow {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (f : R → R) (n : ℕ) (a : A) (hf : autoParam (ContinuousOn f ((fun (x : R) => x ^ n) '' spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f (x ^ n)) a = cfc f (a ^ n)

theorem cfc_comp_smul {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] {S : Type u_3} [SMul 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) '' spectrum R a)) _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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (r : R) (f : R → R) (a : A) (hf : autoParam (ContinuousOn f ((fun (x : R) => r * x) '' spectrum R a)) _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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (star '' spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f (star x)) a = cfc f (star a)

theorem cfc_comp_polynomial {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] (q : Polynomial R) (f : R → R) (a : A) (hf : autoParam (ContinuousOn f ((fun (a : R) => Polynomial.eval a q) '' spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f (Polynomial.eval x q)) a = cfc f ((Polynomial.aeval a) q)

theorem CFC.eq_algebraMap_of_spectrum_subset_singleton {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (r : R) (h_spec : spectrum R a ⊆ {r}) (ha : autoParam (p a) _auto✝) : a = (algebraMap R A) r

theorem CFC.eq_zero_of_spectrum_subset_zero {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (h_spec : spectrum R a ⊆ {0}) (ha : autoParam (p a) _auto✝) : a = 0

theorem CFC.eq_one_of_spectrum_subset_one {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (a : A) (h_spec : spectrum R a ⊆ {1}) (ha : autoParam (p a) _auto✝) : a = 1

theorem CFC.spectrum_algebraMap_subset {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) : spectrum R ((algebraMap R A) r) ⊆ {r}

theorem CFC.spectrum_algebraMap_eq {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [Nontrivial A] (r : R) : spectrum R ((algebraMap R A) r) = {r}

theorem CFC.spectrum_zero_eq {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [Nontrivial A] : spectrum R 0 = {0}

theorem CFC.spectrum_one_eq {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [Nontrivial A] : spectrum R 1 = {1}

@[simp]

theorem cfc_algebraMap {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (r : R) (f : R → R) : cfc f ((algebraMap R A) r) = (algebraMap R A) (f r)

@[simp]

theorem cfc_apply_zero {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} : cfc f 0 = (algebraMap R A) (f 0)

@[simp]

theorem cfc_apply_one {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} : cfc f 1 = (algebraMap R A) (f 1)

@[simp]

instance IsStarNormal.cfc_map {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) : IsStarNormal (cfc f a)

Equations

• ⋯ = ⋯

@[simp]

theorem IsSelfAdjoint.cfc {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [PartialOrder A] [ContinuousFunctionalCalculus R fun (a : A) => 0 ≤ a] {f : R → R} {a : A} : 0 ≤ cfc f a

theorem CFC.spectrum_nonempty (R : Type u_1) {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [Nontrivial A] (a : A) (ha : autoParam (p a) _auto✝) : (spectrum R a).Nonempty

In an R-algebra with a continuous functional calculus, every element satisfying the predicate has nonempty R-spectrum.

theorem isUnit_cfc_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0

theorem isUnit_cfc {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : (∀ x ∈ spectrum R a, f x ≠ 0) → IsUnit (cfc f a)

Alias of the reverse direction of isUnit_cfc_iff.

noncomputable def cfcUnits {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : Aˣ

Bundle cfc f a into a unit given a proof that f is nonzero on the spectrum of a.

Equations

• cfcUnits f a hf' hf ha = { val := cfc f a, inv := cfc (fun (x : R) => (f x)⁻¹) a, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem val_cfcUnits {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : ↑(cfcUnits f a hf' hf ha) = cfc f a

@[simp]

theorem val_inv_cfcUnits {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : ↑(cfcUnits f a hf' hf ha)⁻¹ = cfc (fun (x : R) => (f x)⁻¹) a

theorem cfcUnits_pow {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℕ) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfcUnits f a hf' hf ha ^ n = cfcUnits (fun (x : R) => f x ^ n) a ⋯ ⋯ ha

theorem cfc_inv {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => (f x)⁻¹) a = Ring.inverse (cfc f a)

theorem cfc_inv_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (a : Aˣ) (ha : autoParam (p ↑a) _auto✝) : cfc (fun (x : R) => x⁻¹) ↑a = ↑a⁻¹

theorem cfc_map_div {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (g : R → R) (a : A) (hg' : ∀ x ∈ spectrum R a, g x ≠ 0) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f x / g x) a = cfc f a * Ring.inverse (cfc g a)

theorem Units.continuousOn_inv₀_spectrum {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [TopologicalSpace R] [HasContinuousInv₀ R] [Algebra R A] (a : Aˣ) : ContinuousOn (fun (x : R) => x⁻¹) (spectrum R ↑a)

theorem Units.continuousOn_zpow₀_spectrum {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [TopologicalSpace R] [HasContinuousInv₀ R] [Algebra R A] [ContinuousMul R] (a : Aˣ) (n : ℤ) : ContinuousOn (fun (x : R) => x ^ n) (spectrum R ↑a)

theorem cfcUnits_zpow {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℤ) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfcUnits f a hf' hf ha ^ n = cfcUnits (f ^ n) a ⋯ ⋯ ha

theorem cfc_zpow {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] (a : Aˣ) (n : ℤ) (ha : autoParam (p ↑a) _auto✝) : cfc (fun (x : R) => x ^ n) ↑a = ↑(a ^ n)

theorem cfc_comp_inv {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] [UniqueContinuousFunctionalCalculus R A] (f : R → R) (a : Aˣ) (hf : autoParam (ContinuousOn f ((fun (x : R) => x⁻¹) '' spectrum R ↑a)) _auto✝) (ha : autoParam (p ↑a) _auto✝) : cfc (fun (x : R) => f x⁻¹) ↑a = cfc f ↑a⁻¹

theorem cfc_comp_zpow {R : Type u_1} {A : Type u_2} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] [HasContinuousInv₀ R] [UniqueContinuousFunctionalCalculus R A] (f : R → R) (n : ℤ) (a : Aˣ) (hf : autoParam (ContinuousOn f ((fun (x : R) => x ^ n) '' spectrum R ↑a)) _auto✝) (ha : autoParam (p ↑a) _auto✝) : cfc (fun (x : R) => f (x ^ n)) ↑a = cfc f ↑(a ^ n)

theorem cfc_sub {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] (f : R → R) (g : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _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] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus 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] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] (f : R → R) (a : A) [UniqueContinuousFunctionalCalculus R A] (hf : autoParam (ContinuousOn f ((fun (x : R) => -x) '' spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc (fun (x : R) => f (-x)) a = cfc f (-a)

theorem cfcHom_mono {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) {f : C(↑(spectrum R a), R)} {g : C(↑(spectrum R a), R)} (hfg : f ≤ g) : (cfcHom ha) f ≤ (cfcHom ha) g

theorem cfcHom_nonneg_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(↑(spectrum R a), R)} : 0 ≤ (cfcHom ha) f ↔ 0 ≤ f

theorem cfc_mono {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} {g : R → R} {a : A} (h : ∀ x ∈ spectrum R a, f x ≤ g x) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) : cfc f a ≤ cfc g a

theorem cfc_nonneg_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : 0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x

theorem StarOrderedRing.nonneg_iff_spectrum_nonneg {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (a : A) (ha : autoParam (p a) _auto✝) : 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x

theorem cfc_nonneg {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {f : R → R} {a : A} (h : ∀ x ∈ spectrum 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] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ 0) : cfc f a ≤ 0

theorem cfc_le_algebraMap {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (r : R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ r) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc f a ≤ (algebraMap R A) r

theorem algebraMap_le_cfc {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (r : R) (a : A) (h : ∀ x ∈ spectrum R a, r ≤ f x) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : (algebraMap R A) r ≤ cfc f a

theorem le_algebraMap_of_spectrum_le {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {r : R} {a : A} (h : ∀ x ∈ spectrum R a, x ≤ r) (ha : autoParam (p a) _auto✝) : a ≤ (algebraMap R A) r

theorem algebraMap_le_of_le_spectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {r : R} {a : A} (h : ∀ x ∈ spectrum R a, r ≤ x) (ha : autoParam (p a) _auto✝) : (algebraMap R A) r ≤ a

theorem cfc_le_one {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, f x ≤ 1) : cfc f a ≤ 1

theorem one_le_cfc {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] (f : R → R) (a : A) (h : ∀ x ∈ spectrum R a, 1 ≤ f x) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : 1 ≤ cfc f a

theorem CFC.le_one {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (h : ∀ x ∈ spectrum R a, x ≤ 1) (ha : autoParam (p a) _auto✝) : a ≤ 1

theorem CFC.one_le {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (h : ∀ x ∈ spectrum R a, 1 ≤ x) (ha : autoParam (p a) _auto✝) : 1 ≤ a

theorem CFC.inv_nonneg_of_nonneg {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [Algebra NNReal A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : Aˣ) (ha : autoParam (0 ≤ ↑a) _auto✝) : 0 ≤ ↑a⁻¹

theorem CFC.inv_nonneg {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [Algebra NNReal A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : Aˣ) : 0 ≤ ↑a⁻¹ ↔ 0 ≤ ↑a

theorem cfcHom_le_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(↑(spectrum R a), R)} {g : C(↑(spectrum R a), R)} : (cfcHom ha) f ≤ (cfcHom ha) g ↔ f ≤ g

theorem cfc_le_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (g : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x

theorem cfc_nonpos_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0

theorem cfc_le_algebraMap_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (r : R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc f a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, f x ≤ r

theorem algebraMap_le_cfc_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (r : R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : (algebraMap R A) r ≤ cfc f a ↔ ∀ x ∈ spectrum R a, r ≤ f x

theorem le_algebraMap_iff_spectrum_le {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] {r : R} {a : A} (ha : autoParam (p a) _auto✝) : a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r

theorem algebraMap_le_iff_le_spectrum {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] {r : R} {a : A} (ha : autoParam (p a) _auto✝) : (algebraMap R A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x

theorem cfc_le_one_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : cfc f a ≤ 1 ↔ ∀ x ∈ spectrum R a, f x ≤ 1

theorem one_le_cfc_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (f : R → R) (a : A) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) (ha : autoParam (p a) _auto✝) : 1 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 1 ≤ f x

theorem CFC.le_one_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (a : A) (ha : autoParam (p a) _auto✝) : a ≤ 1 ↔ ∀ x ∈ spectrum R a, x ≤ 1

theorem CFC.one_le_iff {R : Type u_1} {A : Type u_2} {p : A → Prop} [OrderedCommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)] [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] [NonnegSpectrumClass R A] (a : A) (ha : autoParam (p a) _auto✝) : 1 ≤ a ↔ ∀ x ∈ spectrum R a, 1 ≤ x

cfcHom on a superset of the spectrum

noncomputable def cfcHomSuperset {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : C(↑s, R) →⋆ₐ[R] A

The composition of cfcHom with the natural embedding C(s, R) → C(spectrum R a, R) whenever spectrum 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.

Equations

• cfcHomSuperset ha hs = (cfcHom ha).comp (ContinuousMap.compStarAlgHom' R R { toFun := Subtype.map id hs, continuous_toFun := ⋯ })

@[simp]

theorem cfcHomSuperset_apply {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : ∀ (a_1 : C(↑s, R)), (cfcHomSuperset ha hs) a_1 = (cfcHom ha) (a_1.comp { toFun := Subtype.map id hs, continuous_toFun := ⋯ })

theorem cfcHomSuperset_continuous {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : Continuous ⇑(cfcHomSuperset ha hs)

theorem cfcHomSuperset_id {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) : (cfcHomSuperset ha hs) (ContinuousMap.restrict s (ContinuousMap.id R)) = a