Decomposition of the winding number of the boundary contour

For a point off the boundary path fdBoundary H — the contour that traces the boundary of the truncated fundamental domain once the height parameter satisfies 1 < H — the winding number over the full parameter interval [0, 5] splits as the sum of the winding numbers of the four smooth pieces: the right vertical, the arc, the left vertical, and the truncation ceiling. The statements hold for arbitrary H. This is the entry point for evaluating the winding number at interior points piece by piece.

The single-point Cauchy principal values required by the partition additivity are supplied by avoidance: away from the contour the index integrand has no singularity, and its integrability follows from the piecewise-C¹ regularity of the contour.

Main declarations

• TauCeti.ModularForm.cauchyPVExistsAt_fdBoundary
• TauCeti.ModularForm.windingNumber_fdBoundary_eq_sum_pieces

theorem TauCeti.ModularForm.cauchyPVExistsAt_fdBoundary {H : ℝ} {w : ℂ} (c d : ℝ) (hc : c ∈ Set.Icc 0 5) (hd : d ∈ Set.Icc 0 5) (hw : ∀ t ∈ Set.uIcc c d, fdBoundary H t ≠ w) : Contour.CauchyPVExistsAt (fdBoundary H) c d (fun (z : ℂ) => (z - w)⁻¹) w

The single-point Cauchy principal value of the index integrand exists on any parameter subinterval of the boundary path avoiding w: the integrand is then singularity-free, and integrable by piecewise-C¹ regularity.

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_sum_pieces {H : ℝ} {w : ℂ} (hw : ∀ t ∈ Set.Icc 0 5, fdBoundary H t ≠ w) : Contour.windingNumber (fdBoundary H) 0 5 w = Contour.windingNumber (fdBoundary H) 0 1 w + Contour.windingNumber (fdBoundary H) 1 3 w + Contour.windingNumber (fdBoundary H) 3 4 w + Contour.windingNumber (fdBoundary H) 4 5 w

The winding number of the boundary path about a point off it is the sum of the winding numbers of its four smooth pieces: the right vertical, the arc, the left vertical, and the truncation ceiling. This instantiates the finite-partition additivity Contour.windingNumber_eq_sum_range at the junction partition 0, 1, 3, 4, 5.