# Instances of the continuous functional calculus #

## Main theorems #

- `IsSelfAdjoint.instContinuousFunctionalCalculus`: the continuous functional calculus for selfadjoint elements in a `ℂ`-algebra with a continuous functional calculus for normal elements and where every element has compact spectrum. In particular, this includes unital C⋆-algebras over `ℂ`.
- `Nonneg.instContinuousFunctionalCalculus`: the continuous functional calculus for nonnegative elements in an `ℝ`-algebra with a continuous functional calculus for selfadjoint elements, where every element has compact spectrum, and where nonnegative elements have nonnegative spectrum. In particular, this includes unital C⋆-algebras over `ℝ`.

## Tags #

continuous functional calculus, normal, selfadjoint

### Pull back a non-unital instance from a unital one on the unitization #

source
noncomputable def cfcₙAux {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] :
ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜 →⋆ₙₐ[𝕜] Unitization 𝕜 A

This is an auxiliary definition used for constructing an instance of the non-unital continuous functional calculus given a instance of the unital one on the unitization.

This is the natural non-unital star homomorphism obtained from the chain

    calc
      C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] C(σₙ 𝕜 a, 𝕜) := ContinuousMapZero.toContinuousMapHom
      _             ≃⋆[𝕜] C(σ 𝕜 (↑a : A⁺¹), 𝕜) := Homeomorph.compStarAlgEquiv'
      _             →⋆ₐ[𝕜] A⁺¹ := cfcHom

This range of this map is contained in the range of `(↑) : A → A⁺¹` (see `cfcₙAux_mem_range_inr`), and so we may restrict it to `A` to get the necessary homomorphism for the non-unital continuous functional calculus.

Equations

- cfcₙAux hp₁ a ha = ((↑(cfcHom ⋯)).comp ↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))).comp ContinuousMapZero.toContinuousMapHom

Instances For

source
theorem cfcₙAux_id {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] :
(cfcₙAux ⋯ a ha) (ContinuousMapZero.id (quasispectrum 𝕜 a)) = ↑a
source
theorem isClosedEmbedding_cfcₙAux {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] :
Topology.IsClosedEmbedding ⇑(cfcₙAux ⋯ a ha)
source
theorem spec_cfcₙAux {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) :
spectrum 𝕜 ((cfcₙAux ⋯ a ha) f) = Set.range ⇑f
source
theorem cfcₙAux_mem_range_inr {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a) [ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] [CompleteSpace A] (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) :
(cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)
source
theorem RCLike.nonUnitalContinuousFunctionalCalculus {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [StarModule 𝕜 A] {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) [ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁] [CompleteSpace A] [CStarRing A] :
NonUnitalContinuousFunctionalCalculus 𝕜 A p

### Continuous functional calculus for selfadjoint elements #

source
theorem isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} :
IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM

An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its quasispectrum is contained in `ℝ`.

source
theorem IsSelfAdjoint.quasispectrumRestricts {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} (ha : IsSelfAdjoint a) :
QuasispectrumRestricts a ⇑Complex.reCLM
source
@[deprecated isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts (since := "2025-09-16")]
theorem isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} :
IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM

Alias of `isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts`.

An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its quasispectrum is contained in `ℝ`.

source
theorem QuasispectrumRestricts.isSelfAdjoint {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : QuasispectrumRestricts a ⇑Complex.reCLM) [IsStarNormal a] :
IsSelfAdjoint a

A normal element whose `ℂ`-quasispectrum is contained in `ℝ` is selfadjoint.

source
@[deprecated QuasispectrumRestricts.isSelfAdjoint (since := "2025-09-16")]
theorem SpectrumRestricts.isSelfAdjoint {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A) (ha : QuasispectrumRestricts a ⇑Complex.reCLM) [IsStarNormal a] :
IsSelfAdjoint a

Alias of `QuasispectrumRestricts.isSelfAdjoint`.

A normal element whose `ℂ`-quasispectrum is contained in `ℝ` is selfadjoint.

source
instance IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] :
NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
source
theorem IsSelfAdjoint.spectrumRestricts {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} (ha : IsSelfAdjoint a) :
SpectrumRestricts a ⇑Complex.reCLM
source
instance IsSelfAdjoint.instContinuousFunctionalCalculus {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] :
ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
source
theorem IsSelfAdjoint.spectrum_nonempty {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [Nontrivial A] {a : A} (ha : IsSelfAdjoint a) :
(spectrum ℝ a).Nonempty

### Continuous functional calculus for nonnegative elements #

source
theorem CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha₁ : IsSelfAdjoint a) (ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) :
∃ (x : A), IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a
source
@[deprecated CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts (since := "2025-09-16")]
theorem CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts {A : Type u_1} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha₁ : IsSelfAdjoint a) (ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) :
∃ (x : A), IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a

