English
On an open set, for small radii, the circle derivative equals the standard derivative.
Русский
На открытом множестве при достаточном малом радиусе окружной производной совпадает с обычной производной.
LaTeX
$$$\\text{cderiv } r f z = \\text{deriv } f z\\quad\\text{when } z\\in U, r>0$$$
Lean4
/-- A circle integral which coincides with `deriv f z` whenever one can apply the Cauchy formula for
the derivative. It is useful in the proof that locally uniform limits of holomorphic functions are
holomorphic, because it depends continuously on `f` for the uniform topology. -/
noncomputable def cderiv (r : ℝ) (f : ℂ → E) (z : ℂ) : E :=
(2 * π * I : ℂ)⁻¹ • ∮ w in C(z, r), ((w - z) ^ 2)⁻¹ • f w
