feat(analysis/normed_space/spectrum): lemmas about spectral radius, s…

…pectral mapping and `alg_hom_class` maps into the base field (#17178)

- [x] depends on: #17156

src/analysis/normed_space/spectrum.lean

@@ -7,6 +7,7 @@ import algebra.algebra.spectrum
 import analysis.special_functions.pow
 import analysis.special_functions.exponential
 import analysis.complex.liouville
+import analysis.complex.polynomial
 import analysis.analytic.radius_liminf
 import topology.algebra.module.character_space
 /-!
@@ -41,7 +42,7 @@ This file contains the basic theory for the resolvent and spectrum of a Banach a
 
 -/
 
-open_locale ennreal
+open_locale ennreal nnreal
 
 /-- The *spectral radius* is the supremum of the `nnnorm` (`∥⬝∥₊`) of elements in the spectrum,
     coerced into an element of `ℝ≥0∞`. Note that it is possible for `spectrum 𝕜 a = ∅`. In this
@@ -129,6 +130,20 @@ theorem spectral_radius_le_nnnorm [norm_one_class A] (a : A) :
   spectral_radius 𝕜 a ≤ ∥a∥₊ :=
 by { refine supr₂_le (λ k hk, _), exact_mod_cast norm_le_norm_of_mem hk }
 
+lemma exists_nnnorm_eq_spectral_radius_of_nonempty [proper_space 𝕜] {a : A} (ha : (σ a).nonempty) :
+  ∃ k ∈ σ a, (∥k∥₊ : ℝ≥0∞) = spectral_radius 𝕜 a :=
+begin
+  obtain ⟨k, hk, h⟩ := (spectrum.is_compact a).exists_forall_ge ha continuous_nnnorm.continuous_on,
+  exact ⟨k, hk, le_antisymm (le_supr₂ k hk) (supr₂_le $ by exact_mod_cast h)⟩,
+end
+
+lemma spectral_radius_lt_of_forall_lt_of_nonempty [proper_space 𝕜] {a : A}
+  (ha : (σ a).nonempty) {r : ℝ≥0} (hr : ∀ k ∈ σ a, ∥k∥₊ < r) :
+  spectral_radius 𝕜 a < r :=
+Sup_image.symm.trans_lt $ ((spectrum.is_compact a).Sup_lt_iff_of_continuous ha
+  (ennreal.continuous_coe.comp continuous_nnnorm).continuous_on (r : ℝ≥0∞)).mpr
+  (by exact_mod_cast hr)
+
 open ennreal polynomial
 
 variable (𝕜)
@@ -351,10 +366,12 @@ end
 
 end gelfand_formula
 
+section nonempty_spectrum
+
+variables [normed_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A] (a : A)
+
 /-- In a (nontrivial) complex Banach algebra, every element has nonempty spectrum. -/
-theorem nonempty {A : Type*} [normed_ring A] [normed_algebra ℂ A] [complete_space A]
-  [nontrivial A]
-  (a : A) : (spectrum ℂ a).nonempty :=
+protected theorem nonempty : (spectrum ℂ a).nonempty :=
 begin
   /- Suppose `σ a = ∅`, then resolvent set is `ℂ`, any `(z • 1 - a)` is a unit, and `resolvent`
   is differentiable on `ℂ`. -/
@@ -388,6 +405,32 @@ begin
     (mem_resolvent_set_iff.mp (H₀.symm ▸ set.mem_univ 0)))),
 end
 
