English
In a Banach algebra, for a given a and a radius r with r smaller than the reciprocal of the spectral radius, the map z ↦ (1 - z a)^{-1} is differentiable on the closed ball of radius r around 0.
Русский
В банаховом алгебре для данного a и радиуса r, если r меньше оборота спектрального радиуса, отображение z ↦ (1 - z a)^{-1} дифференцируемо на замкнутом шаре радиуса r вокруг 0.
LaTeX
$$$\\text{DifferentiableOn}_{\\mathbb{K}} \\ big( z \\mapsto (1 - z a)^{-1} \\big) (\\overline{B}(0,r))$ under $ (r : \\mathbb{R}_{\\ge 0}) < (\\rho(a))^{-1}$$$
Lean4
/-- 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)⁻¹`. -/
theorem differentiableOn_inverse_one_sub_smul [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A]
[CompleteSpace A] {a : A} {r : ℝ≥0} (hr : (r : ℝ≥0∞) < (spectralRadius 𝕜 a)⁻¹) :
DifferentiableOn 𝕜 (fun z : 𝕜 => Ring.inverse (1 - z • a)) (Metric.closedBall 0 r) :=
by
intro z z_mem
apply DifferentiableAt.differentiableWithinAt
have hu : IsUnit (1 - z • a) :=
by
refine isUnit_one_sub_smul_of_lt_inv_radius (lt_of_le_of_lt (coe_mono ?_) hr)
simpa only [norm_toNNReal, Real.toNNReal_coe] using Real.toNNReal_mono (mem_closedBall_zero_iff.mp z_mem)
have H₁ : Differentiable 𝕜 fun w : 𝕜 => 1 - w • a := (differentiable_id.smul_const a).const_sub 1
exact DifferentiableAt.comp z (differentiableAt_inverse hu) H₁.differentiableAt
