English
Let a be an element of a normed algebra A over 𝕂 and k be in the resolvent set of a. The resolvent map R(k) = (kI - a)^{-1} is differentiable at k and its derivative is -R(k)^{2}. More precisely, d/dk R(k) = - (kI - a)^{-2}.
Русский
Пусть a ∈ A, и k принадлежит резольвентному множеству a. Резольвентная функция R(k) = (kI − a)^{-1} дифференцируема в точке k, производная равна -R(k)²; то есть dR/dk|_{k} = - (kI − a)^{-2}.
LaTeX
$$$\\frac{d}{dk} (kI - a)^{-1} = - (kI - a)^{-2}$ for $k \\in \\rho(a)$$$
Lean4
theorem hasDerivAt_resolvent [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {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₂
