Proximity invariance of the winding number

Two closed curves that stay closer to each other than the first one stays to w have the same winding number about w. This is the "dog on a leash" principle: the leash from γ₀ t to γ₁ t is too short to reach w, so the two walks encircle w the same number of times.

The proof compares the two curves through the quotient σ t = (γ₁ t - w) / (γ₀ t - w). The hypothesis says exactly that ‖σ t - 1‖ < 1, so σ runs inside the open right half-plane; its own winding number about 0 therefore vanishes, because the closed left half-plane is an unbounded connected subset of the complement of its image. Since the index integrands satisfy σ' / σ = γ₁' / (γ₁ - w) - γ₀' / (γ₀ - w) pointwise, that vanishing is the asserted equality.

The Layer 0 item this serves is homotopy invariance of the winding number off the curve. Contour.IsPiecewiseC1On.windingNumber_eq_of_notMem_segment deduces invariance along the straight-line homotopy s ↦ (1 - s) • γ₀ + s • γ₁ from the purely geometric hypothesis that the segment [γ₀ t, γ₁ t] misses w for every parameter t: the intermediate curves are piecewise C¹ because that predicate is stable under affine combinations, and a compactness estimate lets finitely many of them be chained together by the leash lemma.

Main results

• Contour.windingNumber_eq_of_dist_lt_dist — the raw-hypothesis form: closed curves that are continuous, differentiable off a countable set, and have interval-integrable derivatives, with dist (γ₁ t) (γ₀ t) < dist (γ₀ t) w throughout, have equal winding numbers about w.
• Contour.IsPiecewiseC1On.windingNumber_eq_of_dist_lt_dist — the same for closed piecewise-C¹ curves, whose regularity supplies the raw hypotheses on its own.
• Contour.IsPiecewiseC1On.windingNumber_eq_of_dist_lt_dist_of_eq_endpoints — the common-endpoint version for paths that need not be closed.
• Contour.IsPiecewiseC1On.windingNumber_eq_of_notMem_segment — invariance along the straight-line homotopy: if w ∉ [γ₀ t, γ₁ t] for every t, the winding numbers agree.

Provenance

The comparison-quotient argument is the standard proof of the "dog on a leash" lemma (equivalently, the homotopy form of Rouché's theorem); see the references in the Contour Integration roadmap, e.g. L. Ahlfors, Complex Analysis, Ch. 4. No formal source is vendored.

theorem TauCeti.Contour.windingNumber_eq_of_dist_lt_dist {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {w : ℂ} {P : Set ℝ} (hP : P.Countable) (h₀closed : γ₀ a = γ₀ b) (h₁closed : γ₁ a = γ₁ b) (h₀cont : ContinuousOn γ₀ (Set.uIcc a b)) (h₁cont : ContinuousOn γ₁ (Set.uIcc a b)) (h₀diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ₀ t) (h₁diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ₁ t) (h₀int : IntervalIntegrable (fun (t : ℝ) => deriv γ₀ t) MeasureTheory.volume a b) (h₁int : IntervalIntegrable (fun (t : ℝ) => deriv γ₁ t) MeasureTheory.volume a b) (hlt : ∀ t ∈ Set.uIcc a b, dist (γ₁ t) (γ₀ t) < dist (γ₀ t) w) : windingNumber γ₁ a b w = windingNumber γ₀ a b w

Proximity invariance of the winding number (the "dog on a leash" lemma). Let γ₀ and γ₁ be closed curves on the oriented interval with endpoints a, b, each continuous on Set.uIcc a b, differentiable off a common countable set P, and with interval-integrable derivative. If at every parameter the two curves are closer to each other than γ₀ is to w, then they have the same winding number about w.

theorem TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_of_dist_lt_dist {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (h₀ : IsPiecewiseC1On γ₀ a b) (h₁ : IsPiecewiseC1On γ₁ a b) (h₀closed : γ₀ a = γ₀ b) (h₁closed : γ₁ a = γ₁ b) (hlt : ∀ t ∈ Set.uIcc a b, dist (γ₁ t) (γ₀ t) < dist (γ₀ t) w) : windingNumber γ₁ a b w = windingNumber γ₀ a b w

Proximity invariance for closed piecewise-C¹ curves. If two closed piecewise-C¹ curves stay closer to each other than the first stays to w, they have the same winding number about w. Piecewise-C¹ regularity supplies the continuity, differentiability and integrability hypotheses of windingNumber_eq_of_dist_lt_dist.

theorem TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_of_dist_lt_dist_of_eq_endpoints {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (h₀ : IsPiecewiseC1On γ₀ a b) (h₁ : IsPiecewiseC1On γ₁ a b) (ha : γ₀ a = γ₁ a) (hb : γ₀ b = γ₁ b) (hlt : ∀ t ∈ Set.uIcc a b, dist (γ₁ t) (γ₀ t) < dist (γ₀ t) w) : windingNumber γ₁ a b w = windingNumber γ₀ a b w

Proximity invariance for paths with common endpoints. If two piecewise-C¹ paths agree at both endpoints and stay closer to each other than the first stays to w, then they have the same winding number about w. Unlike IsPiecewiseC1On.windingNumber_eq_of_dist_lt_dist, the paths need not be closed; their common endpoints make the comparison quotient a closed curve.

theorem TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_of_notMem_segment {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (h₀ : IsPiecewiseC1On γ₀ a b) (h₁ : IsPiecewiseC1On γ₁ a b) (h₀closed : γ₀ a = γ₀ b) (h₁closed : γ₁ a = γ₁ b) (hseg : ∀ t ∈ Set.uIcc a b, w ∉ segment ℝ (γ₀ t) (γ₁ t)) : windingNumber γ₁ a b w = windingNumber γ₀ a b w

Invariance of the winding number along a straight-line homotopy. If for every parameter t the segment from γ₀ t to γ₁ t misses w, then the two closed piecewise-C¹ curves have the same winding number about w.

No regularity of the homotopy is assumed. The intermediate curves (1 - s) • γ₀ + s • γ₁ are piecewise C¹ because that predicate is stable under affine combinations; a compactness argument bounds their distance to w below by a positive m and the displacement ‖γ₁ - γ₀‖ above by some M; and the N + 1 stages k / N with M / N < m are then chained together by IsPiecewiseC1On.windingNumber_eq_of_dist_lt_dist.