English
If f is continuous on a disk and differentiable inside, then (1/(2πi)) ∮ (z − w)^{-1} f(z) dz = f(w) for w inside.
Русский
Если f непрерывна на диске и дифференцируема внутри, то (1/(2πi)) ∮ (z − w)^{-1} f(z) dz = f(w) для w внутри.
LaTeX
$$$\\frac{1}{2 \\pi i} \\oint_{|z-c|=R} (z-w)^{-1} \\cdot f(z) \\, dz = f(w)$$$
Lean4
/-- If `f : ℂ → E` is complex differentiable on an open disc of positive radius and is continuous
on its closure, then it is analytic on the open disc with coefficients of the power series given by
Cauchy integral formulas. -/
theorem _root_.DiffContOnCl.hasFPowerSeriesOnBall {R : ℝ≥0} {c : ℂ} {f : ℂ → E} (hf : DiffContOnCl ℂ f (ball c R))
(hR : 0 < R) : HasFPowerSeriesOnBall f (cauchyPowerSeries f c R) c R :=
hasFPowerSeriesOnBall_of_differentiable_off_countable countable_empty hf.continuousOn_ball
(fun _z hz => hf.differentiableAt isOpen_ball hz.1) hR
