The model sector's crossing angle is its opening angle

TauCeti.Contour.crossingAngle reads the opening angle at a crossing off the two one-sided tangent limits, and TauCeti.Contour.windingNumber_closedModelSector gives the model sector of opening α winding number α / 2π about its corner. Nothing connected the two: the winding value was stated in terms of the parameter α, and the crossing angle in terms of tangents, with no theorem saying they agree.

This file supplies that bridge. crossingAngle_modelSector holds for every real α: the crossing angle at the corner is the [0, 2π) normalisation of α, which is α itself exactly when 0 ≤ α < 2π. Under those bounds, windingNumber_closedModelSector_eq_crossingAngle_div_two_pi then restates the winding number about the corner as the crossing angle over 2π, with no reference to the parametrisation.

That is the shape a general curve can be compared against, since a curve is tangent to a model sector without being equal to one.

Main declarations

• TauCeti.Contour.crossingAngle_modelSector: the model sector of opening α has crossing angle α at its corner — stated for every real α as the [0, 2π) normalisation of α, which is α itself exactly when 0 ≤ α < 2π.
• TauCeti.Contour.windingNumber_closedModelSector_eq_crossingAngle_div_two_pi: hence its winding number about the corner is crossingAngle / (2π).

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 — the model sector is their equation (2.4), and the crossing-angle reading of its index is what this file supplies.

@[simp]

theorem TauCeti.Contour.crossingAngle_modelSector {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (φ α : ℝ) : crossingAngle (modelSector z₀ r φ α) 0 = toIcoMod Real.two_pi_pos 0 α

The model sector's crossing angle is its opening angle. At the corner the incoming tangent is -exp((φ + α)i) and the outgoing one is exp(φ i), so the normalised angle from the exit ray to the reversed entry ray is α itself — for 0 ≤ α < 2π, the range on which the opening angle determines the sector.

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

The model sector's winding number, read off its crossing angle. Combining windingNumber_closedModelSector with crossingAngle_modelSector: the winding number about the corner is the crossing angle over 2π, with no reference to the parametrisation.