Interior Winding Number

The generalized winding number of the fundamental domain boundary around any strict interior point equals -1.

Main Results

• fdBoundary_H_avoids_interior — the boundary at height H never passes through a strict interior point
• gWN_fdBoundary_H_eq_neg_one_of_interior — gWN = -1 for interior points with im < heightCutoff
• gWN_fdBoundary_H_eq_neg_one_of_strictInterior — gWN = -1 for any strict interior point with im < H

theorem fdBoundary_H_avoids_interior (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (_hp_im_pos : 0 < p.im) {H : ℝ} (hp_im : p.im < H) (t : ℝ) : t ∈ Set.Icc 0 5 → fdBoundaryH H t ≠ p

The boundary at height H avoids any strict interior point p with ‖p‖ > 1, |re p| < 1/2, im p > 0, im p < H.

theorem generalizedWindingNumber_fdBoundary_eq_neg_one (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < heightCutoff) : generalizedWindingNumber' fdBoundary 0 5 p = -1

The winding number of the fixed boundary fdBoundary around an interior point p is -1.

theorem generalizedWindingNumber_fdBoundary_eq_neg_one_uhp (s : UpperHalfPlane) (hs_norm : ‖↑s‖ > 1) (hs_re : |(↑s).re| < 1 / 2) (hs_im : (↑s).im < heightCutoff) : generalizedWindingNumber' fdBoundary 0 5 ↑s = -1

Variant for upper half-plane points.

theorem gWN_fdBoundary_H_eq_neg_one_of_interior (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) (hp_im : p.im < heightCutoff) {H : ℝ} (hH : heightCutoff ≤ H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 p = -1

For interior points with im < heightCutoff, the generalized winding number of fdBoundaryH around p is -1 for any H ≥ heightCutoff.

theorem gWN_fdBoundary_H_eq_neg_one_of_strictInterior (p : ℂ) (hp_norm : ‖p‖ > 1) (hp_re : |p.re| < 1 / 2) (hp_im_pos : 0 < p.im) {H : ℝ} (hH : heightCutoff ≤ H) (hp_im : p.im < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 p = -1

For any strict interior point with im < H, the generalized winding number of fdBoundaryH around p is -1. Requires H ≥ heightCutoff.