Some lemmas on the spectrum and quasispectrum of elements and positivity

theorem SpectrumRestricts.nnreal_iff {A : Type u_1} [Ring A] [Algebra ℝ A] {a : A} : SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x

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

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

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

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

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

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

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

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

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

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