The winding number of a point-avoiding arc exponentiates to its endpoint ratio

For a curve γ on the oriented interval with endpoints a, b that avoids w, the generalized winding number n_w(γ) = windingNumber γ a b w is an ordinary index integral, and

exp (2πi · n_w(γ)) = (γ b - w) / (γ a - w).

This one identity carries the whole polar bookkeeping of the index integral. Its modulus records the imaginary part of the winding number, Im n_w(γ) = (log ‖γ a - w‖ - log ‖γ b - w‖) / 2π — so the winding number of an open arc is real exactly when its two endpoints are equidistant from w. Its argument records the real part modulo 1: 2π · Re n_w(γ) = arg (γ b - w) - arg (γ a - w) in Real.Angle. Closing the curve (γ a = γ b) makes the right-hand side 1, which is the integrality of the winding number off the curve (exists_int_windingNumber_of_closed, now a three-line corollary).

The identity is the mod-1 bookkeeping that Hungerbühler–Wasem Proposition 2.2 telescopes. There a closed piecewise-C¹ immersion Λ is cut at the finitely many parameters where it meets z₀ (IsPwC1ImmersionOn.finite_crossings), and the real part of the winding number of each avoiding piece is pinned modulo 1 by the directions of Λ - z₀ at the two ends of that piece — directions that tendsto_normalize_sub_nhdsGT and tendsto_normalize_sub_nhdsLT identify with the outgoing and reversed incoming tangents, that is with the summands of crossingAngle. Summing the pieces around the closed curve is what turns the endpoint arguments into n_{z₀}(Λ) - Σ_ℓ crossingAngle Λ t_ℓ / 2π ∈ ℤ; that conclusion is TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_sum_crossingAngle, which uses the piecewise-C¹ endpoint-ratio identity below for its avoiding pieces.

Main results

• TauCeti.Contour.exp_two_pi_I_mul_windingNumber_of_avoidance — the endpoint-ratio identity.
• TauCeti.Contour.IsPiecewiseC1On.exp_two_pi_I_mul_windingNumber — the same for a piecewise-C¹ curve, whose regularity supplies the raw hypotheses on its own.
• TauCeti.Contour.im_windingNumber_of_avoidance and its piecewise-C¹ form — the imaginary part of the winding number of an arc is the log-modulus decrement of its endpoints, over 2π.
• TauCeti.Contour.coe_two_pi_mul_re_windingNumber_eq_arg_sub_arg_of_avoidance and its piecewise-C¹ form — the real part of the winding number, read modulo 1 as a Real.Angle, is the argument change between the endpoint directions.

Provenance

The argument-lift partition and the segment-sum evaluation of the index integral are the ones already used for winding-number integrality; the private endpoint-sum lemmas below were factored out of Winding/Integer.lean, whose closed-curve statement is now derived from the identity proved here.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, Definition 2.1 and Proposition 2.2.

theorem TauCeti.Contour.exp_two_pi_I_mul_windingNumber_of_avoidance {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) : Complex.exp (2 * ↑Real.pi * Complex.I * windingNumber γ a b w) = (γ b - w) / (γ a - w)

The winding number of a point-avoiding arc exponentiates to its endpoint ratio. For a curve γ on the oriented interval with endpoints a, b that is continuous on Set.uIcc a b, differentiable off a countable set P, avoids w throughout Set.uIcc a b, and has an interval-integrable index integrand (γ · - w)⁻¹ * deriv γ,

exp (2πi · windingNumber γ a b w) = (γ b - w) / (γ a - w).

Both the modulus and the argument of the winding number are read off this identity, by im_windingNumber_of_avoidance and coe_two_pi_mul_re_windingNumber_eq_arg_sub_arg_of_avoidance.

theorem TauCeti.Contour.IsPiecewiseC1On.exp_two_pi_I_mul_windingNumber {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) : Complex.exp (2 * ↑Real.pi * Complex.I * windingNumber γ a b w) = (γ b - w) / (γ a - w)

Piecewise-C¹ form of the endpoint-ratio identity. Piecewise-C¹ regularity supplies the continuity, differentiability and integrability hypotheses of exp_two_pi_I_mul_windingNumber_of_avoidance.

theorem TauCeti.Contour.im_windingNumber_of_avoidance {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) : (windingNumber γ a b w).im = (Real.log ‖γ a - w‖ - Real.log ‖γ b - w‖) / (2 * Real.pi)

The imaginary part of the winding number of an arc. Under the hypotheses of exp_two_pi_I_mul_windingNumber_of_avoidance, the modulus of the endpoint ratio gives

Im (windingNumber γ a b w) = (log ‖γ a - w‖ - log ‖γ b - w‖) / 2π.

So the winding number of an open arc is real precisely when its endpoints are equidistant from w; a closed curve is the special case where they coincide.

theorem TauCeti.Contour.IsPiecewiseC1On.im_windingNumber {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) : (windingNumber γ a b w).im = (Real.log ‖γ a - w‖ - Real.log ‖γ b - w‖) / (2 * Real.pi)

Piecewise-C¹ form of the imaginary-part formula.

theorem TauCeti.Contour.coe_two_pi_mul_re_windingNumber_eq_arg_sub_arg_of_avoidance {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) : ↑(2 * Real.pi * (windingNumber γ a b w).re) = ↑(γ b - w).arg - ↑(γ a - w).arg

The real part of the winding number of an arc, modulo 1. Under the hypotheses of exp_two_pi_I_mul_windingNumber_of_avoidance, the argument of the endpoint ratio gives

2π · Re (windingNumber γ a b w) = arg (γ b - w) - arg (γ a - w) in Real.Angle,

so the real part of the winding number of an arc is determined modulo 1 by the directions of γ - w at its two endpoints, while the endpoint norms determine its imaginary part. This is the bookkeeping that telescopes around a closed curve cut at its crossings (Hungerbühler–Wasem Proposition 2.2); the statement is an equality of Real.Angles because arg is additive only modulo 2π.

theorem TauCeti.Contour.IsPiecewiseC1On.coe_two_pi_mul_re_windingNumber {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) : ↑(2 * Real.pi * (windingNumber γ a b w).re) = ↑(γ b - w).arg - ↑(γ a - w).arg

Piecewise-C¹ form of the modulo-1 reading of the winding number.