Theorems · Theorem · complex analysis

DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E},
  DiffContOnCl ℂ f (Metric.ball c R) →
    w ∈ Metric.ball c R → (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w

Cauchy integral formula: if f : ℂ → E is complex differentiable on an open disc and is continuous on its closure, then for any w in this open ball we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace