English
If f is continuous on a closed disk of radius R about c and is differentiable on all but a countable set inside, then the contour integral of (z − c)^{-1} f(z) around the circle |z − c| = R equals (2πi) f(c).
Русский
Пусть f непрерывна на замкнутом диске радиуса R вокруг c и дифференцируема на всей внутренности кроме счётного множества; тогда интеграл ∮ (z − c)^{-1} f(z) dz по окружности |z − c| = R равен (2πi) f(c).
LaTeX
$$$\\oint_{|z-c|=R} (z-c)^{-1} \\cdot f(z) \\, dz = (2 \\pi i) \\cdot f(c)$$$
Lean4
/-- **Cauchy integral formula** for the value at the center of a disc. If `f : ℂ → E` is continuous on a
closed disc of radius `R` and center `c`, and is complex differentiable at all but countably many
points of its interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to
`2πi • f c`.
-/
theorem circleIntegral_sub_center_inv_smul_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), (z - c)⁻¹ • f z) = (2 * π * I) • f c :=
circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto h0 hs (hc.mono diff_subset)
(fun z hz => hd z ⟨hz.1.1, hz.2⟩) (hc.continuousAt <| closedBall_mem_nhds _ h0).continuousWithinAt
