3. Order Lemmas🔗

Let \mathcal{A} be a unital C^*-algebra in this chapter. We collect lemmas for the ordering of elements in \mathcal{A}. Recall that a self-adjoint element a \in \mathcal{A} is said to be positive if its spectrum is contained in \mathbb{R}_{\ge 0}. This is written a \ge 0. If a, b \in \mathcal{A} are self-adjoint then b \le a if b - a \ge 0.

Lemma3.1

uses 0used by 1✓L∃∀N

(Sakai 1.4.4) Let h \in \mathcal{A}. The following are equivalent:

h \ge 0;
there exists x \in \mathcal{A} such that h = x^* x.

Lean code for Lemma3.1●2 theorems

theoremdefined in Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

complete

theorem CStarAlgebra.nonneg_TFAE.{u_1} {A : Type u_1} [PartialOrder A]
  [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A]
  [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A]
  {a : A} :
  [0 ≤ a, a = CFC.sqrt a * CFC.sqrt a, ∃ b, 0 ≤ b ∧ a = b * b,
      ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧
        QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE

theorem CStarAlgebra.nonneg_TFAE.{u_1}
  {A : Type u_1} [PartialOrder A]
  [NonUnitalRing A] [TopologicalSpace A]
  [StarRing A] [Module ℝ A]
  [SMulCommClass ℝ A A]
  [IsScalarTower ℝ A A]
  [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ
      A IsSelfAdjoint]
  [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A]
  {a : A} :
  [0 ≤ a, a = CFC.sqrt a * CFC.sqrt a,
      ∃ b, 0 ≤ b ∧ a = b * b,
      ∃ b, IsSelfAdjoint b ∧ a = b * b,
      ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺,
      IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧
        QuasispectrumRestricts a
          ⇑ContinuousMap.realToNNReal].TFAE

For an element `a` in a C⋆-algebra, TFAE:
1. `0 ≤ a`
2. `a = sqrt a * sqrt a`
3. `a = b * b` for some nonnegative `b`
4. `a = b * b` for some self-adjoint `b`
5. `a = star b * b` for some `b`
6. `a = b * star b` for some `b`
7. `a = a⁺`
8. `a` is self-adjoint and `a⁻ = 0`
9. `a` is self-adjoint and has nonnegative spectrum

theoremdefined in Mathlib/Algebra/Order/Star/Basic.lean

complete

theorem StarOrderedRing.nonneg_iff.{u_1} {R : Type u_1} [NonUnitalSemiring R]
  [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
  0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)

theorem StarOrderedRing.nonneg_iff.{u_1}
  {R : Type u_1} [NonUnitalSemiring R]
  [PartialOrder R] [StarRing R]
  [StarOrderedRing R] {x : R} :
  0 ≤ x ↔
    x ∈
      AddSubmonoid.closure
        (Set.range fun s ↦ star s * s)

Corollary3.2

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsmathlib

If h, a \in \mathcal{A} with h \ge 0 then a^* h a \ge 0.

Lean code for Corollary3.2●1 theorem

theoremdefined in Mathlib/Algebra/Order/Star/Basic.lean

complete

theorem star_left_conjugate_nonneg.{u_1} {R : Type u_1} [NonUnitalSemiring R]
  [PartialOrder R] [StarRing R] [StarOrderedRing R] {a : R} (ha : 0 ≤ a)
  (c : R) : 0 ≤ star c * a * c

theorem star_left_conjugate_nonneg.{u_1}
  {R : Type u_1} [NonUnitalSemiring R]
  [PartialOrder R] [StarRing R]
  [StarOrderedRing R] {a : R} (ha : 0 ≤ a)
  (c : R) : 0 ≤ star c * a * c

Proof for Corollary 3.2

uses 0

By Lemma 3.1, a^* h a = a^* x^* x a = (xa)^* (xa) \ge 0.

Lemma3.3

uses 0

Used by 4

Reverse dependency previews

Preview

Lemma 4.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsmathlib

If x \in \mathcal{A} is self-adjoint then \|x\| 1 - x \ge 0.

Lean code for Lemma3.3●1 theorem

theoremdefined in Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

complete

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

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