English
Let f: C → E have a derivative f' on the circle S(c,R). If R ≥ 0 and f′(z) is the derivative for every z on the circle, then the contour integral of f′ around the circle is zero.
Русский
Пусть f: ℂ → E имеет производную f′ на окружности с центром c и радиусом R. Тогда интеграл по контуру окружности от f′(z) dz равен нулю.
LaTeX
$$$$\\displaystyle \\text{If } h_R:\\,0\\le R \\text{ and } \\forall z\\in S(c,R),\\ HasDerivWithinAt\\ f\\ (f'(z))\\ (S(c,R))\\ z, \\text{ then } \\oint_{|z-c|=R} f'(z)\\,dz = 0.$$$$
Lean4
/-- If `f' : ℂ → E` is a derivative of a complex differentiable function on the circle
`Metric.sphere c R`, then `∮ z in C(c, R), f' z = 0`. -/
theorem integral_eq_zero_of_hasDerivWithinAt [CompleteSpace E] {f f' : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R)
(h : ∀ z ∈ sphere c R, HasDerivWithinAt f (f' z) (sphere c R) z) : (∮ z in C(c, R), f' z) = 0 :=
integral_eq_zero_of_hasDerivWithinAt' <| (abs_of_nonneg hR).symm ▸ h
