English
If f is differentiable on a closed disk, then the circle integral ∮ (z − w)^{-1} f(z) dz equals (2πi) f(w) for w inside the disk.
Русский
Если f дифференцируема на замкнутом диске, то интеграл по окружности ∮ (z − w)^{-1} f(z) dz равен (2πi) f(w) при 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 a closed disc of radius
`R`, then for any `w` in its interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$. -/
theorem _root_.DifferentiableOn.circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ} {f : ℂ → E}
(hd : DifferentiableOn ℂ f (closedBall c R)) (hw : w ∈ ball c R) :
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
(hd.mono closure_ball_subset_closedBall).diffContOnCl.circleIntegral_sub_inv_smul hw
