English
If h is differentiable at x and h(x) is a unit, then the map x ↦ h(x)^{-1} is differentiable at x with derivative given by the product rule for inverses, i.e., D(h^{-1})(x) = - h(x)^{-1} (Dh)(x) h(x)^{-1}. In particular, for units x, fderiv_inverse gives the derivative of Ring.inverse at x.
Русский
Если функция h дифференцируема в точке x и h(x) является единицей, то отображение x ↦ h(x)^{-1} дифференцируемо в x; производная равна - h(x)^{-1} (Dh)(x) h(x)^{-1}. В частности, для единиц fderiv_inverse даёт производную Ring.inverse в x.
LaTeX
$$$\text{If } h: E \to R$, DifferentiableAt 𝕜 h x and IsUnit (h x), then HasFDerivAt (Ring.inverse ∘ h) at x equals -h(x)^{-1} Dh(x) h(x)^{-1}.$$$
Lean4
/-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion
operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`.
TODO (low prio): prove a version without assumption `[HasSummableGeomSeries R]` but within the set
of units. -/
@[fun_prop]
theorem hasFDerivAt_ringInverse (x : Rˣ) : HasFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
(inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)
by simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this
