Theorems · Theorem · complex analysis

Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r R : ℝ},
  0 < r →
    r ≤ R →
      ∀ {f : ℂ → E} {s : Set ℂ},
        s.Countable →
          ContinuousOn f (Metric.closedBall c R \ Metric.ball c r) →
            (∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) →
              ∮ (z : ℂ) in C(c, R), f z = ∮ (z : ℂ) in C(c, r), f z

Cauchy-Goursat theorem for an annulus. If f : ℂ → E is continuous on the closed annulus r ≤ ‖z - c‖ ≤ R, 0 < r ≤ R, and is complex differentiable at all but countably many points of its interior, then the integrals of f over the circles ‖z - c‖ = r and ‖z - c‖ = R are equal to each other.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace