English
If f is differentiable on a closed disk and w is inside the disk, then the circle integral of (z − w)^{-1} f(z) equals (2πi) f(w).
Русский
Если 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 complex differentiable on an open disc and is
continuous on its closure, then for any `w` in this open ball we have
$\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$. -/
theorem _root_.DiffContOnCl.circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ} {f : ℂ → E} (h : DiffContOnCl ℂ f (ball c R))
(hw : w ∈ ball c R) : (∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
circleIntegral_sub_inv_smul_of_differentiable_on_off_countable countable_empty hw h.continuousOn_ball fun _x hx =>
h.differentiableAt isOpen_ball hx.1
