feat: upper hemicontinuity of the spectrum in Banach algebras (leanprover-community#33627)

If `A` is a (unital) Banach `𝕜`-algebra, then `spectrum 𝕜 : A → Set 𝕜` is upper hemicontinuous. Likewise, if `A` is a Banach `ℝ`-algebra, this holds for `spectrum ℝ≥0` as well. In addition, both of these results are true for non-unital Banach algebras replacing `spectrum` by `quasispectrum`.

This is useful for providing some more convenience lemmas establishing continuity of the continuous functional calculus in the operator variable.

- [ ] depends on: leanprover-community#33623
- [ ] depends on: leanprover-community#33624
- [ ] depends on: leanprover-community#33625
- [ ] depends on: leanprover-community#33626

Author: j-loreaux

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

@@ -13,6 +13,8 @@ public import Mathlib.Analysis.Normed.Ring.Units
 public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
 public import Mathlib.FieldTheory.IsAlgClosed.Spectrum
 public import Mathlib.Topology.Algebra.Module.CharacterSpace
+public import Mathlib.Topology.Semicontinuity.Hemicontinuity
+import Mathlib.Topology.MetricSpace.Sequences
 
 /-!
 # The spectrum of elements in a complete normed algebra
@@ -689,3 +691,62 @@ lemma compactSpace {R S A : Type*} [Semifield R] [Field S] [NonUnitalRing A]
   exact h.image ▸ h_cpct.image (map_continuous f)
 
 end QuasispectrumRestricts
+
+section UpperHemicontinuous
+
+open Filter Set Topology
+
+variable (𝕜 A)
+
+lemma upperHemicontinuous_spectrum [NormedField 𝕜] [ProperSpace 𝕜]
+    [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] :
+    UpperHemicontinuous (spectrum 𝕜 : A → Set 𝕜) := by
+  /- It suffices to use the sequential characterization of upper hemicontinuity.
+  Suppose that `a : ℕ → A` converges to `a₀`, `x : ℕ → 𝕜` converges to `x₀`, and for all `n`,
+  `x n ∈ spectrum 𝕜 (a n)`. -/
+  rw [upperHemicontinuous_iff]
+  refine fun a₀ ↦ .of_sequences
+    (isCompact_closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)).isSeqCompact ?_ <|
+    fun a ha x hx_mem x₀ hx↦ ?_
+  /- We must show that `spectrum 𝕜 (a n)` is eventually contained in some fixed compact set
+  (we've chosen `closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)`). This follows since the spectrum of any
+  `b` is bounded `‖b‖ * ‖1‖` and `a` converges to `a₀`.  -/
+  · filter_upwards [Metric.closedBall_mem_nhds a₀ zero_lt_one] with a ha
+    apply spectrum.subset_closedBall_norm_mul a |>.trans <| Metric.closedBall_subset_closedBall ?_
+    gcongr
+    apply norm_le_norm_add_norm_sub' a a₀ |>.trans
+    gcongr
+    simpa [dist_eq_norm] using ha
+  /- Finally, `x₀ ∈ spectrum 𝕜 a₀` since `algebraMap 𝕜 A x₀ - a₀` is not invertible, being itself
+  the limit of the non-invertible elements `algebraMap 𝕜 A (x n) - (a n)`. -/
+  · exact nonunits.isClosed.mem_of_tendsto
+      (continuous_algebraMap 𝕜 A |>.tendsto x₀ |>.comp hx |>.sub ha) <| .of_forall hx_mem
+
+/-- The map `a ↦ spectrum ℝ≥0 a` is upper hemicontinuous. -/
+theorem upperHemicontinuous_spectrum_nnreal [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] :
+    UpperHemicontinuous (spectrum ℝ≥0 : A → Set ℝ≥0) := by
+  obtain ⟨⟨h₁, -⟩, h₂⟩ : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := isometry_subtype_coe.isClosedEmbedding
+  exact upperHemicontinuous_spectrum ℝ A |>.isInducing_comp h₁ h₂
+
+open WithLp in
+/-- The map `a ↦ quasispectrum 𝕜 a` is upper hemicontinuous. -/
+theorem upperHemicontinuous_quasispectrum [NontriviallyNormedField 𝕜] [ProperSpace 𝕜]
+    [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A]
+    [CompleteSpace A] :
+    UpperHemicontinuous (quasispectrum 𝕜 : A → Set 𝕜) := by
+  convert upperHemicontinuous_spectrum 𝕜 (WithLp 1 (Unitization 𝕜 A)) |>.comp
+    unitization_isometry_inr.continuous
+  ext1 a
+  rw [Unitization.quasispectrum_eq_spectrum_inr,
+    ← AlgEquiv.spectrum_eq (unitizationAlgEquiv 𝕜 (𝕜 := 𝕜) (A := A) |>.symm)]
+  congr
+
+/-- The map `a ↦ quasispectrum ℝ≥0 a` is upper hemicontinuous. -/
+theorem upperHemicontinuous_quasispectrum_nnreal [NonUnitalNormedRing A]
+    [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [CompleteSpace A] :
+    UpperHemicontinuous (quasispectrum ℝ≥0 : A → Set ℝ≥0) := by
+  obtain ⟨⟨h₁, -⟩, h₂⟩ : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := isometry_subtype_coe.isClosedEmbedding
+  simpa [← NNReal.algebraMap_eq_coe] using
+    upperHemicontinuous_quasispectrum ℝ A |>.isInducing_comp h₁ h₂
+
+end UpperHemicontinuous