instNonnegSpectrumClass — Mathlib

English

There is a NonnegSpectrumClass for the unital C*-algebra, ensuring nonnegative spectra.

Русский

Существет класс неотрицательного спектра для унитального C*-алгебры, обеспечивающий неотрицательные спектры.

LaTeX

$$NonnegSpectrumClass Real A$$

Lean4

instance instNonnegSpectrumClass : NonnegSpectrumClass ℝ A :=
  .of_spectrum_nonneg fun a ha ↦ by
    rw [StarOrderedRing.nonneg_iff] at ha
    induction ha using AddSubmonoid.closure_induction with
    | mem x hx =>
      obtain ⟨b, rfl⟩ := hx
      exact spectrum_star_mul_self_nonneg
    | zero =>
      nontriviality A
      simp
    | add x y x_mem y_mem hx hy =>
      rw [← SpectrumRestricts.nnreal_iff] at hx hy ⊢
      rw [← StarOrderedRing.nonneg_iff] at x_mem y_mem
      exact hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy

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