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 A⁺¹ := 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.
• CStarAlgebra.norm_le_norm_of_nonneg_of_le: in a non-unital C⋆-algebra, if 0 ≤ a ≤ b, then ‖a‖ ≤ ‖b‖.
• CStarAlgebra.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).
• CStarAlgebra.inv_le_inv_iff: in a unital C⋆-algebra, b⁻¹ ≤ a⁻¹ iff a ≤ b.

Tags

continuous functional calculus, normal, selfadjoint

theorem cfc_tsub {A : Type u_1} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f g : NNReal → NNReal) (a : A) (hfg : ∀ x ∈ spectrum NNReal a, g x ≤ f x) (ha : 0 ≤ a := by cfc_tac) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum NNReal a) := by cfc_cont_tac) : cfc (fun (x : NNReal) => f x - g x) a = cfc f a - cfc g a

theorem cfcₙ_tsub {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [IsTopologicalRing A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f g : NNReal → NNReal) (a : A) (hfg : ∀ x ∈ quasispectrum NNReal a, g x ≤ f x) (ha : 0 ≤ a := by cfc_tac) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (hg : ContinuousOn g (quasispectrum NNReal a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : cfcₙ (fun (x : NNReal) => f x - g x) a = cfcₙ f a - cfcₙ g a

@[implicit_reducible]

noncomputable instance Unitization.instPartialOrder {A : Type u_1} [NonUnitalCStarAlgebra A] : PartialOrder (Unitization ℂ A)

Equations

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

instance Unitization.instStarOrderedRing {A : Type u_1} [NonUnitalCStarAlgebra A] : StarOrderedRing (Unitization ℂ A)

theorem Unitization.inr_le_iff {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a b : A) (ha : IsSelfAdjoint a := by cfc_tac) (hb : IsSelfAdjoint b := by cfc_tac) : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem Unitization.inr_nonneg_iff {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} : 0 ≤ ↑a ↔ 0 ≤ a

theorem Unitization.LE.le.of_inr {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} : 0 ≤ ↑a → 0 ≤ a

Alias of the forward direction of Unitization.inr_nonneg_iff.

theorem Unitization.LE.le.inr {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} : 0 ≤ a → 0 ≤ ↑a

Alias of the reverse direction of Unitization.inr_nonneg_iff.

theorem Unitization.nnreal_cfcₙ_eq_cfc_inr {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (f : NNReal → NNReal) (hf₀ : f 0 = 0 := by cfc_zero_tac) : ↑(cfcₙ f a) = cfc f ↑a

theorem Unitization.sqrt_inr {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} : CFC.sqrt ↑a = ↑(CFC.sqrt a)

theorem cfc_nnreal_le_iff {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f g : NNReal → NNReal) (a : A) (ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (hg : ContinuousOn g (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : 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] [Nontrivial A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) : (∃ 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} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) : a ≤ (algebraMap ℝ A) ‖a‖

theorem IsSelfAdjoint.neg_algebraMap_norm_le_self {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) : -(algebraMap ℝ A) ‖a‖ ≤ a

theorem CStarAlgebra.mul_star_le_algebraMap_norm_sq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} : a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

theorem CStarAlgebra.star_mul_le_algebraMap_norm_sq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} : star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

theorem IsSelfAdjoint.toReal_spectralRadius_eq_norm {A : Type u_1} [CStarAlgebra A] {a : A} (ha : IsSelfAdjoint a) : (spectralRadius ℝ a).toReal = ‖a‖

theorem CStarAlgebra.norm_or_neg_norm_mem_spectrum {A : Type u_1} [CStarAlgebra A] [Nontrivial A] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) : ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

theorem CStarAlgebra.nnnorm_mem_spectrum_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] {a : A} (ha : 0 ≤ a := by cfc_tac) : ‖a‖₊ ∈ spectrum NNReal a

theorem CStarAlgebra.norm_mem_spectrum_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] {a : A} (ha : 0 ≤ a := by cfc_tac) : ‖a‖ ∈ spectrum ℝ a

theorem CStarAlgebra.norm_le_iff_le_algebraMap {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) {r : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a := by cfc_tac) : ‖a‖ ≤ r ↔ a ≤ (algebraMap ℝ A) r

theorem CStarAlgebra.nnnorm_le_iff_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (r : NNReal) (ha : 0 ≤ a := by cfc_tac) : ‖a‖₊ ≤ r ↔ a ≤ (algebraMap NNReal A) r

theorem CStarAlgebra.norm_le_one_iff_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (ha : 0 ≤ a := by cfc_tac) : ‖a‖ ≤ 1 ↔ a ≤ 1

theorem CStarAlgebra.nnnorm_le_one_iff_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (ha : 0 ≤ a := by cfc_tac) : ‖a‖₊ ≤ 1 ↔ a ≤ 1

theorem CStarAlgebra.norm_le_natCast_iff_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (n : ℕ) (ha : 0 ≤ a := by cfc_tac) : ‖a‖ ≤ ↑n ↔ a ≤ ↑n

theorem CStarAlgebra.nnnorm_le_natCast_iff_of_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (n : ℕ) (ha : 0 ≤ a := by cfc_tac) : ‖a‖₊ ≤ ↑n ↔ a ≤ ↑n

theorem CStarAlgebra.mem_Icc_algebraMap_iff_norm_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x : A} {r : ℝ} (hr : 0 ≤ r) : x ∈ Set.Icc 0 ((algebraMap ℝ A) r) ↔ 0 ≤ x ∧ ‖x‖ ≤ r

theorem CStarAlgebra.mem_Icc_algebraMap_iff_nnnorm_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x : A} {r : NNReal} : x ∈ Set.Icc 0 ((algebraMap NNReal A) r) ↔ 0 ≤ x ∧ ‖x‖₊ ≤ r

theorem CStarAlgebra.mem_Icc_iff_norm_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x : A} : x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

theorem CStarAlgebra.mem_Icc_iff_nnnorm_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x : A} : x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1

theorem CFC.conjugate_rpow_neg_one_half {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) (ha : IsStrictlyPositive a := by cfc_tac) : a ^ (-(1 / 2)) * a * a ^ (-(1 / 2)) = 1

theorem CStarAlgebra.isUnit_of_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) {b : A} (hab : a ≤ b) (h : IsStrictlyPositive a := by cfc_tac) : IsUnit b

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

theorem le_iff_norm_sqrt_mul_rpow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : IsStrictlyPositive b := by cfc_tac) : a ≤ b ↔ ‖CFC.sqrt a * b ^ (-(1 / 2))‖ ≤ 1

theorem le_iff_norm_sqrt_mul_sqrt_inv {A : Type u_1} [CStarAlgebra 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 CStarAlgebra.inv_le_inv {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing 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 CStarAlgebra.inv_le_inv_iff {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing 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 CStarAlgebra.inv_le_iff {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : Aˣ} (ha : 0 ≤ ↑a) (hb : 0 ≤ ↑b) : ↑a⁻¹ ≤ ↑b ↔ ↑b⁻¹ ≤ ↑a

theorem CStarAlgebra.le_inv_iff {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : Aˣ} (ha : 0 ≤ ↑a) (hb : 0 ≤ ↑b) : ↑a ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a⁻¹

theorem CStarAlgebra.one_le_inv_iff_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 0 ≤ ↑a) : 1 ≤ ↑a⁻¹ ↔ a ≤ 1

theorem CStarAlgebra.inv_le_one_iff_one_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 0 ≤ ↑a) : ↑a⁻¹ ≤ 1 ↔ 1 ≤ a

theorem CStarAlgebra.inv_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 1 ≤ a) : ↑a⁻¹ ≤ 1

theorem CStarAlgebra.le_one_of_one_le_inv {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : Aˣ} (ha : 1 ≤ ↑a⁻¹) : ↑a ≤ 1

