English
Let c ∈ ℂ and 0 < r ≤ R. If f: ℂ → E is countably differentiable off a set and is continuous on the closed set obtained by removing a disk of radius r from the disk of radius R, then the integrals of (z − c)^{-1} f(z) over the two circles |z − c| = R and |z − c| = r coincide.
Русский
Пусть c ∈ ℂ и 0 < r ≤ R. Пусть f: ℂ → E непрерывна на замкнутом множестве, получаемом вычитанием круга радиуса r из круга радиуса R, и разностронно по содержимому внутри есть счётное множество, тогда интегралы ∮ (z − c)^{-1} f(z) dz по окружностям |z − c| = R и |z − c| = r совпадают.
LaTeX
$$$\\oint_{|z-c|=R} (z-c)^{-1} \\cdot f(z) \\, dz \;=\\; \\oint_{|z-c|=r} (z-c)^{-1} \\cdot f(z) \\, dz$$$
Lean4
/-- **Cauchy-Goursat theorem** for an annulus. If `f : ℂ → E` is continuous on the closed annulus
`r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`, and is complex differentiable at all but countably many points of
its interior, then the integrals of `f` over the circles `‖z - c‖ = r` and `‖z - c‖ = R` are equal
to each other. -/
theorem circleIntegral_eq_of_differentiable_on_annulus_off_countable {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R)
{f : ℂ → E} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (closedBall c R \ ball c r))
(hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z) :
(∮ z in C(c, R), f z) = ∮ z in C(c, r), f z :=
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
_ = ∮ z in C(c, r), (z - c)⁻¹ • (z - c) • f z :=
(circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable h0 hle hs
((continuousOn_id.sub continuousOn_const).smul hc) fun z hz => (differentiableAt_id.sub_const _).smul (hd z hz))
_ = ∮ z in C(c, r), f z := circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _
