Theorems · Theorem · complex analysis

Complex.circleIntegral_sub_center_inv_smul_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), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z

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 z / (z - c) (formally, (z - c)⁻¹ • f z) over the circles ‖z - c‖ = r and ‖z - c‖ = R are equal to each other.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace