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
andIsSelfAdjoint.le_algebraMap_norm_self
, which respectively show thata ≤ algebraMap ℝ A ‖a‖
and-(algebraMap ℝ A ‖a‖) ≤ a
in a C⋆-algebra.mul_star_le_algebraMap_norm_sq
andstar_mul_le_algebraMap_norm_sq
, which give similar statements fora * star a
andstar 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✝)
:
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}
:
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}
: