The winding number is locally constant off a closed curve

For a closed curve γ (so γ a = γ b) that is continuous on Set.uIcc a b, differentiable off a countable set, with interval-integrable derivative, the generalized winding number fun w ↦ windingNumber γ a b w, viewed as a function on the points off the curve, is locally constant (isLocallyConstant_windingNumber_of_closed). It is the ingredient Dixon's argument uses for the homology form of Cauchy's theorem (roadmap homologyCauchyTheorem). As a corollary, the winding number is constant on every connected component of the curve complement. Also, exists_ball_windingNumber_zero packages the local matching data Dixon needs: around an off-curve point where the winding number vanishes, it vanishes on a whole ball that stays off the curve.

Main results

• TauCeti.Contour.isLocallyConstant_windingNumber_of_closed — the winding number is locally constant on the complement of a closed curve.
• TauCeti.Contour.windingNumber_eq_of_mem_connectedComponentIn — the winding number is constant on each connected component of the curve complement.
• TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_of_mem_connectedComponentIn — the direct piecewise-C¹ form.
• TauCeti.Contour.exists_ball_windingNumber_zero — around an off-curve point where the winding number vanishes, it vanishes on a whole ball that stays off the curve.

Provenance

Adapted from generalizedWindingNumber_locally_const_of_closed in WindingArgDiff.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval with endpoints a and b.

theorem TauCeti.Contour.eq_of_dist_intCast_lt_one {m n : ℤ} (h : dist ↑m ↑n < 1) : m = n

Two integers whose complex images are closer than 1 are equal.

theorem TauCeti.Contour.isLocallyConstant_windingNumber_of_closed {γ : ℝ → ℂ} {a b : ℝ} {P : Set ℝ} (hclosed : γ a = γ b) (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) : IsLocallyConstant fun (w : { w : ℂ // ∀ t ∈ Set.uIcc a b, γ t ≠ w }) => windingNumber γ a b ↑w

The winding number is locally constant off a closed curve. Let γ be a closed curve (γ a = γ b), differentiable off a countable set P, continuous on Set.uIcc a b, with interval-integrable derivative. Then, as a function of the point ranging over the complement of the curve, the generalized winding number fun w ↦ windingNumber γ a b w is locally constant.

theorem TauCeti.Contour.windingNumber_eq_of_mem_connectedComponentIn {γ : ℝ → ℂ} {a b : ℝ} {P : Set ℝ} (hclosed : γ a = γ b) (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) {w₀ w₁ : ℂ} (hw₁ : w₁ ∈ connectedComponentIn (γ '' Set.uIcc a b)ᶜ w₀) : windingNumber γ a b w₁ = windingNumber γ a b w₀

The winding number is constant on a connected component of the curve complement. For a closed curve that is continuous on [[a, b]], differentiable away from a countable set, and has interval-integrable derivative, two points in the same connected component of ℂ \ γ '' [[a, b]] have the same winding number.

This is the connected-component form of homotopy invariance in the point: it follows from local constancy of the integer-valued winding number off the curve.

theorem TauCeti.Contour.IsPiecewiseC1On.windingNumber_eq_of_mem_connectedComponentIn {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) {w₀ w₁ : ℂ} (hw₁ : w₁ ∈ connectedComponentIn (γ '' Set.uIcc a b)ᶜ w₀) : windingNumber γ a b w₁ = windingNumber γ a b w₀

Piecewise-C¹ form of componentwise constancy. For a closed piecewise-C¹ curve, two points in the same connected component of the curve complement have the same winding number.

theorem TauCeti.Contour.exists_ball_windingNumber_zero {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} (hclosed : γ a = γ b) (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (hw_zero : windingNumber γ a b w = 0) : ∃ ε > 0, ∀ w' ∈ Metric.ball w ε, (∀ t ∈ Set.uIcc a b, γ t ≠ w') ∧ windingNumber γ a b w' = 0

The winding number vanishes on a ball around an off-curve null point. For a closed curve γ (differentiable off a countable set, continuous on uIcc a b, with interval-integrable derivative), if the winding number about an off-curve point w is 0, then it is 0 throughout a ball around w that stays off the curve. This is the local matching input for Dixon's argument: the off-curve set is open, so the subtype-open set on which local constancy pins the winding number to 0 pushes forward, along the open inclusion Subtype.val, to a ℂ-ball.