Facts about star-ordered rings that depend on the continuous functional calculus

This file contains various basic facts about star-ordered rings (i.e. mainly C⋆-algebras) that depend on the continuous functional calculus.

Main theorems

• IsSelfAdjoint.le_algebraMap_norm_self and IsSelfAdjoint.le_algebraMap_norm_self, which respectively show that a ≤ algebraMap ℝ A ‖a‖ and -(algebraMap ℝ A ‖a‖) ≤ a in a C⋆-algebra.
• mul_star_le_algebraMap_norm_sq and star_mul_le_algebraMap_norm_sq, which give similar statements for a * star a and star a * a.

Tags

continuous functional calculus, normal, selfadjoint

theorem IsSelfAdjoint.le_algebraMap_norm_self {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : autoParam (IsSelfAdjoint a) _auto✝) : a ≤ (algebraMap ℝ A) ‖a‖

theorem IsSelfAdjoint.neg_algebraMap_norm_le_self {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : autoParam (IsSelfAdjoint a) _auto✝) : -(algebraMap ℝ A) ‖a‖ ≤ a

theorem mul_star_le_algebraMap_norm_sq {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} : a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

theorem star_mul_le_algebraMap_norm_sq {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} : star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)