Theorems · Theorem · functional analysis

spectrum.differentiableOn_inverse_one_sub_smul

∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {r : NNReal},
  ↑r < (spectralRadius 𝕜 a)⁻¹ → DifferentiableOn 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)

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)⁻¹.

Defined in

Mathlib.Analysis.Normed.Algebra.GelfandFormula

Cited by

1 results in Mathlib

Foundations

Depth 186 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraCompleteSpace