The half-disc residue theorem

The Hungerbühler–Wasem generalized residue theorem, run on the boundary of the upper half-disc of radius R about the origin -- the contour of WorkedExamples/HalfDisc/Basic.lean, which passes through the origin instead of detouring around it. With the winding numbers of WorkedExamples/HalfDisc/Winding.lean -- 1 in the open upper half-disc, ½ at the origin, 0 outside -- the principal value of ∮ f along that contour is

2π i · Σ_{s ∈ S} Res_s f + π i · Res₀ f

for f holomorphic off insert 0 S with at worst simple poles there and S inside the half-disc: each enclosed possible singularity contributes its full residue, while the possible singularity on the contour contributes only half of its own. In the nonremovable simple-pole case at the origin, the classical residue theorem cannot reach the second term at all, because the pole lies on the path of integration and only a principal-value integral exists.

The S = ∅ case, where the origin is the only prescribed point, is WorkedExamples/HalfDisc/HalfResidue.lean; when f is regular at the origin, the result reduces to the classical residue theorem for this contour.

The possible singularity on the real axis is pinned at the origin, as throughout the half-disc development: the contour halfDiscBoundary is centred there, and a possible real singularity elsewhere is reached by centring the contour on it instead. Every prescribed singularity is required to be at worst simple, which is what makes the Hungerbühler–Wasem conditions (A′) and (B) automatic.

Main results

• TauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_poles — the principal value along the half-disc boundary, with possible enclosed singularities and a possible singularity at the origin on the contour.
• TauCeti.Contour.hasCauchyPV_halfDiscBoundary_diameter_of_simple_poles — the same with the arc contribution subtracted off, leaving the principal value along the diameter and an explicit circleMap integral for the arc, the form Jordan's lemma bounds.
• TauCeti.Contour.hasCauchyPV_realSegment_of_simple_poles — the same restated along the straight line t ↦ t, the form a real-axis improper integral consumes.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, Thm 3.3.
• P. Henrici, Applied and Computational Complex Analysis, Volume 1: Power Series—Integration— Conformal Mapping—Location of Zeros, Wiley, 1974, Thm 4.8f.

theorem TauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_poles {R : ℝ} {S : Finset ℂ} {f : ℂ → ℂ} (hR : 0 < R) (hS : ∀ s ∈ S, 0 < s.im ∧ ‖s‖ < R) (hf : DifferentiableOn ℂ f (Set.univ \ ↑(insert 0 S))) (hmero : ∀ s ∈ insert 0 S, MeromorphicAt f s) (h_simple : ∀ s ∈ insert 0 S, ↑(-1) ≤ meromorphicOrderAt f s) : HasCauchyPV (halfDiscBoundary R) (-R) (R + Real.pi) f (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, residue f s + ↑Real.pi * Complex.I * residue f 0)

The half-disc residue theorem with enclosed possible singularities. Let f be holomorphic off the finite set insert 0 S, with at worst a simple singularity at each of its points, and let every point of S lie in the open upper half-disc of radius R. Then the Cauchy principal value of ∮ f along the half-disc boundary is

2π i · Σ_{s ∈ S} Res_s f + π i · Res₀ f:

each enclosed possible singularity contributes its full residue, because the generalized winding number there is 1, while the possible singularity on the contour contributes only half of its own. In the genuine simple-pole case, this is the half-residue contribution from the winding number ½ at a smooth crossing.

theorem TauCeti.Contour.hasCauchyPV_halfDiscBoundary_diameter_of_simple_poles {R : ℝ} {S : Finset ℂ} {f : ℂ → ℂ} (hR : 0 < R) (hS : ∀ s ∈ S, 0 < s.im ∧ ‖s‖ < R) (hf : DifferentiableOn ℂ f (Set.univ \ ↑(insert 0 S))) (hmero : ∀ s ∈ insert 0 S, MeromorphicAt f s) (h_simple : ∀ s ∈ insert 0 S, ↑(-1) ≤ meromorphicOrderAt f s) : HasCauchyPV (halfDiscBoundary R) (-R) R f (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, residue f s + ↑Real.pi * Complex.I * residue f 0 - ∫ (θ : ℝ) in 0..Real.pi, f (circleMap 0 R θ) * deriv (circleMap 0 R) θ)

Splitting off the arc. Subtracting the arc contribution from the principal value along the whole half-disc boundary leaves the principal value along the diameter alone, with the arc expressed as a circleMap integral — the form Jordan's lemma bounds when the radius grows.

theorem TauCeti.Contour.hasCauchyPV_realSegment_of_simple_poles {R : ℝ} {S : Finset ℂ} {f : ℂ → ℂ} (hR : 0 < R) (hS : ∀ s ∈ S, 0 < s.im ∧ ‖s‖ < R) (hf : DifferentiableOn ℂ f (Set.univ \ ↑(insert 0 S))) (hmero : ∀ s ∈ insert 0 S, MeromorphicAt f s) (h_simple : ∀ s ∈ insert 0 S, ↑(-1) ≤ meromorphicOrderAt f s) : HasCauchyPV (fun (t : ℝ) => ↑t) (-R) R f (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, residue f s + ↑Real.pi * Complex.I * residue f 0 - ∫ (θ : ℝ) in 0..Real.pi, f (circleMap 0 R θ) * deriv (circleMap 0 R) θ)

The identity along the real segment. The diameter of the half-disc traces the straight line t ↦ t, so the principal value can be stated along that curve directly — the form a real-axis improper integral consumes, with no reference to the auxiliary contour. Letting R → ∞ with an arc bound (Jordan's lemma, say) turns this into an improper-integral evaluation that the classical residue theorem cannot reach when the origin is a genuine pole on the line of integration.