feat(Analysis): add resolvent derivatives in the algebra component (leanprover-community#37172)

I would take suggestions for better names.

Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>

Author: DavidLedvinka

Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.Normed.Algebra.Spectrum
 public import Mathlib.Analysis.Calculus.Deriv.Basic
-import Mathlib.Analysis.Complex.Liouville
+public import Mathlib.Analysis.Normed.Operator.Mul
 import Mathlib.Analysis.Complex.Polynomial.Basic
 import Mathlib.Analysis.Analytic.RadiusLiminf
 
@@ -20,7 +20,8 @@ complex Banach algebra has nonempty spectrum.
 
 ## Main results
 
-* `spectrum.hasDerivAt_resolvent`: the resolvent function is differentiable on the resolvent set.
+* `spectrum.hasDerivAt_resolvent_const_left`: the resolvent function is differentiable on the
+  resolvent set.
 * `spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius`: 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.
@@ -45,15 +46,38 @@ open Filter ENNReal
 
 namespace spectrum
 
-theorem hasDerivAt_resolvent [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A]
-    [CompleteSpace A] {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a) :
+section NonTriviallyNormedField
+
+variable [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A]
+
+theorem hasDerivAt_resolvent_const_left {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a) :
     HasDerivAt (resolvent a) (-resolvent a k ^ 2) k := by
   have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
     hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
   have H₂ : HasDerivAt (fun k => algebraMap 𝕜 A k - a) 1 k := by
     simpa using (Algebra.linearMap 𝕜 A).hasDerivAt.sub_const a
   simpa [resolvent, sq, hk.unit_spec, ← Ring.inverse_unit hk.unit] using H₁.comp_hasDerivAt k H₂
 
+@[deprecated  (since := "2026-03-26")]
+alias hasDerivAt_resolvent := hasDerivAt_resolvent_const_left
+
+theorem hasFDerivAt_resolvent {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a) :
+    HasFDerivAt (resolvent · k)
+      (((ContinuousLinearMap.mulLeftRight 𝕜 A) (resolvent a k)) (resolvent a k)) a := by
+  have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
+    hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
+  have H₂ : HasFDerivAt (fun a => algebraMap 𝕜 A k - a) (- .id 𝕜 A) a := by
+    simpa using (hasFDerivAt_const _ _).sub (hasFDerivAt_id (𝕜 := 𝕜) _)
+  simpa [resolvent_eq hk] using H₁.comp a H₂
+
+end NonTriviallyNormedField
+
+theorem hasDerivAt_resolvent_const_right [NontriviallyNormedField 𝕜] [NontriviallyNormedField A]
+    [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a) :
+    HasDerivAt (resolvent · k) (resolvent a k ^ 2) a := by
+  convert hasFDerivAt_resolvent (𝕜 := A) hk |>.hasDerivAt
+  simp [resolvent, pow_two]
+
 open ENNReal in
 /-- In a Banach algebra `A` over `𝕜`, for `a : A` the function `fun z ↦ (1 - z • a)⁻¹` is
 differentiable on any closed ball centered at zero of radius `r < (spectralRadius 𝕜 a)⁻¹`. -/
@@ -125,7 +149,8 @@ protected theorem nonempty (a : A) : (spectrum ℂ a).Nonempty := by
   by_contra! h
   have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h
   have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
-    (hasDerivAt_resolvent (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)).differentiableAt
+    hasDerivAt_resolvent_const_left (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)
+      |>.differentiableAt
   /- Since `resolvent a` tends to zero at infinity, by Liouville's theorem `resolvent a = 0`,
   which contradicts that `resolvent a z` is invertible. -/
   have H₃ := H₁.apply_eq_of_tendsto_cocompact 0 <| by