English
Let F be a function from the complex plane to a normed space, differentiable in a neighborhood of a circle around c with radius R>0, and let f coincide with F on that circle. Then the derivative at c is given by a Cauchy-type circle integral: deriv f c = (2πi)^{-1} ∮_{|z−c|=R} (z−c)^{-2} f(z) dz.
Русский
Пусть f: ℂ→F дифференцируема в окрестности окружности с центром c и радиусом R>0, и на окружности она совпадает с g. Тогда производная в c задаётся интегралом по окружности: f'(c) = (2πi)^{-1} ∮_{|z−c|=R} (z−c)^{-2} f(z) dz.
LaTeX
$$$\\displaystyle \\text{For completeness } \\text{If } f: \\mathbb{C} \\to F, \\ R>0, \\\\ f \\text{ differentiable on } C(c,R) \\\\ \\text{then } \\mathrm{deriv}\, f\\, c = (2 \\pi i)^{-1} \\oint z \\in C(c,R) (z-c)^{-2} \\cdot f(z) \\, dz.$$$
Lean4
/-- If `f` is complex differentiable on an open disc with center `c` and radius `R > 0` and is
continuous on its closure, then `f' c` can be represented as an integral over the corresponding
circle.
TODO: add a version for `w ∈ Metric.ball c R`.
TODO: add a version for higher derivatives. -/
theorem deriv_eq_smul_circleIntegral [CompleteSpace F] {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R)
(hf : DiffContOnCl ℂ f (ball c R)) : deriv f c = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z :=
by
lift R to ℝ≥0 using hR.le
refine (hf.hasFPowerSeriesOnBall hR).hasFPowerSeriesAt.deriv.trans ?_
simp only [cauchyPowerSeries_apply, one_div, zpow_neg, pow_one, smul_smul, zpow_two, mul_inv]
