The winding numbers of the half-disc contour

WorkedExamples/HalfDisc/Basic.lean builds the boundary of the upper half-disc of radius R about the origin and computes its generalized winding number at the one point of the contour that the Hungerbühler–Wasem half-residue theorem needs: the origin, where the value is ½. This file computes the winding number at every point off the contour, which is what turns the contour from the carrier of a single worked example into a general tool:

• 1 at every point of the open upper half-disc, the classical interior value, so a singularity there contributes its full residue;
• 0 below the real axis and outside the closed disc, so a singularity there contributes nothing.

The interior value is obtained with no homotopy or Jordan-curve input. Write Λ for the diameter piece, A for the upper arc and B for the lower arc of the same circle. The full circle gives n(A) + n(B) = 1, and Λ and B are evaluated by the same logarithmic FTC: about a point s strictly above the real axis, neither Λ t - s nor B θ - s ever leaves the open lower half-plane, hence never leaves Complex.slitPlane, so the principal branch of Complex.log is a single-valued primitive along each and both integrals telescope to the same value log (R - s) - log (-R - s). Hence n(Λ) + n(A) = n(B) + n(A) = 1.

The vanishing statements go through IsPiecewiseC1On.windingNumber_eq_zero_of_ray: a point below the axis escapes to infinity straight downwards, and a point outside the closed disc escapes radially, in both cases without meeting the contour.

Together with windingNumber_halfDiscBoundary, this settles every point except those on the contour other than the origin -- a real t with |t| < R, or a point of the upper semicircle. There the winding number is a genuine principal value rather than an ordinary integral, and the diameter's contribution is the principal value of a segment crossed away from its midpoint, which the segment API does not yet evaluate.

Main results

• TauCeti.Contour.windingNumber_halfDiscBoundary_eq_one — the winding number is 1 at every point of the open upper half-disc.
• TauCeti.Contour.windingNumber_halfDiscBoundary_eq_zero_of_im_neg and TauCeti.Contour.windingNumber_halfDiscBoundary_eq_zero_of_lt_norm — it is 0 below the real axis and outside the closed disc.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

A logarithmic evaluation of an index integral

The interior value

theorem TauCeti.Contour.windingNumber_halfDiscBoundary_eq_one {R : ℝ} {s : ℂ} (him : 0 < s.im) (hs : ‖s‖ < R) : windingNumber (halfDiscBoundary R) (-R) (R + Real.pi) s = 1

The half-disc contour has winding number 1 about every point of the open upper half-disc.

The diameter and the lower semicircle both telescope, through the principal logarithm, to log (R - s) - log (-R - s): about a point s above the real axis, neither t - s (for real t) nor B θ - s (for B the lower semicircle) ever leaves the open lower half-plane, which is contained in Complex.slitPlane. Since the whole circle has winding number 1, the upper semicircle contributes 1 minus the lower one, and the two occurrences of that common logarithmic value cancel.

The exterior values

theorem TauCeti.Contour.windingNumber_halfDiscBoundary_eq_zero_of_im_neg {R : ℝ} (hR : 0 < R) {s : ℂ} (him : s.im < 0) : windingNumber (halfDiscBoundary R) (-R) (R + Real.pi) s = 0

The half-disc contour has winding number 0 below the real axis. The contour lies in the closed upper half-plane, so a point beneath the axis escapes to infinity straight downwards without meeting it.

theorem TauCeti.Contour.windingNumber_halfDiscBoundary_eq_zero_of_lt_norm {R : ℝ} (hR : 0 < R) {s : ℂ} (hs : R < ‖s‖) : windingNumber (halfDiscBoundary R) (-R) (R + Real.pi) s = 0

The half-disc contour has winding number 0 outside the closed disc. The contour lies in the closed disc of radius R, so a point beyond it escapes to infinity radially without meeting the contour.