+/-- In a complex Banach algebra, the spectral radius is always attained by some element of the
+spectrum. -/
+lemma exists_nnnorm_eq_spectral_radius : ∃ z ∈ spectrum ℂ a, (∥z∥₊ : ℝ≥0∞) = spectral_radius ℂ a :=
+exists_nnnorm_eq_spectral_radius_of_nonempty (spectrum.nonempty a)
+
+/-- In a complex Banach algebra, if every element of the spectrum has norm strictly less than
+`r : ℝ≥0`, then the spectral radius is also strictly less than `r`. -/
+lemma spectral_radius_lt_of_forall_lt {r : ℝ≥0} (hr : ∀ z ∈ spectrum ℂ a, ∥z∥₊ < r) :
+  spectral_radius ℂ a < r :=
+spectral_radius_lt_of_forall_lt_of_nonempty (spectrum.nonempty a) hr
+
+open_locale polynomial
+open polynomial
+
+/-- The **spectral mapping theorem** for polynomials in a Banach algebra over `ℂ`. -/
+lemma map_polynomial_aeval (p : ℂ[X]) :
+  spectrum ℂ (aeval a p) = (λ k, eval k p) '' (spectrum ℂ a) :=
+map_polynomial_aeval_of_nonempty a p (spectrum.nonempty a)
+
+/-- A specialization of the spectral mapping theorem for polynomials in a Banach algebra over `ℂ`
+to monic monomials. -/
+protected lemma map_pow (n : ℕ) : spectrum ℂ (a ^ n) = (λ x, x ^ n) '' (spectrum ℂ a) :=
+by simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval a (X ^ n)
+
+end nonempty_spectrum
+
 section gelfand_mazur_isomorphism
 
 variables [normed_ring A] [normed_algebra ℂ A] (hA : ∀ {a : A}, is_unit a ↔ a ≠ 0)
@@ -462,12 +505,13 @@ end spectrum
 namespace alg_hom
 
 section normed_field
-variables [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
+variables {F : Type*} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
 local notation `↑ₐ` := algebra_map 𝕜 A
 
 /-- An algebra homomorphism into the base field, as a continuous linear map (since it is
-automatically bounded). -/
-instance : continuous_linear_map_class (A →ₐ[𝕜] 𝕜) 𝕜 A 𝕜 :=
+automatically bounded). See note [lower instance priority] -/
+@[priority 100]
+instance [alg_hom_class F 𝕜 A 𝕜] : continuous_linear_map_class F 𝕜 A 𝕜 :=
 { map_continuous := λ φ, add_monoid_hom_class.continuous_of_bound φ ∥(1 : A)∥ $
     λ a, (mul_comm ∥a∥ ∥(1 : A)∥) ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ _),
   .. alg_hom_class.linear_map_class }
@@ -480,6 +524,13 @@ def to_continuous_linear_map (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
 @[simp] lemma coe_to_continuous_linear_map (φ : A →ₐ[𝕜] 𝕜) :
   ⇑φ.to_continuous_linear_map = φ := rfl
 
+lemma norm_apply_le_self_mul_norm_one [alg_hom_class F 𝕜 A 𝕜] (f : F) (a : A) :
+  ∥f a∥ ≤ ∥a∥ * ∥(1 : A)∥ :=
+spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum f _)
+
+lemma norm_apply_le_self [norm_one_class A] [alg_hom_class F 𝕜 A 𝕜] (f : F) (a : A) : ∥f a∥ ≤ ∥a∥ :=
+spectrum.norm_le_norm_of_mem (apply_mem_spectrum f _)
+
 end normed_field
 
 section nontrivially_normed_field

src/analysis/normed_space/star/spectrum.lean

@@ -186,6 +186,18 @@ noncomputable instance : star_hom_class F A ℂ :=
 /-- This is not an instance to avoid type class inference loops. See
 `weak_dual.complex.star_hom_class`. -/
 noncomputable def _root_.alg_hom_class.star_alg_hom_class : star_alg_hom_class F ℂ A ℂ :=
-{ .. hF, .. weak_dual.complex.star_hom_class }
+{ coe := λ f, f,
+  .. weak_dual.complex.star_hom_class,
+  .. hF }
+
+omit hF
+
+namespace character_space
+
+noncomputable instance : star_alg_hom_class (character_space ℂ A) ℂ A ℂ :=
+{ coe := λ f, f,
+  .. alg_hom_class.star_alg_hom_class }
+
+end character_space
 
 end weak_dual