Theorems · Theorem · complex analysis

DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ},
  0 < R →
    ∀ (n : ℕ),
      DiffContOnCl ℂ f (Metric.ball c R) →
        ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
          (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c

Cauchy integral formula for derivatives, assuming f is continuous on a closed ball and differentiable on its interior.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

3 results in Mathlib

Foundations

Depth 284 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace