The Hungerbühler–Wasem model sector

The model sector of opening angle α at z₀ is the closed curve made of a radial segment inward to z₀ along direction φ + α, a radial segment back out along direction φ, and a circular arc of radius r sweeping α from φ round to φ + α, which closes the curve at the point it started from. Both radii are traversed before the arc — the parameterization on [-r, r + α] puts the corner at 0 and the arc on (r, r + α] — so the curve is traversed from the far end of the incoming radius, not from the corner.

The geometry and closure hold for 0 ≤ r and 0 ≤ α, with r = 0 and α = 0 degenerate rather than ill-formed; only the winding number needs 0 < r, so that the arc avoids its centre. For negative r or α the two parameter intervals reverse and this description does not apply.

Its generalized winding number about its own corner is α / 2π — the value HW (2.4) attaches to a corner of interior angle α when 0 < α < 2π, and the source of the ½ at a smooth crossing and the 1/6 at a π/3 corner. Outside that range the formula still holds but the corner reading does not: at α = 0 the two radii coincide, and for α ≥ 2π the arc wraps, so the curve is a multi-turn swept arc rather than a sector.

The two radial segments are packaged as a single twoRayCorner, since neither has a principal value on its own; the arc is a reparametrised circleMap.

Main definitions

• TauCeti.Contour.modelSector — the model sector, on [-r, r + α] with the corner at parameter 0; closed when 0 ≤ r and 0 ≤ α. The winding number needs 0 < r, so that the arc avoids its centre.

Main results

• TauCeti.Contour.windingNumber_closedModelSector — its winding number about z₀ is α / 2π, for every 0 ≤ α. This is the roadmap's acceptance criterion.
• TauCeti.Contour.windingNumber_closedModelSector_eq_half and TauCeti.Contour.windingNumber_closedModelSector_eq_one_div_six — the ½ at a smooth crossing and the 1/6 at a π/3 corner, the two values the valence formula consumes.

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.modelSector (z₀ : ℂ) (r φ α : ℝ) : ℝ → ℂ

The Hungerbühler–Wasem model sector of radius r and opening angle α at z₀, with the incoming radius at angle φ + α and the outgoing one at angle φ.

For 0 ≤ r and 0 ≤ α: on [-r, r] it is the two-ray corner through z₀, running from z₀ + r e^{i(φ+α)} in to z₀ and back out to z₀ + r e^{iφ}; on [r, r + α] it is the arc of radius r from angle φ to φ + α, returning to the start. At r = 0 or α = 0 the corresponding piece degenerates to a point. For negative r or α the two intervals reverse and the branches no longer line up that way.

Equations

• TauCeti.Contour.modelSector z₀ r φ α t = if t ≤ r then TauCeti.Contour.twoRayCorner z₀ (Complex.exp (↑(φ + α) * Complex.I)) (Complex.exp (↑φ * Complex.I)) t else circleMap z₀ r (φ + (t - r))

@[simp]

theorem TauCeti.Contour.modelSector_of_le {z₀ : ℂ} {r φ α t : ℝ} (ht : t ≤ r) : modelSector z₀ r φ α t = twoRayCorner z₀ (Complex.exp (↑(φ + α) * Complex.I)) (Complex.exp (↑φ * Complex.I)) t

Pointwise value of the model sector on the corner interval.

@[simp]

theorem TauCeti.Contour.modelSector_of_lt {z₀ : ℂ} {r φ α t : ℝ} (ht : r < t) : modelSector z₀ r φ α t = circleMap z₀ r (φ + (t - r))

Pointwise value of the model sector on the arc interval.

theorem TauCeti.Contour.modelSector_neg (z₀ : ℂ) {r : ℝ} (hr : 0 ≤ r) (φ α : ℝ) : modelSector z₀ r φ α (-r) = circleMap z₀ r (φ + α)

The model sector starts at the outer end of the incoming radius.

@[simp]

theorem TauCeti.Contour.modelSector_add (z₀ : ℂ) {r : ℝ} (hr : 0 ≤ r) (φ : ℝ) {α : ℝ} (hα : 0 ≤ α) : modelSector z₀ r φ α (r + α) = circleMap z₀ r (φ + α)

The model sector ends at the outer end of the incoming radius, the same point it started from.

theorem TauCeti.Contour.modelSector_closed (z₀ : ℂ) {r : ℝ} (hr : 0 ≤ r) (φ : ℝ) {α : ℝ} (hα : 0 ≤ α) : modelSector z₀ r φ α (-r) = modelSector z₀ r φ α (r + α)

The model sector is a closed curve for 0 ≤ r and 0 ≤ α.

theorem TauCeti.Contour.modelSector_eqOn_corner (z₀ : ℂ) {r : ℝ} (hr : 0 ≤ r) (φ α : ℝ) : Set.EqOn (twoRayCorner z₀ (Complex.exp (↑(φ + α) * Complex.I)) (Complex.exp (↑φ * Complex.I))) (modelSector z₀ r φ α) (Set.uIoo (-r) r)

On the corner interval the model sector is its two-ray corner.

theorem TauCeti.Contour.modelSector_eqOn_arc (z₀ : ℂ) (r φ : ℝ) {α : ℝ} (hα : 0 ≤ α) : Set.EqOn (circleMap z₀ r ∘ fun (t : ℝ) => 1 * t + (φ - r)) (modelSector z₀ r φ α) (Set.uIoo r (r + α))

On the arc interval the model sector is the reparametrised circle map.

theorem TauCeti.Contour.continuous_modelSector {z₀ : ℂ} {r : ℝ} (hr : 0 ≤ r) (φ α : ℝ) : Continuous (modelSector z₀ r φ α)

The model sector is continuous: the two-ray corner and circular arc agree at their join.

theorem TauCeti.Contour.isPiecewiseC1On_modelSector {z₀ : ℂ} {r : ℝ} (hr : 0 ≤ r) (φ α : ℝ) : IsPiecewiseC1On (modelSector z₀ r φ α) (-r) (r + α)

The model sector is piecewise C¹. For nonnegative radius it is affine on the two rays and smoothly parametrized on the circular arc, with corners only at the parameters 0 and r. The opening angle is unconstrained: for α < 0 the parameter interval reverses, but the curve is still built from the same three pieces.

@[simp]

theorem TauCeti.Contour.windingNumber_closedModelSector {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (φ : ℝ) {α : ℝ} (hα : 0 ≤ α) : windingNumber (modelSector z₀ r φ α) (-r) (r + α) z₀ = ↑α / (2 * ↑Real.pi)

The swept-arc curve has winding number α / 2π about its corner. The two radial segments contribute nothing and the arc contributes its swept angle.

This holds for every 0 ≤ α, and is the roadmap's acceptance criterion. The curve is the Hungerbühler–Wasem model sector of interior angle α only for 0 < α < 2π: at α = 0 the two radii coincide, and at α ≥ 2π the arc wraps — α = 4π traverses the circle twice, giving winding 2. At both ends the formula stands; it is the corner reading that lapses.

theorem TauCeti.Contour.windingNumber_closedModelSector_eq_half {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (φ : ℝ) : windingNumber (modelSector z₀ r φ Real.pi) (-r) (r + Real.pi) z₀ = 1 / 2

A smooth crossing contributes winding ½ — the α = π model sector (HW (2.4)). This is the coefficient of ord_i f in the valence formula: at the smooth boundary point i the contour indents by a semicircle.

theorem TauCeti.Contour.windingNumber_closedModelSector_eq_one_div_six {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (φ : ℝ) : windingNumber (modelSector z₀ r φ (Real.pi / 3)) (-r) (r + Real.pi / 3) z₀ = 1 / 6

A π/3 corner contributes winding 1/6 — the α = π/3 model sector (HW (2.4)). The two such corners ρ and ρ + 1 of the fundamental domain sum to the 1/3 coefficient of ord_ρ f.