theorem CStarAlgebra.rpow_neg_one_le_rpow_neg_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : a ≤ b) (ha : IsStrictlyPositive a := by cfc_tac) : b ^ (-1) ≤ a ^ (-1)

theorem CStarAlgebra.rpow_neg_one_le_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : 1 ≤ a) : a ^ (-1) ≤ 1

theorem IsStrictlyPositive.of_le {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (ha : IsStrictlyPositive a) (hab : a ≤ b) : IsStrictlyPositive b

theorem IsStrictlyPositive.add_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (ha : IsStrictlyPositive a) (hb : 0 ≤ b) : IsStrictlyPositive (a + b)

theorem IsStrictlyPositive.nonneg_add {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (ha : 0 ≤ a) (hb : IsStrictlyPositive b) : IsStrictlyPositive (a + b)

theorem isStrictlyPositive_add {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (h : IsStrictlyPositive a ∧ 0 ≤ b ∨ 0 ≤ a ∧ IsStrictlyPositive b) : IsStrictlyPositive (a + b)

instance CStarAlgebra.instNonnegSpectrumClassComplexNonUnital {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : NonnegSpectrumClass ℂ A

theorem CStarAlgebra.norm_le_norm_of_nonneg_of_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖ ≤ ‖b‖

theorem CStarAlgebra.nnnorm_le_nnnorm_of_nonneg_of_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖₊ ≤ ‖b‖₊

theorem CStarAlgebra.star_left_conjugate_le_norm_smul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : star a * b * a ≤ ‖b‖ • (star a * a)

@[deprecated CStarAlgebra.star_left_conjugate_le_norm_smul (since := "2025-10-20")]

theorem CStarAlgebra.conjugate_le_norm_smul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : star a * b * a ≤ ‖b‖ • (star a * a)

Alias of CStarAlgebra.star_left_conjugate_le_norm_smul.

theorem CStarAlgebra.star_right_conjugate_le_norm_smul {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : a * b * star a ≤ ‖b‖ • (a * star a)

@[deprecated CStarAlgebra.star_right_conjugate_le_norm_smul (since := "2025-10-20")]

theorem CStarAlgebra.conjugate_le_norm_smul' {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : a * b * star a ≤ ‖b‖ • (a * star a)

Alias of CStarAlgebra.star_right_conjugate_le_norm_smul.

theorem CStarAlgebra.isClosed_nonneg {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : IsClosed {a : A | 0 ≤ a}

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

instance CStarAlgebra.instOrderClosedTopology {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : OrderClosedTopology A

theorem CStarAlgebra.inr_mem_Icc_iff_norm_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x : A} : ↑x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

theorem CStarAlgebra.inr_mem_Icc_iff_nnnorm_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {x : A} : ↑x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1

theorem CStarAlgebra.preimage_inr_Icc_zero_one {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Unitization.inr ⁻¹' Set.Icc 0 1 = {x : A | 0 ≤ x} ∩ Metric.closedBall 0 1

theorem IsStarProjection.mul_right_and_mul_left_of_nonneg_of_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a e : A} (he : IsStarProjection e) (ha : 0 ≤ a) (hae : a ≤ e) : a * e = a ∧ e * a = a

theorem IsStarProjection.conjugate_of_nonneg_of_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a e : A} (he : IsStarProjection e) (ha : 0 ≤ a) (hae : a ≤ e) : e * a * e = a

theorem CStarAlgebra.pow_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : 0 ≤ a := by cfc_tac) (n : ℕ) : 0 ≤ a ^ n

theorem CStarAlgebra.pow_monotone {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : 1 ≤ a) : Monotone fun (x : ℕ) => a ^ x

theorem CStarAlgebra.pow_antitone {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a : A} (ha₀ : 0 ≤ a := by cfc_tac) (ha₁ : a ≤ 1) : Antitone fun (x : ℕ) => a ^ x