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
/-- If `f : ℂ → E` is complex differentiable on a closed disc of positive radius, then it is
analytic on the corresponding open disc, and the coefficients of the power series are given by
Cauchy integral formulas. See also
`Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable` for a version of this lemma with
weaker assumptions. -/
protected theorem _root_.DifferentiableOn.hasFPowerSeriesOnBall {R : ℝ≥0} {c : ℂ} {f : ℂ → E}
(hd : DifferentiableOn ℂ f (closedBall c R)) (hR : 0 < R) : HasFPowerSeriesOnBall f (cauchyPowerSeries f c R) c R :=
(hd.mono closure_ball_subset_closedBall).diffContOnCl.hasFPowerSeriesOnBall hR
