English
If f′ is a derivative inside the circle of a complex-differentiable function, then its circle integral is zero.
Русский
Если f′ является производной внутри круга для комплексной дифференцируемой функции, то её круговой интеграл равен нулю.
LaTeX
$$$\\text{If } \\forall z \\in \\mathrm{sphere}\\;c|R|,\\ HasDerivWithinAt f (f'(z))\\;\\text{ then } \\oint z in C(c,R), f'(z) = 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 : ℝ}
(h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z) : (∮ z in C(c, R), f' z) = 0 :=
by
by_cases hi : CircleIntegrable f' c R
· rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]
refine intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => ?_) hi.out
exact
(h _ (circleMap_mem_sphere' _ _ _)).scomp_hasDerivAt θ (differentiable_circleMap _ _ _).hasDerivAt
(circleMap_mem_sphere' _ _)
· exact integral_undef hi
