Documentation

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

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 #

Tags #

continuous functional calculus, normal, selfadjoint

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) xspectrum 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 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 CStarAlgebra.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) :

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) :
theorem CStarAlgebra.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 CStarAlgebra.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 CStarAlgebra.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 CStarAlgebra.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 CStarAlgebra.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)

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