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.

We also put an order instance on Unitization ℂ A when A is a C⋆-algebra via the spectral order.

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.
• CstarRing.norm_le_norm_of_nonneg_of_le: in a non-unital C⋆-algebra, if 0 ≤ a ≤ b, then ‖a‖ ≤ ‖b‖.
• CstarRing.conjugate_le_norm_smul: in a non-unital C⋆-algebra, we have that star a * b * a ≤ ‖b‖ • (star a * a) (and a primed version for the a * b * star a case).

Tags

continuous functional calculus, normal, selfadjoint

instance Unitization.instPartialOrder {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] : PartialOrder (Unitization ℂ A)

Equations

• Unitization.instPartialOrder = CstarRing.spectralOrder (Unitization ℂ A)

instance Unitization.instStarOrderedRing {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] : StarOrderedRing (Unitization ℂ A)

Equations

• ⋯ = ⋯

theorem Unitization.inr_le_iff {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] (a : A) (b : A) (ha : autoParam (IsSelfAdjoint a) _auto✝) (hb : autoParam (IsSelfAdjoint b) _auto✝) : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem Unitization.inr_nonneg_iff {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] {a : A} : 0 ≤ ↑a ↔ 0 ≤ a

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 CstarRing.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 CstarRing.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)

theorem IsSelfAdjoint.toReal_spectralRadius_eq_norm {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] {a : A} (ha : IsSelfAdjoint a) : (spectralRadius ℝ a).toReal = ‖a‖

theorem CstarRing.norm_or_neg_norm_mem_spectrum {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [Nontrivial A] {a : A} (ha : autoParam (IsSelfAdjoint a) _auto✝) : ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

theorem CstarRing.nnnorm_mem_spectrum_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] {a : A} (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖₊ ∈ spectrum NNReal a

theorem CstarRing.norm_mem_spectrum_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CstarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] {a : A} (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖ ∈ spectrum ℝ a

instance CstarRing.instNonnegSpectrumClassComplexNonUnital {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] : NonnegSpectrumClass ℂ A

Equations

• ⋯ = ⋯

theorem CstarRing.norm_le_norm_of_nonneg_of_le {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] {a : A} {b : A} (ha : autoParam (0 ≤ a) _auto✝) (hab : a ≤ b) : ‖a‖ ≤ ‖b‖

theorem CstarRing.conjugate_le_norm_smul {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] {a : A} {b : A} (hb : autoParam (IsSelfAdjoint b) _auto✝) : star a * b * a ≤ ‖b‖ • (star a * a)

theorem CstarRing.conjugate_le_norm_smul' {A : Type u_1} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A] [NormedSpace ℂ A] [StarModule ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] {a : A} {b : A} (hb : autoParam (IsSelfAdjoint b) _auto✝) : a * b * star a ≤ ‖b‖ • (a * star a)