feat(Analysis/Normed/Algebra/SpectralNorm): extensions of absolute values

Mathlib.lean

@@ -2154,6 +2154,8 @@ public import Mathlib.Analysis.Normed.Algebra.GelfandFormula
 public import Mathlib.Analysis.Normed.Algebra.GelfandMazur
 public import Mathlib.Analysis.Normed.Algebra.MatrixExponential
 public import Mathlib.Analysis.Normed.Algebra.QuaternionExponential
+public import Mathlib.Analysis.Normed.Algebra.SpectralNorm
+public import Mathlib.Analysis.Normed.Algebra.SpectralRadiusLimit
 public import Mathlib.Analysis.Normed.Algebra.Spectrum
 public import Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
 public import Mathlib.Analysis.Normed.Algebra.Ultra
@@ -2294,6 +2296,7 @@ public import Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
 public import Mathlib.Analysis.Normed.Unbundled.FiniteExtension
 public import Mathlib.Analysis.Normed.Unbundled.InvariantExtension
 public import Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful
+public import Mathlib.Analysis.Normed.Unbundled.IsPowMulUnique
 public import Mathlib.Analysis.Normed.Unbundled.RingSeminorm
 public import Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
 public import Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 module
 
+public import Mathlib.Analysis.Normed.Algebra.SpectralRadiusLimit
 public import Mathlib.Analysis.Normed.Algebra.Spectrum
 public import Mathlib.Analysis.Calculus.Deriv.Basic
 public import Mathlib.Analysis.Normed.Operator.Mul
@@ -129,7 +130,7 @@ alias gelfand_formula := pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius
 /- This is the same as `pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius` but for `norm`
 instead of `nnnorm`. -/
 /-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
-`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖₊ ^ (1 / n)`. -/
+`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖ ^ (1 / n)`. -/
 theorem pow_norm_pow_one_div_tendsto_nhds_spectralRadius (a : A) :
     Tendsto (fun n : ℕ => ENNReal.ofReal (‖a ^ n‖ ^ (1 / n : ℝ))) atTop
       (𝓝 (spectralRadius ℂ a)) := by
@@ -138,6 +139,15 @@ theorem pow_norm_pow_one_div_tendsto_nhds_spectralRadius (a : A) :
   rw [← ofReal_rpow_of_nonneg (norm_nonneg _) _, ← coe_nnnorm, coe_nnreal_eq]
   simp
 
+/-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
+`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖ ^ (1 / n)`. -/
+theorem spectralRadius_eq_spectralRadiusLimit (a : A) :
+    spectralRadius ℂ a = ENNReal.ofReal (spectralRadiusLim a) := by
+  have h1 := pow_norm_pow_one_div_tendsto_nhds_spectralRadius a
+  simp_rw [one_div] at h1
+  have h2 := continuous_ofReal.continuousAt.tendsto.comp (tendsto_spectralRadiusLim a)
+  exact tendsto_nhds_unique h1 h2
+
 section Nontrivial
 
 variable [Nontrivial A]