Instances of the continuous functional calculus

Main definitions

• 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 unital C⋆-algebra over ℂ.
• Nonneg.instContinuousFunctionalCalculus: the continuous functional calculus for nonnegative elements in a unital C⋆-algebra over ℂ, which is also a StarOrderedRing.

Tags

continuous functional calculus, normal, selfadjoint

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] [ContinuousFunctionalCalculus R p] (a : A) (f : R → R) : IsStarNormal (cfc f a)

Equations

• ⋯ = ⋯

instance IsStarNormal.instContinuousFunctionalCalculus {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] : ContinuousFunctionalCalculus ℂ IsStarNormal

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.

theorem IsSelfAdjoint.continuousFunctionalCalculus_of_compactSpace_spectrum {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] [h : ∀ (x : A), CompactSpace ↑(spectrum ℂ x)] : ContinuousFunctionalCalculus ℝ IsSelfAdjoint

instance IsSelfAdjoint.instContinuousFunctionalCalculus {A : Type u_2} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] : ContinuousFunctionalCalculus ℝ IsSelfAdjoint

Equations

• ⋯ = ⋯

theorem unitary_iff_isStarNormal_and_spectrum_subset_circle {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {u : A} : u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑circle

theorem mem_unitary_of_spectrum_subset_circle {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {u : A} [IsStarNormal u] (hu : spectrum ℂ u ⊆ ↑circle) : u ∈ unitary A

theorem spectrum_subset_circle_of_mem_unitary {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {u : A} (hu : u ∈ unitary A) : spectrum ℂ u ⊆ ↑circle

theorem SpectrumRestricts.nnreal_iff_nnnorm {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ 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} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] {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} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] {a : A} (ha : IsSelfAdjoint a) : SpectrumRestricts (a ^ 2) ⇑ContinuousMap.realToNNReal

theorem SpectrumRestricts.eq_zero_of_neg {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ 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} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] {b : A} (x : ℝ) : x ∈ spectrum ℝ (star b * b) → 0 ≤ x

theorem nonneg_iff_isSelfAdjoint_and_spectrumRestricts {A : Type u_1} [NormedRing A] [CompleteSpace A] [PartialOrder A] [StarOrderedRing A] [CstarRing A] [NormedAlgebra ℂ A] [StarModule ℂ A] {a : A} : 0 ≤ a ↔ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

instance Nonneg.instContinuousFunctionalCalculus {A : Type u_1} [NormedRing A] [CompleteSpace A] [PartialOrder A] [StarOrderedRing A] [CstarRing A] [NormedAlgebra ℂ A] [StarModule ℂ A] : ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x

Equations

• ⋯ = ⋯