Unit Arc Winding Number Helpers

Helper lemmas for proving generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1/2 for points s on the unit circle arc of the fundamental domain (‖s‖ = 1, |s.re| < 1/2, s.im > 0).

Contains parameterization, separation, slitPlane conditions, and the FTC value computation.

theorem unitArc_t₀_mem_Ioo (s : ℂ) (hs_re : |s.re| < 1 / 2) (_hs_im_pos : 0 < s.im) : 6 * Real.arccos s.re / Real.pi - 1 ∈ Set.Ioo 1 3

The crossing parameter t₀ = 6·arccos(s.re)/π − 1 lies in (1, 3).

theorem unitArc_fdBoundary_eq (H : ℝ) (s : ℂ) (hs_norm : ‖s‖ = 1) (hs_re : |s.re| < 1 / 2) (hs_im_pos : 0 < s.im) : have t₀ := 6 * Real.arccos s.re / Real.pi - 1; fdBoundaryH H t₀ = s

fdBoundaryH H passes through s at the arc parameter t₀.

theorem unitArc_min_dist_pos (s : ℂ) (_hs_norm : ‖s‖ = 1) (hs_re : |s.re| < 1 / 2) (_hs_im_pos : 0 < s.im) (H : ℝ) (hH : 1 < H) : 0 < min (min (1 / 2 - s.re) (s.re + 1 / 2)) (H - 1)

Minimum separation distance for arc points.

theorem unitArc_min_dist_from_non_arc (H : ℝ) (hH : 1 < H) (s : ℂ) (hs_norm : ‖s‖ = 1) (hs_re : |s.re| < 1 / 2) (_hs_im_pos : 0 < s.im) (t : ℝ) (ht_arc_right : 3 ≤ t) (ht5 : t ≤ 5) : min (min (1 / 2 - s.re) (s.re + 1 / 2)) (H - 1) ≤ ‖fdBoundaryH H t - s‖

Non-arc segments of fdBoundaryH stay at distance ≥ d from arc point s.

theorem unitArc_min_dist_from_seg1 (H : ℝ) (s : ℂ) (hs_re : |s.re| < 1 / 2) (t : ℝ) (ht : t ≤ 1) : 1 / 2 - s.re ≤ ‖fdBoundaryH H t - s‖

Non-arc segments to the LEFT (t ≤ 1) stay at distance ≥ d from arc point s.

theorem unitArc_ratio_eq (t₀ δ : ℝ) (hδ_pos : 0 < δ) (hδ_small : δ < 6) : have g_minus := Complex.exp (↑(Real.pi * (1 + (t₀ - δ)) / 6) * Complex.I) - Complex.exp (↑(Real.pi * (1 + t₀) / 6) * Complex.I); have neg_g_plus := -(Complex.exp (↑(Real.pi * (1 + (t₀ + δ)) / 6) * Complex.I) - Complex.exp (↑(Real.pi * (1 + t₀) / 6) * Complex.I)); g_minus / neg_g_plus = Complex.exp (↑(-(Real.pi * δ / 6)) * Complex.I)

The ratio g(t₀-δ) / (−g(t₀+δ)) = exp(−i·πδ/6) on the arc.

theorem unitArc_ftc_value (H : ℝ) (hH : 1 < H) (s : ℂ) (hs_norm : ‖s‖ = 1) (hs_re : |s.re| < 1 / 2) (hs_im_pos : 0 < s.im) (δ : ℝ) (hδ_pos : 0 < δ) (t₀ : ℝ) (ht₀_Ioo : t₀ ∈ Set.Ioo 1 3) (h_s_arc : s = Complex.exp (↑(Real.pi * (1 + t₀) / 6) * Complex.I)) (hδ_left : 1 < t₀ - δ) (hδ_right : t₀ + δ < 3) : IntervalIntegrable (fun (t : ℝ) => deriv (fun (u : ℝ) => fdBoundaryH H u - s) t / (fdBoundaryH H t - s)) MeasureTheory.volume 0 (t₀ - δ) ∧ IntervalIntegrable (fun (t : ℝ) => deriv (fun (u : ℝ) => fdBoundaryH H u - s) t / (fdBoundaryH H t - s)) MeasureTheory.volume (t₀ + δ) 5 ∧ (∫ (t : ℝ) in 0..t₀ - δ, deriv (fun (u : ℝ) => fdBoundaryH H u - s) t / (fdBoundaryH H t - s)) + ∫ (t : ℝ) in t₀ + δ..5, deriv (fun (u : ℝ) => fdBoundaryH H u - s) t / (fdBoundaryH H t - s) = Complex.log ((fdBoundaryH H (t₀ - δ) - s) / -(fdBoundaryH H (t₀ + δ) - s)) - ↑Real.pi * Complex.I