Alias of `CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts`.

source
theorem nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts {A : Type u_1} [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} :
0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
source
@[deprecated nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts (since := "2025-09-16")]
theorem nonneg_iff_isSelfAdjoint_and_spectrumRestricts {A : Type u_1} [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} :
0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal

Alias of `nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts`.

source
instance Nonneg.instNonUnitalContinuousFunctionalCalculus {A : Type u_1} [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] :
NonUnitalContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x
source
theorem Commute.mul_nonneg {A : Type u_1} [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : Commute a b) :
0 ≤ a * b

In a C⋆-algebra, commuting nonnegative elements have nonnegative products.

source
theorem commute_iff_mul_nonneg {A : Type u_1} [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a b : A} (ha : 0 ≤ a) (hb : 0 ≤ b) :
Commute a b ↔ 0 ≤ a * b
source
theorem NNReal.spectrum_nonempty {A : Type u_2} [Ring A] [StarRing A] [LE A] [TopologicalSpace A] [Algebra NNReal A] [ContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x] [Nontrivial A] {a : A} (ha : 0 ≤ a) :
(spectrum NNReal a).Nonempty
source
instance Nonneg.instContinuousFunctionalCalculus {A : Type u_1} [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] :
ContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x
source
theorem IsStrictlyPositive.commute_iff {A : Type u_1} [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a b : A} (ha : IsStrictlyPositive a) (hb : IsStrictlyPositive b) :
Commute a b ↔ IsStrictlyPositive (a * b)

### The restriction of a continuous functional calculus is equal to the original one #

source
theorem cfcHom_real_eq_restrict {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [T2Space A] {a : A} (ha : IsSelfAdjoint a) :
cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
source
theorem cfc_real_eq_complex {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [T2Space A] {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) :
cfc f a = cfc (fun (x : ℂ) => ↑(f x.re)) a
source
theorem cfc_complex_eq_real {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] [T2Space A] {f : ℂ → ℂ} (a : A) (hf_real : ∀ x ∈ spectrum ℂ a, star (f x) = f x) (ha : IsSelfAdjoint a := by cfc_tac) :
cfc f a = cfc (fun (x : ℝ) => (f ↑x).re) a
source
theorem cfcₙHom_real_eq_restrict {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} (ha : IsSelfAdjoint a) :
cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯
source
theorem cfcₙ_real_eq_complex {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) :
cfcₙ f a = cfcₙ (fun (x : ℂ) => ↑(f x.re)) a
source
theorem cfcₙ_complex_eq_real {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {f : ℂ → ℂ} (a : A) (hf_real : ∀ x ∈ quasispectrum ℂ a, star (f x) = f x) (ha : IsSelfAdjoint a := by cfc_tac) :
cfcₙ f a = cfcₙ (fun (x : ℝ) => (f ↑x).re) a
source
theorem cfcHom_nnreal_eq_restrict {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) :
cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
source
theorem cfc_nnreal_eq_real {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (ha : 0 ≤ a := by cfc_tac) :
cfc f a = cfc (fun (x : ℝ) => ↑(f x.toNNReal)) a
source
theorem cfc_real_eq_nnreal {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : ℝ → ℝ} (a : A) (hf_nonneg : ∀ x ∈ spectrum ℝ a, 0 ≤ f x) (ha : 0 ≤ a := by cfc_tac) :
cfc f a = cfc (fun (x : NNReal) => (f ↑x).toNNReal) a
source
theorem cfcₙHom_nnreal_eq_restrict {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℝ A] [IsTopologicalRing A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) :
cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯
source
theorem cfcₙ_nnreal_eq_real {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℝ A] [IsTopologicalRing A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (ha : 0 ≤ a := by cfc_tac) :
cfcₙ f a = cfcₙ (fun (x : ℝ) => ↑(f x.toNNReal)) a
source
theorem cfcₙ_real_eq_nnreal {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℝ A] [IsTopologicalRing A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : ℝ → ℝ} (a : A) (hf_nonneg : ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x) (ha : 0 ≤ a := by cfc_tac) :
cfcₙ f a = cfcₙ (fun (x : NNReal) => (f ↑x).toNNReal) a