Instances of the continuous functional calculus

Main theorems

• IsStarNormal.instContinuousFunctionalCalculus: the continuous functional calculus for normal elements in a unital C⋆-algebra over ℂ.
• 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 ℝ.
• CStarAlgebra.instNonnegSpectrumClass: In a unital C⋆-algebra over ℂ which is also a StarOrderedRing, the spectrum of a nonnegative element is nonnegative.

Tags

continuous functional calculus, normal, selfadjoint

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

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 𝕜 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

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 𝕜 p₁] : (cfcₙAux ⋯ a ha) (ContinuousMapZero.id ⋯) = ↑a

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 𝕜 p₁] : Topology.IsClosedEmbedding ⇑(cfcₙAux ⋯ a ha)

@[deprecated isClosedEmbedding_cfcₙAux]

theorem closedEmbedding_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 𝕜 p₁] : Topology.IsClosedEmbedding ⇑(cfcₙAux ⋯ a ha)

Alias of isClosedEmbedding_cfcₙAux.

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 𝕜 p₁] (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) : spectrum 𝕜 ((cfcₙAux ⋯ a ha) f) = Set.range ⇑f

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 𝕜 p₁] [CompleteSpace A] (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) : (cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

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 𝕜 p₁] [CompleteSpace A] [CStarRing A] : NonUnitalContinuousFunctionalCalculus 𝕜 p

Continuous functional calculus for normal elements

instance IsStarNormal.instContinuousFunctionalCalculus {A : Type u_1} [CStarAlgebra A] : ContinuousFunctionalCalculus ℂ IsStarNormal

Equations

• ⋯ = ⋯

theorem cfcHom_eq_of_isStarNormal {A : Type u_1} [CStarAlgebra A] (a : A) [ha : IsStarNormal a] : cfcHom ha = (StarAlgebra.elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)

instance IsStarNormal.instNonUnitalContinuousFunctionalCalculus {A : Type u_1} [NonUnitalCStarAlgebra A] : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal

Equations

• ⋯ = ⋯

theorem inr_comp_cfcₙHom_eq_cfcₙAux {A : Type u_1} [NonUnitalCStarAlgebra A] (a : A) [ha : IsStarNormal a] : (Unitization.inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux ⋯ a ha

Continuous functional calculus for selfadjoint elements

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 ℂ 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 ℝ.

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

Alias of the forward direction 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 ℝ.

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

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

instance IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal] : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint

Equations

• ⋯ = ⋯

theorem isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {a : A} : IsSelfAdjoint a ↔ IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM

An element in a C⋆-algebra is selfadjoint if and only if it is normal and its spectrum is contained in ℝ.

theorem IsSelfAdjoint.spectrumRestricts {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {a : A} (ha : IsSelfAdjoint a) : SpectrumRestricts a ⇑Complex.reCLM

theorem SpectrumRestricts.isSelfAdjoint {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] (a : A) (ha : SpectrumRestricts a ⇑Complex.reCLM) [IsStarNormal a] : IsSelfAdjoint a

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

instance IsSelfAdjoint.instContinuousFunctionalCalculus {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] : ContinuousFunctionalCalculus ℝ IsSelfAdjoint

Equations

• ⋯ = ⋯

theorem IsSelfAdjoint.spectrum_nonempty {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [Nontrivial A] {a : A} (ha : IsSelfAdjoint a) : (spectrum ℝ a).Nonempty

Continuous functional calculus for nonnegative elements

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 ℝ IsSelfAdjoint] {a : A} (ha₁ : IsSelfAdjoint a) (ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) : ∃ (x : A), IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a

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 ℝ IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} : 0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal

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 ℝ IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : NonUnitalContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x

Equations

• ⋯ = ⋯

theorem NNReal.spectrum_nonempty {A : Type u_2} [Ring A] [StarRing A] [PartialOrder A] [TopologicalSpace A] [Algebra NNReal A] [ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x] [Nontrivial A] {a : A} (ha : 0 ≤ a) : (spectrum NNReal a).Nonempty

theorem CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts {A : Type u_1} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] {a : A} (ha₁ : IsSelfAdjoint a) (ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) : ∃ (x : A), IsSelfAdjoint x ∧ SpectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x ^ 2 = a

theorem nonneg_iff_isSelfAdjoint_and_spectrumRestricts {A : Type u_1} [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} : 0 ≤ a ↔ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

instance Nonneg.instContinuousFunctionalCalculus {A : Type u_1} [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x

Equations

• ⋯ = ⋯

The spectrum of a nonnegative element is nonnegative

theorem SpectrumRestricts.nnreal_iff_nnnorm {A : Type u_1} [CStarAlgebra A] {a : A} {t : NNReal} (ha : IsSelfAdjoint a) (ht : ‖a‖₊ ≤ t) : SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t

theorem SpectrumRestricts.nnreal_add {A : Type u_1} [CStarAlgebra A] {a b : A} (ha₁ : IsSelfAdjoint a) (hb₁ : IsSelfAdjoint b) (ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) (hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal) : SpectrumRestricts (a + b) ⇑ContinuousMap.realToNNReal

theorem IsSelfAdjoint.sq_spectrumRestricts {A : Type u_1} [CStarAlgebra A] {a : A} (ha : IsSelfAdjoint a) : SpectrumRestricts (a ^ 2) ⇑ContinuousMap.realToNNReal

theorem SpectrumRestricts.eq_zero_of_neg {A : Type u_1} [CStarAlgebra A] {a : A} (ha : IsSelfAdjoint a) (ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) (ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal) : a = 0

theorem SpectrumRestricts.smul_of_nonneg {A : Type u_2} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : ℝ} (hr : 0 ≤ r) : SpectrumRestricts (r • a) ⇑ContinuousMap.realToNNReal

