Cauchy's Theorem for the annulus

This file proves Cauchy's Theorem for the annulus (concentric circles): if f is holomorphic on the annular region between two concentric circles, then the integrals over the two circles are equal.

This is invoked in the book (Lecture 14) to justify that the residue Res_{z=a} f(z) = (1/2πi) ∮_C f(z) dz is independent of the choice of circle C centered at a.

Main results

• circleIntegral_eq_of_holomorphic_on_annulus: If f is holomorphic on closedBall a R \ ball a r (with 0 < r ≤ R), then ∮_{C(a,R)} f = ∮_{C(a,r)} f.

• circleIntegral_eq_of_annulus: Strict inequality variant (with 0 < r < R).

Implementation notes

This is a direct consequence of Mathlib's Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable, which proves the result for concentric circles allowing a countable exceptional set. We specialize it with an empty exceptional set.

theorem circleIntegral_eq_of_holomorphic_on_annulus {a : ℂ} {R r : ℝ} (hr : 0 < r) (hle : r ≤ R) {f : ℂ → ℂ} (hcont : ContinuousOn f (Metric.closedBall a R \ Metric.ball a r)) (hdiff : ∀ z ∈ Metric.ball a R \ Metric.closedBall a r, DifferentiableAt ℂ f z) : ∮ (z : ℂ) in C(a, R), f z = ∮ (z : ℂ) in C(a, r), f z

Cauchy's Theorem for the annulus (concentric circles).

If f is holomorphic on the closed annulus closedBall a R \ ball a r (with 0 < r ≤ R), then the integrals over the two concentric circles C(a, R) and C(a, r) are equal: ∮_{C(a,R)} f = ∮_{C(a,r)} f.

This corresponds to the book's statement that the residue is independent of the choice of circle centered at a, justified by "Cauchy's Theorem for the annulus". The book cites this as a known result without proof; we prove it using Mathlib's circleIntegral_eq_of_differentiable_on_annulus_off_countable.

theorem circleIntegral_eq_of_annulus {a : ℂ} {r R : ℝ} (hr : 0 < r) (_hR : 0 < R) (hrR : r < R) {f : ℂ → ℂ} (hcont : ContinuousOn f (Metric.closedBall a R \ Metric.ball a r)) (hdiff : ∀ z ∈ Metric.ball a R \ Metric.closedBall a r, DifferentiableAt ℂ f z) : ∮ (z : ℂ) in C(a, R), f z = ∮ (z : ℂ) in C(a, r), f z

Cauchy's Theorem for the annulus (concentric circles), strict inequality variant.

If f is continuous on the closed annulus closedBall a R \ ball a r and differentiable on its interior (with 0 < r < R), then the contour integrals over the two concentric circles are equal: ∮_{C(a,R)} f = ∮_{C(a,r)} f.