Cauchy's derivative formula at an arbitrary point of a disk

Mathlib's higher-derivative circle formula is stated at the center. Here the evaluation point may be anywhere in the open disk. Differentiating the contour kernel with respect to that point preserves the hypothesis of continuity on the boundary: no boundary derivatives of the function are required.

These scalar-valued, one-variable results also support iterated Cauchy formulas in several variables. The circle center and evaluation point are independent, and the derivative order is arbitrary. The statements use Mathlib's HasDerivAt, iteratedDeriv, DiffContOnCl, and circle-integral interfaces rather than introducing a separate contour or derivative theory. Their intended Mathlib home is Analysis.Complex.CauchyIntegral.

theorem hasDerivAt_circleIntegral_sub_zpow_mulCarlson {c w : ℂ} {R : ℝ} (hR : 0 ≤ R) (hw : w ∈ Metric.ball c R) {f : ℂ → ℂ} (hf : ContinuousOn f (Metric.sphere c R)) (n : ℕ) : HasDerivAt (fun (w : ℂ) => ∮ (s : ℂ) in C(c, R), (s - w) ^ (-(↑n + 1)) * f s) ((↑n + 1) * ∮ (s : ℂ) in C(c, R), (s - w) ^ (-(↑(n + 1) + 1)) * f s) w

Differentiation in the evaluation point raises the order of the circle Cauchy kernel.

theorem DiffContOnCl.iteratedDeriv_eq_circleIntegral_sub_zpow_mulCarlson {c : ℂ} {R : ℝ} {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hR : 0 < R) (n : ℕ) {w : ℂ} (hw : w ∈ Metric.ball c R) : iteratedDeriv n f w = ↑n.factorial * (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, R), (s - w) ^ (-(↑n + 1)) * f s

Cauchy's formula for every derivative at any point inside the circle. The function need only be holomorphic in the open disk and continuous on its closure.