theorem spectrum_star_mul_self_nonneg {A : Type u_1} [CStarAlgebra A] {b : A} (x : ℝ) : x ∈ spectrum ℝ (star b * b) → 0 ≤ x

theorem IsSelfAdjoint.coe_mem_spectrum_complex {A : Type u_2} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {a : A} {x : ℝ} (ha : IsSelfAdjoint a := by cfc_tac) : ↑x ∈ spectrum ℂ a ↔ x ∈ spectrum ℝ a

instance CStarAlgebra.instNonnegSpectrumClass {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : NonnegSpectrumClass ℝ A

Equations

• ⋯ = ⋯

instance CStarAlgebra.instNonnegSpectrumClassComplexUnital {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : NonnegSpectrumClass ℂ A

Equations

• ⋯ = ⋯

@[reducible]

def CStarAlgebra.spectralOrder (A : Type u_1) [CStarAlgebra A] : PartialOrder A

The partial order on a unital C⋆-algebra defined by x ≤ y if and only if y - x is selfadjoint and has nonnegative spectrum.

This is not declared as an instance because one may already have a partial order with better definitional properties. However, it can be useful to invoke this as an instance in proofs.

Equations

• CStarAlgebra.spectralOrder A = PartialOrder.mk ⋯

theorem CStarAlgebra.spectralOrderedRing (A : Type u_1) [CStarAlgebra A] : StarOrderedRing A

The CStarAlgebra.spectralOrder on a unital C⋆-algebra is a StarOrderedRing.

instance CStarAlgebra.instNonnegSpectrumClass' {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : NonnegSpectrumClass ℝ A

Equations

• ⋯ = ⋯

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

theorem cfcHom_real_eq_restrict {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] [UniqueContinuousFunctionalCalculus ℝ A] {a : A} (ha : IsSelfAdjoint a) : cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯

theorem cfc_real_eq_complex {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] [UniqueContinuousFunctionalCalculus ℝ A] {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) : cfc f a = cfc (fun (x : ℂ) => ↑(f x.re)) a

theorem cfcₙHom_real_eq_restrict {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] {a : A} (ha : IsSelfAdjoint a) : cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯

theorem cfcₙ_real_eq_complex {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) : cfcₙ f a = cfcₙ (fun (x : ℂ) => ↑(f x.re)) a

theorem cfcHom_nnreal_eq_restrict {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra ℝ A] [TopologicalRing A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x] [UniqueContinuousFunctionalCalculus ℝ A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) : cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯

theorem cfc_nnreal_eq_real {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra ℝ A] [TopologicalRing A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x] [UniqueContinuousFunctionalCalculus ℝ A] [NonnegSpectrumClass ℝ A] {a : A} (f : NNReal → NNReal) (ha : 0 ≤ a := by cfc_tac) : cfc f a = cfc (fun (x : ℝ) => ↑(f x.toNNReal)) a

theorem cfcₙHom_nnreal_eq_restrict {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℝ A] [TopologicalRing A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) : cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯

theorem cfcₙ_nnreal_eq_real {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℝ A] [TopologicalRing A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [NonnegSpectrumClass ℝ A] {a : A} (f : NNReal → NNReal) (ha : 0 ≤ a := by cfc_tac) : cfcₙ f a = cfcₙ (fun (x : ℝ) => ↑(f x.toNNReal)) a

theorem Unitization.cfcₙ_eq_cfc_inr {A : Type u_1} [NonUnitalCStarAlgebra A] {R : Type u_2} [Semifield R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [CompleteSpace R] [Algebra R ℂ] [IsScalarTower R ℂ A] {p : A → Prop} {p' : Unitization ℂ A → Prop} [NonUnitalContinuousFunctionalCalculus R p] [ContinuousFunctionalCalculus R p'] [UniqueNonUnitalContinuousFunctionalCalculus R (Unitization ℂ A)] (hp : ∀ {a : A}, p' ↑a ↔ p a) (a : A) (f : R → R) (hf₀ : f 0 = 0 := by cfc_zero_tac) : ↑(cfcₙ f a) = cfc f ↑a

This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke versions for ℝ≥0, ℝ, and ℂ.

theorem Unitization.complex_cfcₙ_eq_cfc_inr {A : Type u_1} [NonUnitalCStarAlgebra A] (a : A) (f : ℂ → ℂ) (hf₀ : f 0 = 0 := by cfc_zero_tac) : ↑(cfcₙ f a) = cfc f ↑a

theorem Unitization.real_cfcₙ_eq_cfc_inr {A : Type u_1} [NonUnitalCStarAlgebra A] (a : A) (f : ℝ → ℝ) (hf₀ : f 0 = 0 := by cfc_zero_tac) : ↑(cfcₙ f a) = cfc f ↑a

note: the version for ℝ≥0, Unization.nnreal_cfcₙ_eq_cfc_inr, can be found in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order