feat(algebra/algebra/spectrum, analysis/normed_space/spectrum): prove…

… the spectrum of any element in a complex Banach algebra is nonempty (#12115)

This establishes that the spectrum of any element in a (nontrivial) complex Banach algebra is nonempty. The nontrivial assumption is necessary, as otherwise the only element is invertible. In addition, we establish some properties of the resolvent function; in particular, it tends to zero at infinity.

- [x] depends on: #12095 



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/algebra/spectrum.lean

@@ -44,13 +44,15 @@ section defs
 variables (R : Type u) {A : Type v}
 variables [comm_semiring R] [ring A] [algebra R A]
 
+local notation `↑ₐ` := algebra_map R A
+
 -- definition and basic properties
 
 /-- 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_set (a : A) : set R :=
-{ r : R | is_unit (algebra_map R A r - a) }
+{ r : R | is_unit (↑ₐr - a) }
 
 
 /-- Given a commutative ring `R` and an `R`-algebra `A`, the *spectrum* of `a : A`
@@ -66,23 +68,23 @@ variable {R}
     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
+ring.inverse (↑ₐr - a)
 
+/-- The unit `1 - r⁻¹ • a` constructed from `r • 1 - a` when the latter is a unit. -/
+@[simps]
+noncomputable def is_unit.sub_inv_smul {r : Rˣ} {s : R} {a : A}
+  (h : is_unit $ r • ↑ₐs  - a) : Aˣ :=
+{ val := ↑ₐs - r⁻¹ • a,
+  inv := r • ↑h.unit⁻¹,
+  val_inv := by rw [mul_smul_comm, ←smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_coe_inv],
+  inv_val := by rw [smul_mul_assoc, ←mul_smul_comm, smul_sub, smul_inv_smul, h.coe_inv_mul], }
 
 -- products of scalar units and algebra units
-
-
-lemma is_unit.smul_sub_iff_sub_inv_smul {R : Type u} {A : Type v}
-  [comm_ring R] [ring A] [algebra R A] {r : Rˣ} {a : A} :
+lemma is_unit.smul_sub_iff_sub_inv_smul {r : Rˣ} {a : A} :
   is_unit (r • 1 - a) ↔ is_unit (1 - r⁻¹ • a) :=
-begin
-  have a_eq : a = r•r⁻¹•a, by simp,
-  nth_rewrite 0 a_eq,
-  rw [←smul_sub,is_unit_smul_iff],
-end
+by rw [←@is_unit_smul_iff _ _ _ _ _ _ _ r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]
+
+end defs
 
 namespace spectrum
 open_locale polynomial
@@ -116,6 +118,34 @@ lemma resolvent_eq {a : A} {r : R} (h : r ∈ resolvent_set R a) :
   resolvent a r = ↑h.unit⁻¹ :=
 ring.inverse_unit h.unit
 
+lemma units_smul_resolvent {r : Rˣ} {s : R} {a : A} :
+  r • resolvent a (s : R) = resolvent (r⁻¹ • a) (r⁻¹ • s : R) :=
+begin
+  by_cases h : s ∈ spectrum R a,
+  { rw [mem_iff] at h,
+    simp only [resolvent, algebra.algebra_map_eq_smul_one] at *,
+    rw [smul_assoc, ←smul_sub],
+    have h' : ¬ is_unit (r⁻¹ • (s • 1 - a)),
+      from λ hu, h (by simpa only [smul_inv_smul] using is_unit.smul r hu),
+    simp only [ring.inverse_non_unit _ h, ring.inverse_non_unit _ h', smul_zero] },
+  { simp only [resolvent],
+    have h' : is_unit (r • (algebra_map R A (r⁻¹ • s)) - a),
+      { simpa [algebra.algebra_map_eq_smul_one, smul_assoc] using not_mem_iff.mp h },
+    rw [←h'.coe_sub_inv_smul, ←(not_mem_iff.mp h).unit_spec, ring.inverse_unit, ring.inverse_unit,
+      h'.coe_inv_sub_inv_smul],
+    simp only [algebra.algebra_map_eq_smul_one, smul_assoc, smul_inv_smul], },
+end
+
+lemma units_smul_resolvent_self {r : Rˣ} {a : A} :
+  r • resolvent a (r : R) = resolvent (r⁻¹ • a) (1 : R) :=
+by simpa only [units.smul_def, algebra.id.smul_eq_mul, units.inv_mul]
+  using @units_smul_resolvent _ _ _ _ _ r r a
+
+/-- The resolvent is a unit when the argument is in the resolvent set. -/
+lemma is_unit_resolvent {r : R} {a : A} :
+  r ∈ resolvent_set R a ↔ is_unit (resolvent a r) :=
+is_unit_ring_inverse.symm
+
 lemma inv_mem_resolvent_set {r : Rˣ} {a : Aˣ} (h : (r : R) ∈ resolvent_set R (a : A)) :
   (↑r⁻¹ : R) ∈ resolvent_set R (↑a⁻¹ : A) :=
 begin

src/analysis/normed_space/spectrum.lean

@@ -5,7 +5,7 @@ Authors: Jireh Loreaux
 -/
 import algebra.algebra.spectrum
 import analysis.special_functions.pow
-import analysis.complex.cauchy_integral
+import analysis.complex.liouville
 import analysis.analytic.radius_liminf
 /-!
 # The spectrum of elements in a complete normed algebra
@@ -27,6 +27,7 @@ This file contains the basic theory for the resolvent and spectrum of a Banach a
 * `spectrum.has_deriv_at_resolvent`: the resolvent function is differentiable on the resolvent set.
 * `spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius`: Gelfand's formula for the
   spectral radius in Banach algebras over `ℂ`.
+* `spectrum.nonempty`: the spectrum of any element in a complex Banach algebra is nonempty.
 
 
 ## TODO
@@ -123,7 +124,9 @@ end
 
 end spectrum_compact
 
-section resolvent_deriv
+section resolvent
+
+open filter asymptotics
 
 variables [nondiscrete_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A]
 
@@ -139,7 +142,40 @@ begin
   simpa [resolvent, sq, hk.unit_spec, ← ring.inverse_unit hk.unit] using H₁.comp_has_deriv_at k H₂,
 end
 
-end resolvent_deriv
+/- TODO: Once there is sufficient API for bornology, we should get a nice filter / asymptotics
+version of this, for example: `tendsto (resolvent a) (cobounded 𝕜) (𝓝 0)` or more specifically
+`is_O (resolvent a) (λ z, z⁻¹) (cobounded 𝕜)`. -/
+lemma norm_resolvent_le_forall (a : A) :
+  ∀ ε > 0, ∃ R > 0, ∀ z : 𝕜, R ≤ ∥z∥ → ∥resolvent a z∥ ≤ ε :=
+begin
+  obtain ⟨c, c_pos, hc⟩ := (@normed_ring.inverse_one_sub_norm A _ _).exists_pos,
+  rw [is_O_with_iff, eventually_iff, metric.mem_nhds_iff] at hc,
+  rcases hc with ⟨δ, δ_pos, hδ⟩,
+  simp only [cstar_ring.norm_one, mul_one] at hδ,
+  intros ε hε,
+  have ha₁ : 0 < ∥a∥ + 1 := lt_of_le_of_lt (norm_nonneg a) (lt_add_one _),
+  have min_pos : 0 < min (δ * (∥a∥ + 1)⁻¹) (ε * c⁻¹),
+    from lt_min (mul_pos δ_pos (inv_pos.mpr ha₁)) (mul_pos hε (inv_pos.mpr c_pos)),
+  refine ⟨(min (δ * (∥a∥ + 1)⁻¹) (ε * c⁻¹))⁻¹, inv_pos.mpr min_pos, (λ z hz, _)⟩,
+  have hnz : z ≠ 0 := norm_pos_iff.mp (lt_of_lt_of_le (inv_pos.mpr min_pos) hz),
+  replace hz := inv_le_of_inv_le min_pos hz,
+  rcases (⟨units.mk0 z hnz, units.coe_mk0 hnz⟩ : is_unit z) with ⟨z, rfl⟩,
+  have lt_δ : ∥z⁻¹ • a∥ < δ,
+  { rw [units.smul_def, norm_smul, units.coe_inv', norm_inv],
+    calc ∥(z : 𝕜)∥⁻¹ * ∥a∥ ≤ δ * (∥a∥ + 1)⁻¹ * ∥a∥
+        : mul_le_mul_of_nonneg_right (hz.trans (min_le_left _ _)) (norm_nonneg _)
+    ...                   < δ
+        : by { conv { rw mul_assoc, to_rhs, rw (mul_one δ).symm },
+               exact mul_lt_mul_of_pos_left
+                 ((inv_mul_lt_iff ha₁).mpr ((mul_one (∥a∥ + 1)).symm ▸ (lt_add_one _))) δ_pos } },
+  rw [←inv_smul_smul z (resolvent a (z : 𝕜)), units_smul_resolvent_self, resolvent,
+    algebra.algebra_map_eq_smul_one, one_smul, units.smul_def, norm_smul, units.coe_inv', norm_inv],
+  calc _ ≤ ε * c⁻¹ * c : mul_le_mul (hz.trans (min_le_right _ _)) (hδ (mem_ball_zero_iff.mpr lt_δ))
+                           (norm_nonneg _) (mul_pos hε (inv_pos.mpr c_pos)).le
+  ...    = _           : inv_mul_cancel_right₀ c_pos.ne.symm ε,
+end
+
+end resolvent
 
 section one_sub_smul
 
@@ -273,6 +309,43 @@ end
 
 end gelfand_formula
 
+/-- 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] [topological_space.second_countable_topology A]
+  (a : A) : (spectrum ℂ a).nonempty :=
+begin
+  /- Suppose `σ a = ∅`, then resolvent set is `ℂ`, any `(z • 1 - a)` is a unit, and `resolvent`
+  is differentiable on `ℂ`. -/
+  rw ←set.ne_empty_iff_nonempty,
+  by_contra h,
+  have H₀ : resolvent_set ℂ a = set.univ, by rwa [spectrum, set.compl_empty_iff] at h,
+  have H₁ : differentiable ℂ (λ z : ℂ, resolvent a z), from λ z,
+    (has_deriv_at_resolvent (H₀.symm ▸ set.mem_univ z : z ∈ resolvent_set ℂ a)).differentiable_at,
+  /- The norm of the resolvent is small for all sufficently large `z`, and by compactness and
+  continuity it is bounded on the complement of a large ball, thus uniformly bounded on `ℂ`.
+  By Liouville's theorem `λ z, resolvent a z` is constant -/
+  have H₂ := norm_resolvent_le_forall a,
+  have H₃ : ∀ z : ℂ, resolvent a z = resolvent a (0 : ℂ),
+  { refine λ z, H₁.apply_eq_apply_of_bounded (bounded_iff_exists_norm_le.mpr _) z 0,
+    rcases H₂ 1 zero_lt_one with ⟨R, R_pos, hR⟩,
+    rcases (proper_space.is_compact_closed_ball (0 : ℂ) R).exists_bound_of_continuous_on
+      H₁.continuous.continuous_on with ⟨C, hC⟩,
+    use max C 1,
+    rintros _ ⟨w, rfl⟩,
+    refine or.elim (em (∥w∥ ≤ R)) (λ hw, _) (λ hw, _),
+      { exact (hC w (mem_closed_ball_zero_iff.mpr hw)).trans (le_max_left _ _) },
+      { exact (hR w (not_le.mp hw).le).trans (le_max_right _ _), }, },
+  /- `resolvent a 0 = 0`, which is a contradition because it isn't a unit. -/
+  have H₅ : resolvent a (0 : ℂ) = 0,
+  { refine norm_eq_zero.mp (le_antisymm (le_of_forall_pos_le_add (λ ε hε, _)) (norm_nonneg _)),
+    rcases H₂ ε hε with ⟨R, R_pos, hR⟩,
+    simpa only [H₃ R] using (zero_add ε).symm.subst
+      (hR R (by exact_mod_cast (real.norm_of_nonneg R_pos.lt.le).symm.le)), },
+  /- `not_is_unit_zero` is where we need `nontrivial A`, it is unavoidable. -/
+  exact not_is_unit_zero (H₅.subst (is_unit_resolvent.mp
+    (mem_resolvent_set_iff.mp (H₀.symm ▸ set.mem_univ 0)))),
+end
+
 end spectrum
 
 namespace alg_hom