The half-disc boundary contour

For 0 < R, the boundary of the upper half-disc of radius R about the origin, traversed counterclockwise on [-R, R + π]: the diameter along the real axis from -R to R, followed by the semicircular arc from R back to -R, the arc carrying its angle in t - R.

Its distinguishing feature is that it passes through the origin rather than detouring around it, so the origin is an on-curve point and the generalized winding number there is ½ — the value strictly between the exterior 0 and the interior 1:

• the diameter contributes 0: the index integrand 1 / t is odd, so its principal value over the symmetric interval vanishes (windingNumber_eq_zero_segment);
• the arc contributes ½: it is a half-circle about its own centre, so its winding is its angular extent π / 2π (windingNumber_circleMap_center_eq_half).

That ½ is exactly the hypothesis of the Hungerbühler–Wasem half-residue theorem hasCauchyPV_half_residue, which is why this contour is the one HW's motivating example uses: a Cauchy principal value along the real axis with a simple pole at the origin, where the classical residue theorem does not apply because the pole lies on the contour.

Main results

• TauCeti.Contour.halfDiscBoundary — the contour, with halfDiscBoundary_of_le and halfDiscBoundary_of_lt evaluating its two branches and halfDiscBoundary_left, halfDiscBoundary_right its endpoints (equal, so the contour is closed).
• TauCeti.Contour.continuous_halfDiscBoundary — the two branches agree at the junction, so the contour is continuous.
• TauCeti.Contour.isPwC1ImmersionOn_halfDiscBoundary — it is a piecewise-C¹ immersion, with the single breakpoint R; this is the regularity hypothesis of the Hungerbühler–Wasem theorems.
• TauCeti.Contour.windingNumber_halfDiscBoundary — its generalized winding number about the origin is ½.
• TauCeti.Contour.halfDiscBoundary_eq_zero_iff — the contour meets the origin exactly once, at t = 0.
• TauCeti.Contour.halfDiscBoundary_im_eq_zero_or_norm_eq, TauCeti.Contour.im_halfDiscBoundary_nonneg, and TauCeti.Contour.norm_halfDiscBoundary_le — the contour lies in the closed upper half-disc on its parameter interval, with TauCeti.Contour.norm_halfDiscBoundary_eq pinning the arc to the circle itself.
• TauCeti.Contour.halfDiscBoundary_ne_of_im_pos_of_norm_lt — the contour avoids the open upper half-disc.
• TauCeti.Contour.deriv_halfDiscBoundary_of_lt_radius and TauCeti.Contour.deriv_halfDiscBoundary_of_lt — before the junction the derivative is the real inclusion's, beyond it the circle map's at the shifted parameter.
• TauCeti.Contour.integral_halfDiscBoundary_arc — the [R, R + π] piece of the contour integral is the circleMap 0 R integral over [0, π]; for 0 < R that is the upper semicircle, the form Jordan's lemma bounds.
• TauCeti.Contour.flatOfOrder_halfDiscBoundary — both one-sided branches at the origin lie on the real line, so the contour is flat there to every order.
• TauCeti.Contour.conditionAprime_halfDiscBoundary — Hungerbühler–Wasem condition (A′) at the origin, for any integrand.

References

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

noncomputable def TauCeti.Contour.halfDiscBoundary (R : ℝ) : ℝ → ℂ

The half-disc boundary contour. On [-R, R + π]: the diameter t ↦ t for t ≤ R, then the semicircular arc t ↦ R e^{i(t-R)} from R back to -R.

Equations

• TauCeti.Contour.halfDiscBoundary R t = if t ≤ R then ↑t else circleMap 0 R (t - R)

@[simp]

theorem TauCeti.Contour.halfDiscBoundary_of_le {R t : ℝ} (h : t ≤ R) : halfDiscBoundary R t = ↑t

@[simp]

theorem TauCeti.Contour.halfDiscBoundary_of_lt {R t : ℝ} (h : R < t) : halfDiscBoundary R t = circleMap 0 R (t - R)

Where the contour lives

theorem TauCeti.Contour.halfDiscBoundary_im_eq_zero_or_norm_eq {R : ℝ} (hR : 0 ≤ R) (t : ℝ) : (halfDiscBoundary R t).im = 0 ∨ ‖halfDiscBoundary R t‖ = R

Each point of the half-disc contour is either real or on the circle. Up to the junction the contour runs along the real diameter, beyond it along the circle of radius R; there is no third possibility. This dichotomy is what keeps the contour out of the open upper half-disc.

theorem TauCeti.Contour.im_halfDiscBoundary_nonneg {R : ℝ} (hR : 0 ≤ R) {t : ℝ} (ht : t ≤ R + Real.pi) : 0 ≤ (halfDiscBoundary R t).im

The half-disc contour stays in the closed upper half-plane on its parameter interval: the diameter is real and the arc is the upper semicircle.

theorem TauCeti.Contour.norm_halfDiscBoundary_le {R : ℝ} (hR : 0 ≤ R) {t : ℝ} (ht : -R ≤ t) : ‖halfDiscBoundary R t‖ ≤ R

The half-disc contour stays in the closed disc of radius R on its parameter interval: the diameter has |t| ≤ R and the arc has norm exactly R.

theorem TauCeti.Contour.norm_halfDiscBoundary_eq {R : ℝ} (hR : 0 ≤ R) {t : ℝ} (ht : R ≤ t) : ‖halfDiscBoundary R t‖ = R

Beyond the junction the half-disc contour has norm exactly R. At the junction itself the contour is the real point R; past it, it is the circle of radius R.

theorem TauCeti.Contour.halfDiscBoundary_ne_of_im_pos_of_norm_lt {R : ℝ} {s : ℂ} (him : 0 < s.im) (hs : ‖s‖ < R) (t : ℝ) : halfDiscBoundary R t ≠ s

