English
An auxiliary lemma for the circle integral formula: under appropriate hypotheses, the integral ∮ (z − w)^{-1} f(z) dz equals (2πi) f(w).
Русский
Вспомогательная лемма для формулы окружного интеграла: при надлежащих предпосылках интеграл ∮ (z − w)^{-1} f(z) dz равен (2πi) f(w).
LaTeX
$$$\\oint_{z\\in C(c,R)} (z-w)^{-1} \\cdot f(z) \\, dz = (2 \\pi i) \\cdot f(w)$$$
Lean4
/-- **Cauchy integral formula**: if `f : ℂ → E` 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}(z-w)^{-1}f(z)\,dz=2πif(w)$.
-/
theorem circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : Set ℂ}
(hs : s.Countable) (hw : w ∈ ball c R) (hc : ContinuousOn f (closedBall c R))
(hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) : (∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
by
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd, smul_inv_smul₀]
simp [Real.pi_ne_zero, I_ne_zero]
