Theorems · Theorem · complex analysis

Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux

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

An auxiliary lemma for Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable. This lemma assumes w ∉ s while the main lemma drops this assumption.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace