refactor: redefine spectralRadius in terms of quasispectrum

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -268,6 +268,19 @@ instance quasispectrum.instZero [Nontrivial R] (a : A) : Zero (quasispectrum R a
 
 variable {R}
 
+@[simp]
+lemma quasispectrum_zero {R A : Type*} [Field R] [NonUnitalRing A] [Module R A] :
+    quasispectrum R (0 : A) = {0} := by
+  refine Set.eq_singleton_iff_unique_mem.mpr ⟨quasispectrum.zero_mem R 0, fun r hr => ?_⟩
+  by_contra h
+  exact hr (isUnit_iff_ne_zero.mpr h) (by simp only [smul_zero, neg_zero]; exact ⟨1, rfl⟩)
+
+@[simp]
+theorem quasispectrum.of_subsingleton {R A : Type*} [Field R] [NonUnitalRing A]
+    [Module R A] [Subsingleton A] (a : A) :
+    quasispectrum R a = {0} := by
+  rw [Subsingleton.elim a 0, quasispectrum_zero]
+
 /-- A version of `NonUnitalAlgHom.quasispectrum_apply_subset` which allows for `quasispectrum R`,
 where `R` is a *semi*ring, but `φ` must still function over a scalar ring `S`. In this case, we
 need `S` to be explicit. The primary use case is, for instance, `R := ℝ≥0` and `S := ℝ` or

Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

@@ -148,7 +148,7 @@ theorem gelfandTransform_isometry : Isometry (gelfandTransform ℂ A) := by
     self-adjoint, so also do their norms. Applying the C⋆-property of the norm and taking square
     roots shows that the norm is preserved. -/
   have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
-    unfold spectralRadius; rw [spectrum.gelfandTransform_eq]
+    simp only [spectrum.spectralRadius_eq_of_unital, spectrum.gelfandTransform_eq]
   rw [map_mul, (IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
     (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this
   simp only [ENNReal.coe_inj, CStarRing.nnnorm_star_mul_self, ← sq] at this

Mathlib/Analysis/CStarAlgebra/Hom.lean

@@ -68,7 +68,7 @@ lemma norm_map (φ : F) (hφ : Function.Injective φ) (a : A) : ‖φ a‖ = ‖
   calc ‖ψ (star a * a)‖ = (spectralRadius ℝ (ψ (star a * a))).toReal :=
       ha.map ψ |>.toReal_spectralRadius_eq_norm.symm
     _ = (spectralRadius ℝ (star a * a)).toReal := by
-      simp only [spectralRadius, ha.map_spectrum_real ψ hψ]
+      simp only [spectrum.spectralRadius_eq_of_unital, ha.map_spectrum_real ψ hψ]
     _ = ‖star a * a‖ := ha.toReal_spectralRadius_eq_norm
 
 /-- A non-unital star algebra monomorphism of complex C⋆-algebras is isometric. -/

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -278,7 +278,7 @@ lemma nnnorm_apply_le (φ : F) (a : A) : ‖φ a‖₊ ≤ ‖a‖₊ := by
     suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
       rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
         at this
-    exact iSup_le_iSup_of_subset (AlgHom.spectrum_apply_subset ψ s)
+    exact iSup_le_iSup_of_subset (NonUnitalAlgHom.quasispectrum_apply_subset ψ s)
   simpa [nnnorm_inr] using h (starLift (inrNonUnitalStarAlgHom ℂ B |>.comp (φ : A →⋆ₙₐ[ℂ] B))) a
 
 /-- A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive. -/

Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

@@ -182,9 +182,10 @@ theorem abs_rayleighQuotient_le_of_norm_mem_resolventSet [Nontrivial E]
 theorem spectralRadius_eq_nnnorm [CompleteSpace E] (hT : IsSelfAdjoint T) :
     spectralRadius 𝕜 T = ‖T‖₊ := by
   nontriviality E
-  apply le_antisymm (spectrum.spectralRadius_le_nnnorm T)
+  apply le_antisymm (spectralRadius_le_nnnorm T)
   suffices h : algebraMap ℝ 𝕜 ‖T‖ ∈ spectrum 𝕜 T ∨ algebraMap ℝ 𝕜 (-‖T‖) ∈ spectrum 𝕜 T by
-    rcases h with h | h <;> exact le_trans (by simp) (le_biSup _ h)
+    rcases h with h | h <;>
+      exact le_trans (by simp) (le_biSup _ (spectrum_subset_quasispectrum 𝕜 T h))
   simp_rw [spectrum, Set.mem_compl_iff, map_neg]
   by_contra! h
   obtain ⟨c, hc0, hc⟩ := T.abs_rayleighQuotient_le_of_norm_mem_resolventSet h.1 h.2

Mathlib/Analysis/InnerProductSpace/Spectrum.lean

@@ -433,7 +433,7 @@ variable [CompleteSpace E] {T : E →L[𝕜] E}
 theorem eq_zero_of_forall_hasEigenvalue_eq_zero (hT : IsCompactOperator T) (hT' : T.IsSymmetric) :
     (∀ μ, HasEigenvalue (T : End 𝕜 E) μ → μ = 0) ↔ T = 0 := by
   rw [← nnnorm_eq_zero, ← ENNReal.coe_eq_zero, ← T.spectralRadius_eq_nnnorm hT'.isSelfAdjoint,
-    spectralRadius, ← not_iff_not, ENNReal.iSup_eq_zero]
+    spectrum.spectralRadius_eq_of_unital, ← not_iff_not, ENNReal.iSup_eq_zero]
   push Not
   apply exists_congr
   simp +contextual [hT.hasEigenvalue_iff_mem_spectrum]