# Some lemmas on the spectrum and quasispectrum of elements and positivity #

source
theorem SpectrumRestricts.nnreal_iff {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} :
SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x
source
theorem SpectrumRestricts.nnreal_of_nonneg {A : Type u_1} [Ring A] [Algebra ℝ A] [PartialOrder A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) :
SpectrumRestricts a ⇑ContinuousMap.realToNNReal
source
theorem SpectrumRestricts.nnreal_le_iff {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} :
(∀ x ∈ spectrum NNReal a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, ↑r ≤ x
source
theorem SpectrumRestricts.nnreal_lt_iff {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} :
(∀ x ∈ spectrum NNReal a, r < x) ↔ ∀ x ∈ spectrum ℝ a, ↑r < x
source
theorem SpectrumRestricts.le_nnreal_iff {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} :
(∀ x ∈ spectrum NNReal a, x ≤ r) ↔ ∀ x ∈ spectrum ℝ a, x ≤ ↑r
source
theorem SpectrumRestricts.lt_nnreal_iff {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} (ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} :
(∀ x ∈ spectrum NNReal a, x < r) ↔ ∀ x ∈ spectrum ℝ a, x < ↑r
source
theorem QuasispectrumRestricts.nnreal_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} :
QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ quasispectrum ℝ a, 0 ≤ x
source
theorem QuasispectrumRestricts.nnreal_of_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a) :
QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
source
theorem QuasispectrumRestricts.le_nnreal_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} (ha : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} :
(∀ x ∈ quasispectrum NNReal a, x ≤ r) ↔ ∀ x ∈ quasispectrum ℝ a, x ≤ ↑r
source
theorem QuasispectrumRestricts.lt_nnreal_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} (ha : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) {r : NNReal} :
(∀ x ∈ quasispectrum NNReal a, x < r) ↔ ∀ x ∈ quasispectrum ℝ a, x < ↑r
source
theorem coe_mem_spectrum_real_of_nonneg {A : Type u_1} [Ring A] [PartialOrder A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] {a : A} {x : NNReal} (ha : 0 ≤ a := by cfc_tac) :
↑x ∈ spectrum ℝ a ↔ x ∈ spectrum NNReal a