The half-disc contour avoids the open upper half-disc. A point strictly above the real axis and strictly inside the disc is neither real nor at distance R from the origin.

theorem TauCeti.Contour.halfDiscBoundary_left {R : ℝ} (hR : 0 ≤ R) : halfDiscBoundary R (-R) = ↑(-R)

The contour starts at -R.

@[simp]

theorem TauCeti.Contour.halfDiscBoundary_right (R : ℝ) : halfDiscBoundary R (R + Real.pi) = ↑(-R)

The contour ends at -R, so it is closed.

theorem TauCeti.Contour.eqOn_halfDiscBoundary_segment {R : ℝ} (hR : 0 ≤ R) : Set.EqOn (fun (t : ℝ) => 1 * ↑t + 0) (halfDiscBoundary R) (Set.uIoo (-R) R)

On the diameter's parameter interval the contour is the real segment.

@[simp]

theorem TauCeti.Contour.deriv_halfDiscBoundary_of_lt_radius {R t : ℝ} (h : t < R) : deriv (halfDiscBoundary R) t = deriv (fun (s : ℝ) => ↑s) t

The derivative on the open diameter. Strictly before the junction the half-disc boundary is the real inclusion on a whole neighbourhood, so the two derivatives agree.

@[simp]

theorem TauCeti.Contour.deriv_halfDiscBoundary_of_lt {R t : ℝ} (h : R < t) : deriv (halfDiscBoundary R) t = deriv (circleMap 0 R) (t - R)

The derivative on the open arc. Strictly beyond the junction the half-disc boundary coincides with the shifted circle map on a whole neighbourhood, so its derivative is the circle map's, evaluated at the shifted parameter. (At the junction t = R itself the contour has a corner, and no such identity is claimed.)

theorem TauCeti.Contour.integral_halfDiscBoundary_arc (f : ℂ → ℂ) (R : ℝ) : ∫ (t : ℝ) in R..R + Real.pi, f (halfDiscBoundary R t) * deriv (halfDiscBoundary R) t = ∫ (θ : ℝ) in 0..Real.pi, f (circleMap 0 R θ) * deriv (circleMap 0 R) θ

The arc piece of the contour integral is the circle-map integral. Beyond the junction the half-disc boundary is the circle map shifted by R, so translating the parameter identifies the [R, R + π] piece of ∮_γ f with the integral of circleMap 0 R over [0, π]. The junction t = R itself, where the contour has a corner, is a single point and does not affect the integral.

The identity holds for every R. For 0 < R the right-hand side is the upper semicircle traversed counterclockwise — the form Jordan's lemma bounds; for R < 0 the same parametrization traces the lower semicircle instead, and R = 0 is degenerate, circleMap 0 0 being the constant path at the origin.

theorem TauCeti.Contour.eqOn_halfDiscBoundary_arc (R : ℝ) : Set.EqOn (circleMap 0 R ∘ fun (s : ℝ) => s - R) (halfDiscBoundary R) (Set.uIcc R (R + Real.pi))

On the arc's parameter interval — including both endpoints, where the two agree — the contour is the circle reparametrized by t ↦ t - R.

theorem TauCeti.Contour.continuous_halfDiscBoundary (R : ℝ) : Continuous (halfDiscBoundary R)

The half-disc boundary is continuous, the two branches agreeing at the junction t = R (where circleMap 0 R 0 = R).

theorem TauCeti.Contour.isPwC1ImmersionOn_halfDiscBoundary {R : ℝ} (hR : 0 < R) : IsPwC1ImmersionOn (halfDiscBoundary R) (-R) (R + Real.pi)

The half-disc boundary is a piecewise-C¹ immersion, with the single breakpoint R where the diameter meets the arc. Off that breakpoint each piece is one of the two smooth branches: the real inclusion, of derivative 1, or the shifted circle, of derivative R e^{i(t-R)} · i; both are nonzero for 0 < R, so the tangent never vanishes.

theorem TauCeti.Contour.windingNumber_halfDiscBoundary {R : ℝ} (hR : 0 < R) : windingNumber (halfDiscBoundary R) (-R) (R + Real.pi) 0 = 1 / 2

The half-disc boundary has winding number ½ about the origin. The diameter through the origin contributes 0 and the semicircular arc about it contributes ½.

@[simp]

theorem TauCeti.Contour.halfDiscBoundary_eq_zero_iff {R : ℝ} (hR : 0 < R) {t : ℝ} : halfDiscBoundary R t = 0 ↔ t = 0

The half-disc boundary meets the origin exactly once, at t = 0: on the diameter γ t = t vanishes only there, and the arc stays at distance |R| from the origin.

theorem TauCeti.Contour.flatOfOrder_halfDiscBoundary {R : ℝ} (hR : 0 ≤ R) (n : ℕ) : FlatOfOrder (halfDiscBoundary R) 0 n

The half-disc boundary is flat to every order at the origin. With tangent direction v = 1 the perpendicular deviation |Im (γ t - γ 0)| vanishes identically near t = 0, which is o of anything. For R > 0 that is because the contour is locally the real diameter; for the degenerate radius R = 0 the arc collapses to the origin, so both one-sided branches still lie on the real line.

theorem TauCeti.Contour.conditionAprime_halfDiscBoundary {R : ℝ} (hR : 0 < R) (f : ℂ → ℂ) : ConditionAprime (halfDiscBoundary R) (-R) (R + Real.pi) f {0}

Condition (A′) holds for the half-disc boundary at the origin, for any integrand. The origin is met exactly once, the contour is flat there to every order (it is locally the real diameter), and the basepoint γ(-R) = -R is not the origin, so that clause is vacuous.