feat(analysis/normed_space/spectrum and algebra/algebra/spectrum): pr…

…ove properties of spectrum in a Banach algebra (#10530)

Prove that the `spectrum` of an element in a Banach algebra is closed and bounded, hence compact when the scalar field is                               
proper. Compute the derivative of the `resolvent a` function in preparation for showing that the spectrum is nonempty when  the base field is ℂ. Define the `spectral_radius` and prove that it is bounded by the norm. Also rename the resolvent set to `resolvent_set` instead of `resolvent` so that it doesn't clash with the function name.

src/algebra/algebra/spectrum.lean

@@ -12,10 +12,12 @@ This theory will serve as the foundation for spectral theory in Banach algebras.
 
 ## Main definitions
 
-* `resolvent a : set R`: the resolvent set of an element `a : A` where
+* `resolvent_set a : set R`: the resolvent set of an element `a : A` where
   `A` is an  `R`-algebra.
 * `spectrum a : set R`: the spectrum of an element `a : A` where
   `A` is an  `R`-algebra.
+* `resolvent : R → A`: the resolvent function is `λ r, ring.inverse (↑ₐr - a)`, and hence
+  when `r ∈ resolvent R A`, it is actually the inverse of the unit `(↑ₐr - a)`.
 
 ## Main statements
 
@@ -43,20 +45,27 @@ variables [comm_ring R] [ring A] [algebra R A]
 
 -- definition and basic properties
 
-/-- Given a commutative ring `R` and an `R`-algebra `A`, the *resolvent* of `a : A`
+/-- Given a commutative ring `R` and an `R`-algebra `A`, the *resolvent set* of `a : A`
 is the `set R` consisting of those `r : R` for which `r•1 - a` is a unit of the
 algebra `A`.  -/
-def resolvent (a : A) : set R :=
+def resolvent_set (a : A) : set R :=
 { r : R | is_unit (algebra_map R A r - a) }
 
 
 /-- Given a commutative ring `R` and an `R`-algebra `A`, the *spectrum* of `a : A`
 is the `set R` consisting of those `r : R` for which `r•1 - a` is not a unit of the
 algebra `A`.
 
-The spectrum is simply the complement of the resolvent.  -/
+The spectrum is simply the complement of the resolvent set.  -/
 def spectrum (a : A) : set R :=
-(resolvent R a)ᶜ
+(resolvent_set R a)ᶜ
+
+variable {R}
+/-- Given an `a : A` where `A` is an `R`-algebra, the *resolvent* is
+    a map `R → A` which sends `r : R` to `(algebra_map R A r - a)⁻¹` when
+    `r ∈ resolvent R A` and `0` when `r ∈ spectrum R A`. -/
+noncomputable def resolvent (a : A) (r : R) : A :=
+ring.inverse (algebra_map R A r - a)
 
 end defs
 
@@ -88,20 +97,24 @@ lemma not_mem_iff {r : R} {a : A} :
   r ∉ σ a ↔ is_unit (↑ₐr - a) :=
 by { apply not_iff_not.mp, simp [set.not_not_mem, mem_iff] }
 
-lemma mem_resolvent_of_left_right_inverse {r : R} {a b c : A}
+lemma mem_resolvent_set_of_left_right_inverse {r : R} {a b c : A}
   (h₁ : (↑ₐr - a) * b = 1) (h₂ : c * (↑ₐr - a) = 1) :
-  r ∈ resolvent R a :=
+  r ∈ resolvent_set R a :=
 units.is_unit ⟨↑ₐr - a, b, h₁, by rwa ←left_inv_eq_right_inv h₂ h₁⟩
 
-lemma mem_resolvent_iff {r : R} {a : A} :
-  r ∈ resolvent R a ↔ is_unit (↑ₐr - a) :=
+lemma mem_resolvent_set_iff {r : R} {a : A} :
+  r ∈ resolvent_set R a ↔ is_unit (↑ₐr - a) :=
 iff.rfl
 
+lemma resolvent_eq {a : A} {r : R} (h : r ∈ resolvent_set R a) :
+  resolvent a r = ↑h.unit⁻¹ :=
+ring.inverse_unit h.unit
+
 lemma add_mem_iff {a : A} {r s : R} :
   r ∈ σ a ↔ r + s ∈ σ (↑ₐs + a) :=
 begin
   apply not_iff_not.mpr,
-  simp only [mem_resolvent_iff],
+  simp only [mem_resolvent_set_iff],
   have h_eq : ↑ₐ(r+s) - (↑ₐs + a) = ↑ₐr - a,
     { simp, noncomm_ring },
   rw h_eq,
@@ -111,7 +124,7 @@ lemma smul_mem_smul_iff {a : A} {s : R} {r : units R} :
   r • s ∈ σ (r • a) ↔ s ∈ σ a :=
 begin
   apply not_iff_not.mpr,
-  simp only [mem_resolvent_iff, algebra.algebra_map_eq_smul_one],
+  simp only [mem_resolvent_set_iff, algebra.algebra_map_eq_smul_one],
   have h_eq : (r•s)•(1 : A) = r•s•1, by simp,
   rw [h_eq,←smul_sub,is_unit_smul_iff],
 end
@@ -140,7 +153,7 @@ theorem unit_mem_mul_iff_mem_swap_mul {a b : A} {r : units R} :
   ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a) :=
 begin
   apply not_iff_not.mpr,
-  simp only [mem_resolvent_iff, algebra.algebra_map_eq_smul_one],
+  simp only [mem_resolvent_set_iff, algebra.algebra_map_eq_smul_one],
   have coe_smul_eq : ↑r•1 = r•(1 : A), from rfl,
   rw coe_smul_eq,
   simp only [is_unit.smul_sub_iff_sub_inv_smul],

