spectralOrderedRing — Mathlib

English

The unital nonnegative spectrum class asserts nonnegativity of spectrum for complex numbers in a unital C*-algebra.

Русский

Унитарный класс неотрицательного спектра утверждает неотрицательность спектра комплексных чисел в унитальной C*-алгебре.

LaTeX

$$NonnegSpectrumClass Complex A$$

Lean4

/-- The `CStarAlgebra.spectralOrder` on a C⋆-algebra is a `StarOrderedRing`. -/
theorem spectralOrderedRing : @StarOrderedRing A _ (CStarAlgebra.spectralOrder A) _ :=
  let _ := CStarAlgebra.spectralOrder A
  {
    le_iff := by
      intro x y
      constructor
      · intro h
        obtain ⟨s, hs₁, _, hs₂⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.2
        refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩
        exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq]⟩
      · rintro ⟨p, hp, rfl⟩
        simp only [spectralOrder, add_sub_cancel_left]
        induction hp using AddSubmonoid.closure_induction with
        | mem x hx =>
          obtain ⟨s, rfl⟩ := hx
          refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff, Unitization.inr_mul,
            Unitization.inr_star]
          exact spectrum_star_mul_self_nonneg
        | zero =>
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
          nontriviality A
          simp
        | add x y _ _ hx
          hy =>
          simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
          rw [Unitization.inr_add]
          exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩ }

Похожие утверждения