Theorems · Theorem · complex analysis

DiffContOnCl.circleIntegral_eq_zero

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ},
  0 ≤ R → ∀ {f : ℂ → E} {c : ℂ}, DiffContOnCl ℂ f (Metric.ball c R) → ∮ (z : ℂ) in C(c, R), f z = 0

Cauchy-Goursat theorem for a disk: if f : ℂ → E is continuous on a closed disk {z | ‖z - c‖ ≤ R} and is complex differentiable on the open disk, then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace