Theorems · Theorem · complex analysis

Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto

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

Cauchy integral formula for the value at the center of a disc. If f is continuous on a punctured closed disc of radius R, is differentiable at all but countably many points of the interior of this disc, and has a limit y at the center of the disc, then the integral $\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to 2πiy.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace