English
Let f be continuous on a closed disk of radius R about c and differentiable at all interior points except a countable set. Then the contour integral of f around the circle |z − c| = R is zero.
Русский
Пусть f непрерывна на замкнутом диске радиуса R вокруг c и дифференцируема во всех внутренних точках кроме счётного множества. Тогда интеграл по контуру окружности |z − c| = R от f(z) dz равен нулю.
LaTeX
$$$\\oint_{|z-c|=R} f(z) \\, dz = 0$$$
Lean4
/-- **Cauchy-Goursat theorem** for a disk: if `f : ℂ → E` is continuous on a closed disk
`{z | ‖z - c‖ ≤ R}` and is complex differentiable at all but countably many points of its interior,
then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero. -/
theorem circleIntegral_eq_zero_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E} {c : ℂ} {s : Set ℂ}
(hs : s.Countable) (hc : ContinuousOn f (closedBall c R)) (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
(∮ z in C(c, R), f z) = 0 := by
wlog hE : CompleteSpace E generalizing
· simp [circleIntegral, intervalIntegral, integral, hE]
rcases h0.eq_or_lt with (rfl | h0); · apply circleIntegral.integral_radius_zero
calc
(∮ z in C(c, R), f z) = ∮ z in C(c, R), (z - c)⁻¹ • (z - c) • f z :=
(circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm
_ = (2 * ↑π * I : ℂ) • (c - c) • f c :=
(circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable h0 hs
((continuousOn_id.sub continuousOn_const).smul hc) fun z hz => (differentiableAt_id.sub_const _).smul (hd z hz))
_ = 0 := by rw [sub_self, zero_smul, smul_zero]