src/analysis/normed_space/spectrum.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2021 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import algebra.algebra.spectrum
+import analysis.calculus.deriv
+/-!
+# The spectrum of elements in a complete normed algebra
+
+This file contains the basic theory for the resolvent and spectrum of a Banach algebra.
+
+## Main definitions
+
+* `spectral_radius : ℝ≥0∞`: supremum of `∥k∥₊` for all `k ∈ spectrum 𝕜 a`
+
+## Main statements
+
+* `spectrum.is_open_resolvent_set`: the resolvent set is open.
+* `spectrum.is_closed`: the spectrum is closed.
+* `spectrum.subset_closed_ball_norm`: the spectrum is a subset of closed disk of radius
+  equal to the norm.
+* `spectrum.is_compact`: the spectrum is compact.
+* `spectrum.spectral_radius_le_nnnorm`: the spectral radius is bounded above by the norm.
+* `spectrum.has_deriv_at_resolvent`: the resolvent function is differentiable on the resolvent set.
+
+
+## TODO
+
+* after we have Liouville's theorem, prove that the spectrum is nonempty when the
+  scalar field is ℂ.
+* compute all derivatives of `resolvent a`.
+
+-/
+
+open_locale ennreal
+
+/-- 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
+    case, `spectral_radius a = 0`.  It is also possible that `spectrum 𝕜 a` be unbounded (though
+    not for Banach algebras, see `spectrum.is_bounded`, below).  In this case,
+    `spectral_radius a = ∞`. -/
+noncomputable def spectral_radius (𝕜 : Type*) {A : Type*} [normed_field 𝕜] [ring A]
+  [algebra 𝕜 A] (a : A) : ℝ≥0∞ :=
+⨆ k ∈ spectrum 𝕜 a, ∥k∥₊
+
+namespace spectrum
+
+section spectrum_compact
+
+variables {𝕜 : Type*} {A : Type*}
+variables [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
+
+local notation `σ` := spectrum 𝕜
+local notation `ρ` := resolvent_set 𝕜
+local notation `↑ₐ` := algebra_map 𝕜 A
+
+lemma is_open_resolvent_set (a : A) : is_open (ρ a) :=
+units.is_open.preimage ((algebra_map_isometry 𝕜 A).continuous.sub continuous_const)
+
+lemma is_closed (a : A) : is_closed (σ a) :=
+(is_open_resolvent_set a).is_closed_compl
+
+lemma mem_resolvent_of_norm_lt {a : A} {k : 𝕜} (h : ∥a∥ < ∥k∥) :
+  k ∈ ρ a :=
+begin
+  rw [resolvent_set, set.mem_set_of_eq, algebra.algebra_map_eq_smul_one],
+  have hk : k ≠ 0 := ne_zero_of_norm_pos (by linarith [norm_nonneg a]),
+  let ku := units.map (↑ₐ).to_monoid_hom (units.mk0 k hk),
+  have hku : ∥-a∥ < ∥(↑ku⁻¹:A)∥⁻¹ := by simpa [ku, algebra_map_isometry] using h,
+  simpa [ku, sub_eq_add_neg, algebra.algebra_map_eq_smul_one] using (ku.add (-a) hku).is_unit,
+end
+
+lemma norm_le_norm_of_mem {a : A} {k : 𝕜} (hk : k ∈ σ a) :
+  ∥k∥ ≤ ∥a∥ :=
+le_of_not_lt $ mt mem_resolvent_of_norm_lt hk
+
+lemma subset_closed_ball_norm (a : A) :
+  σ a ⊆ metric.closed_ball (0 : 𝕜) (∥a∥) :=
+λ k hk, by simp [norm_le_norm_of_mem hk]
+
+lemma is_bounded (a : A) : metric.bounded (σ a) :=
+(metric.bounded_iff_subset_ball 0).mpr ⟨∥a∥, subset_closed_ball_norm a⟩
+
+theorem is_compact [proper_space 𝕜] (a : A) : is_compact (σ a) :=
+metric.is_compact_of_is_closed_bounded (is_closed a) (is_bounded a)
+
+theorem spectral_radius_le_nnnorm (a : A) :
+  spectral_radius 𝕜 a ≤ ∥a∥₊ :=
+begin
+  suffices h : ∀ k ∈ σ a, (∥k∥₊ : ℝ≥0∞) ≤ ∥a∥₊,
+  { exact bsupr_le h, },
+  { by_cases ha : (σ a).nonempty,
+    { intros _ hk,
+      exact_mod_cast norm_le_norm_of_mem hk },
+    { rw set.not_nonempty_iff_eq_empty at ha,
+      simp [ha, set.ball_empty_iff] } }
+end
+
+end spectrum_compact
+
+section resolvent_deriv
+
+variables {𝕜 : Type*} {A : Type*}
+variables [nondiscrete_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
+
+local notation `ρ` := resolvent_set 𝕜
+local notation `↑ₐ` := algebra_map 𝕜 A
+
+theorem has_deriv_at_resolvent {a : A} {k : 𝕜} (hk : k ∈ ρ a) :
+  has_deriv_at (resolvent a) (-(resolvent a k) ^ 2) k :=
+begin
+  have H₁ : has_fderiv_at ring.inverse _ (↑ₐk - a) := has_fderiv_at_ring_inverse hk.unit,
+  have H₂ : has_deriv_at (λ k, ↑ₐk - a) 1 k,
+  { simpa using (algebra.linear_map 𝕜 A).has_deriv_at.sub_const a },
+  simpa [resolvent, sq, hk.unit_spec, ← ring.inverse_unit hk.unit] using H₁.comp_has_deriv_at k H₂,
+end
+
+end resolvent_deriv
+
+end spectrum