A circle integral with two simple poles

This file verifies the two-pole worked example from the contour-integration roadmap. For two distinct points s₁ and s₂, the function

z ↦ A / (z - s₁) + B / (z - s₂)

has residues A and B at the respective poles. When both poles lie inside a circle, its contour integral is therefore 2πi (A + B). The calculation is stated directly for arbitrary centres, radii, pole positions, and coefficients, so it also covers a vanishing coefficient without pretending that the corresponding point remains a pole.

The integral calculation uses Mathlib's circleIntegral.integral_sub_inv_of_mem_ball; the residue calculations use the simple-pole API in TauCeti.Analysis.Contour.Residue.SimplePole.

This is the concrete two-simple-pole acceptance criterion in TauCetiRoadmap/ContourIntegration/README.md, under “Worked examples”.

noncomputable def TauCeti.Contour.twoPrincipalParts (A B s₁ s₂ z : ℂ) : ℂ

The rational function with prescribed principal parts A / (z - s₁) and B / (z - s₂).

Equations

• TauCeti.Contour.twoPrincipalParts A B s₁ s₂ z = A * (z - s₁)⁻¹ + B * (z - s₂)⁻¹

@[simp]

theorem TauCeti.Contour.twoPrincipalParts_apply (A B s₁ s₂ z : ℂ) : twoPrincipalParts A B s₁ s₂ z = A * (z - s₁)⁻¹ + B * (z - s₂)⁻¹

The value of twoPrincipalParts at a point.

theorem TauCeti.Contour.twoPrincipalParts_eq (A B s₁ s₂ : ℂ) : twoPrincipalParts A B s₁ s₂ = fun (z : ℂ) => A * (z - s₁)⁻¹ + B * (z - s₂)⁻¹

The function-level defining equation for twoPrincipalParts.

theorem TauCeti.Contour.analyticAt_twoPrincipalParts {A B s₁ s₂ z : ℂ} (h : (A = 0 ∨ z ≠ s₁) ∧ (B = 0 ∨ z ≠ s₂) ∨ s₁ = s₂ ∧ A + B = 0) : AnalyticAt ℂ (twoPrincipalParts A B s₁ s₂) z

twoPrincipalParts is analytic where each nonzero principal part is away from its designated point, or where coincident principal parts cancel.

theorem TauCeti.Contour.meromorphicAt_twoPrincipalParts (A B s₁ s₂ z : ℂ) : MeromorphicAt (twoPrincipalParts A B s₁ s₂) z

The function twoPrincipalParts is meromorphic everywhere.

@[simp]

theorem TauCeti.Contour.residue_twoPrincipalParts_left {A B s₁ s₂ : ℂ} (h : B = 0 ∨ s₁ ≠ s₂) : residue (twoPrincipalParts A B s₁ s₂) s₁ = A

At the first designated point, the residue of twoPrincipalParts is the first coefficient if the other principal part vanishes or is designated at a distinct point.

@[simp]

theorem TauCeti.Contour.residue_twoPrincipalParts_right {A B s₁ s₂ : ℂ} (h : A = 0 ∨ s₁ ≠ s₂) : residue (twoPrincipalParts A B s₁ s₂) s₂ = B

At the second designated point, the residue of twoPrincipalParts is the second coefficient if the other principal part vanishes or is designated at a distinct point.

theorem TauCeti.Contour.circleIntegral_twoPrincipalParts {A B c s₁ s₂ : ℂ} {R : ℝ} (hs₁ : A = 0 ∨ s₁ ∈ Metric.ball c R) (hs₂ : B = 0 ∨ s₂ ∈ Metric.ball c R) : circleIntegral (twoPrincipalParts A B s₁ s₂) c R = 2 * ↑Real.pi * Complex.I * (A + B)

Two-pole circle integral. If the designated point of each nonzero principal part lies strictly inside the circle C(c, R), then the integral of A / (z - s₁) + B / (z - s₂) around that circle is 2πi (A + B). Together with residue_twoPrincipalParts_left and residue_twoPrincipalParts_right, this is the roadmap's worked example of the classical residue theorem with two simple poles.

theorem TauCeti.Contour.circleIntegral_twoPrincipalParts_eq_residue_sum {A B c s₁ s₂ : ℂ} {R : ℝ} (hs : s₁ ≠ s₂) (hs₁ : A = 0 ∨ s₁ ∈ Metric.ball c R) (hs₂ : B = 0 ∨ s₂ ∈ Metric.ball c R) : circleIntegral (twoPrincipalParts A B s₁ s₂) c R = 2 * ↑Real.pi * Complex.I * (residue (twoPrincipalParts A B s₁ s₂) s₁ + residue (twoPrincipalParts A B s₁ s₂) s₂)

The two-pole calculation in residue-theorem form: for distinct designated points, with the point of each nonzero principal part inside the circle, the integral is 2πi times the sum of the two residues.