English
For f: ℂ → ℂ continuous on a closed disk and differentiable off a countable interior set, the integral ∮ f(z)/(z − w) dz equals 2πi f(w) for w in the disk.
Русский
Для f: ℂ → ℂ непрерывной на замкненном диске и дифференцируемой вне счётного множества внутри, интеграл ∮ f(z)/(z − w) dz равен 2πi f(w) при w внутри диска.
LaTeX
$$$\\oint_{z\\in C(c,R)} \\frac{f(z)}{z-w} \\, dz = 2 \\pi i \\cdot f(w)$$$
Lean4
/-- **Cauchy integral formula**: if `f : ℂ → ℂ` is continuous on a closed disc of radius `R` and is
complex differentiable at all but countably many points of its interior, then for any `w` in this
interior we have $\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$.
-/
theorem circleIntegral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {s : Set ℂ} (hs : s.Countable)
(hw : w ∈ ball c R) {f : ℂ → ℂ} (hc : ContinuousOn f (closedBall c R))
(hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) : (∮ z in C(c, R), f z / (z - w)) = 2 * π * I * f w := by
simpa only [smul_eq_mul, div_eq_inv_mul] using
circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
