The two-ray corner and its vanishing index principal value

The Hungerbühler–Wasem model sector (HW (2.4)) is the closed curve made of a radial segment into its centre, a circular arc of opening angle α, and a radial segment back out. The arc's contribution is α / 2π (indexIntegral_arc); this file supplies the other half, that the two radial segments contribute nothing.

The two segments cannot be treated separately: for nonzero ray directions and R > 0 each excised integral diverges logarithmically as ε → 0. Taken together they cancel exactly, at every ε, so the pair is packaged here as a single curve through the centre.

Main definitions

• TauCeti.Contour.twoRayCorner — the corner z₀ approached along direction u and left along direction v, with the corner at t = 0.

Main results

• TauCeti.Contour.deriv_twoRayCorner_of_ne and TauCeti.Contour.norm_twoRayCorner_sub — the derivative and the distance from the corner, off the corner itself.
• TauCeti.Contour.hasCauchyPVAt_inv_sub_twoRayCorner — the index principal value along a two-ray corner with ‖u‖ = ‖v‖, over [-R, R], is 0; cauchyPVExistsAt_inv_sub_twoRayCorner is its existence form.
• TauCeti.Contour.windingNumber_eq_zero_twoRayCorner — its generalized winding number vanishes.

This is Layer 1 of the Hungerbühler–Wasem generalized residue theorem (HW Thm 3.3).

References

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

noncomputable def TauCeti.Contour.twoRayCorner (z₀ u v : ℂ) : ℝ → ℂ

The two-ray corner at z₀. For t < 0 the curve sits at distance |t| ‖u‖ from z₀ along u, and for t ≥ 0 at distance t ‖v‖ along v; it meets z₀ at t = 0. If both directions are nonzero that is the only such parameter; if one of them vanishes the corresponding ray is constant at z₀.

On [-R, R] with ‖u‖ = ‖v‖ the two endpoints lie on the circle of radius |R| ‖v‖ about z₀, so concatenating with the arc between them gives the Hungerbühler–Wasem model sector, parametrised from the far end of one radius rather than from the corner. For unequal norms it is simply a two-ray curve.

Equations

• TauCeti.Contour.twoRayCorner z₀ u v t = if t < 0 then z₀ - ↑t * u else z₀ + ↑t * v

@[simp]

theorem TauCeti.Contour.twoRayCorner_of_neg {z₀ u v : ℂ} {t : ℝ} (ht : t < 0) : twoRayCorner z₀ u v t = z₀ - ↑t * u

Evaluation of the corner curve on the incoming ray.

@[simp]

theorem TauCeti.Contour.twoRayCorner_of_nonneg {z₀ u v : ℂ} {t : ℝ} (ht : 0 ≤ t) : twoRayCorner z₀ u v t = z₀ + ↑t * v

Evaluation of the corner curve on the outgoing ray, including the corner itself.

theorem TauCeti.Contour.continuous_twoRayCorner (z₀ u v : ℂ) : Continuous (twoRayCorner z₀ u v)

The two-ray corner is continuous: its two affine branches agree at the corner.

theorem TauCeti.Contour.deriv_twoRayCorner_of_ne {z₀ u v : ℂ} {t : ℝ} (ht : t ≠ 0) : deriv (twoRayCorner z₀ u v) t = if t < 0 then -u else v

The derivative of the corner curve off the corner: -u on the negative ray, v on the positive ray.

theorem TauCeti.Contour.norm_twoRayCorner_sub {z₀ u v : ℂ} (huv : ‖u‖ = ‖v‖) (t : ℝ) : ‖twoRayCorner z₀ u v t - z₀‖ = |t| * ‖v‖

The distance from the corner is |t| times the common ray length.

theorem TauCeti.Contour.hasCauchyPVAt_inv_sub_twoRayCorner {z₀ u v : ℂ} (huv : ‖u‖ = ‖v‖) (R : ℝ) : HasCauchyPVAt (twoRayCorner z₀ u v) (-R) R (fun (z : ℂ) => (z - z₀)⁻¹) z₀ 0

The index principal value along a two-ray corner vanishes. For nonzero rays of equal length the excision ‖γ t - z₀‖ > ε is the symmetric condition |t| ‖v‖ > ε, and the integrand is the odd function 1 / t on both rays, so every truncated integral is 0 — not merely its limit. Equal norms also permit u = v = 0, where the curve is constant at z₀ and the integrand vanishes identically; that case is immediate.

theorem TauCeti.Contour.cauchyPVExistsAt_inv_sub_twoRayCorner {z₀ u v : ℂ} (huv : ‖u‖ = ‖v‖) (R : ℝ) : CauchyPVExistsAt (twoRayCorner z₀ u v) (-R) R (fun (z : ℂ) => (z - z₀)⁻¹) z₀

Existence form of hasCauchyPVAt_inv_sub_twoRayCorner, matching the existence-form API that the winding-number composition lemmas consume.

@[simp]

theorem TauCeti.Contour.windingNumber_eq_zero_twoRayCorner {z₀ u v : ℂ} (huv : ‖u‖ = ‖v‖) (R : ℝ) : windingNumber (twoRayCorner z₀ u v) (-R) R z₀ = 0

The generalized winding number of a two-ray corner vanishes. The radial approach and departure contribute nothing to the model sector's index; all of it comes from the arc.