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).
• CStarRing.inv_le_inv_iff: in a unital C⋆-algebra, b⁻¹ ≤ a⁻¹ iff a ≤ b.

Tags

continuous functional calculus, normal, selfadjoint

instance Unitization.instPartialOrder {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] : PartialOrder (Unitization ℂ A)

Equations

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

instance Unitization.instStarOrderedRing {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] : 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 cfc_nnreal_le_iff {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra ℝ A] [TopologicalRing A] [NonnegSpectrumClass ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueContinuousFunctionalCalculus ℝ A] (f : NNReal → NNReal) (g : NNReal → NNReal) (a : A) (ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) (hf : autoParam (ContinuousOn f (spectrum NNReal a)) _auto✝) (hg : autoParam (ContinuousOn g (spectrum NNReal a)) _auto✝) (ha : autoParam (0 ≤ a) _auto✝) : cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum NNReal a, f x ≤ g x

cfc_le_iff only applies to a scalar ring where R is an actual Ring, and not a Semiring. However, this theorem still holds for ℝ≥0 as long as the algebra A itself is an ℝ-algebra.

theorem CFC.exists_pos_algebraMap_le_iff {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] [ContinuousFunctionalCalculus ℝ IsSelfAdjoint] {a : A} [CompactSpace ↑(spectrum ℝ a)] (h_non : (spectrum ℝ a).Nonempty) (ha : autoParam (IsSelfAdjoint a) _auto✝) : (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

In a unital ℝ-algebra A with a continuous functional calculus, an element a : A is larger than some algebraMap ℝ A r if and only if every element of the ℝ-spectrum is nonnegative.

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

theorem CStarRing.norm_le_iff_le_algebraMap {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (a : A) {r : ℝ} (hr : 0 ≤ r) (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A) r

theorem CStarRing.nnnorm_le_iff_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (a : A) (r : NNReal) (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖₊ ≤ r ↔ a ≤ (algebraMap NNReal A) r

theorem CStarRing.norm_le_one_iff_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (a : A) (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖ ≤ 1 ↔ a ≤ 1

theorem CStarRing.nnnorm_le_one_iff_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (a : A) (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖₊ ≤ 1 ↔ a ≤ 1

theorem CStarRing.norm_le_natCast_iff_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (a : A) (n : ℕ) (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖ ≤ ↑n ↔ a ≤ ↑n

theorem CStarRing.nnnorm_le_natCast_iff_of_nonneg {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] (a : A) (n : ℕ) (ha : autoParam (0 ≤ a) _auto✝) : ‖a‖₊ ≤ ↑n ↔ a ≤ ↑n

theorem CFC.conjugate_rpow_neg_one_half {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} (h₀ : IsUnit a) (ha : autoParam (0 ≤ a) _auto✝) : a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1

theorem CStarRing.isUnit_of_le {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} {b : A} (h₀ : IsUnit a) (ha : autoParam (0 ≤ a) _auto✝) (hab : a ≤ b) : IsUnit b

In a unital C⋆-algebra, if a is nonnegative and invertible, and a ≤ b, then b is invertible.

theorem le_iff_norm_sqrt_mul_rpow {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} {b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb : 0 ≤ b) : a ≤ b ↔ ‖CFC.sqrt a * b ^ (-(1 / 2))‖ ≤ 1

theorem le_iff_norm_sqrt_mul_sqrt_inv {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} {b : Aˣ} (ha : 0 ≤ a) (hb : 0 ≤ ↑b) : a ≤ ↑b ↔ ‖CFC.sqrt a * CFC.sqrt ↑b⁻¹‖ ≤ 1

theorem CStarRing.inv_le_inv {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} {b : Aˣ} (ha : 0 ≤ ↑a) (hab : ↑a ≤ ↑b) : ↑b⁻¹ ≤ ↑a⁻¹

In a unital C⋆-algebra, if 0 ≤ a ≤ b and a and b are units, then b⁻¹ ≤ a⁻¹.

theorem CStarRing.inv_le_inv_iff {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} {b : Aˣ} (ha : 0 ≤ ↑a) (hb : 0 ≤ ↑b) : ↑a⁻¹ ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a

In a unital C⋆-algebra, if 0 ≤ a and 0 ≤ b and a and b are units, then a⁻¹ ≤ b⁻¹ if and only if b ≤ a.

theorem CStarRing.inv_le_iff {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} {b : Aˣ} (ha : 0 ≤ ↑a) (hb : 0 ≤ ↑b) : ↑a⁻¹ ≤ ↑b ↔ ↑b⁻¹ ≤ ↑a

theorem CStarRing.le_inv_iff {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} {b : Aˣ} (ha : 0 ≤ ↑a) (hb : 0 ≤ ↑b) : ↑a ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a⁻¹

theorem CStarRing.one_le_inv_iff_le_one {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 0 ≤ ↑a) : 1 ≤ ↑a⁻¹ ↔ a ≤ 1

theorem CStarRing.inv_le_one_iff_one_le {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 0 ≤ ↑a) : ↑a⁻¹ ≤ 1 ↔ 1 ≤ a

theorem CStarRing.inv_le_one {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 1 ≤ a) : ↑a⁻¹ ≤ 1

theorem CStarRing.le_one_of_one_le_inv {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 1 ≤ ↑a⁻¹) : ↑a ≤ 1

theorem CStarRing.rpow_neg_one_le_rpow_neg_one {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} {b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hau : IsUnit a) : b ^ (-1) ≤ a ^ (-1)

theorem CStarRing.rpow_neg_one_le_one {A : Type u_1} [NormedRing A] [StarRing A] [CStarRing A] [CompleteSpace A] [NormedAlgebra ℂ A] [StarModule ℂ A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : 1 ≤ a) : a ^ (-1) ≤ 1

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)

theorem CStarRing.isClosed_nonneg {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] : IsClosed {a : A | 0 ≤ a}

The set of nonnegative elements in a C⋆-algebra is closed.