Homotopy Invariance of Winding Numbers

Homotopy invariance for generalized winding numbers (both piecewise C¹ and smooth), plus the classical winding number formula for curves avoiding a point.

Main Results

• windingNumber_eq_of_piecewise_homotopic — winding number invariant under piecewise homotopy
• windingNumber_eq_of_homotopic_closed — winding number invariant under smooth homotopy
• generalizedWindingNumber_eq_classical_away — PV winding number equals classical integral when curve avoids z₀
• contourIntegral_eq_of_homotopic — contour integrals equal under homotopy for holomorphic integrands

theorem windingNumber_eq_of_piecewise_homotopic (γ₀ γ₁ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (P : Finset ℝ) (hab : a < b) (hhom : PiecewiseCurvesHomotopicAvoiding γ₀ γ₁ a b z₀ P) : generalizedWindingNumber' γ₀ a b z₀ = generalizedWindingNumber' γ₁ a b z₀

Winding number is invariant under piecewise C¹ homotopy.

theorem windingNumber_eq_of_homotopic_closed (γ₀ γ₁ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (hab : a < b) (hhom : ClosedCurvesHomotopicAvoiding γ₀ γ₁ a b z₀) : generalizedWindingNumber' γ₀ a b z₀ = generalizedWindingNumber' γ₁ a b z₀

Winding number is invariant under smooth homotopy.

theorem generalizedWindingNumber_eq_classical_away (γ : PiecewiseC1Curve) (z₀ : ℂ) (hoff : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ z₀) : generalizedWindingNumber' γ.toFun γ.a γ.b z₀ = (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (t : ℝ) in γ.a..γ.b, (γ.toFun t - z₀)⁻¹ * deriv γ.toFun t

When γ avoids z₀, the PV winding number equals the classical contour integral.

theorem contourIntegral_eq_of_homotopic (f : ℂ → ℂ) (γ₀ γ₁ : ℝ → ℂ) (a b : ℝ) (hab : a < b) (_hγ₀_cont : ContinuousOn γ₀ (Set.Icc a b)) (_hγ₁_cont : ContinuousOn γ₁ (Set.Icc a b)) (_hγ₀_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ γ₀ t) (_hγ₁_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ γ₁ t) (H : ℝ × ℝ → ℂ) (_hH_cont : Continuous H) (hH0 : ∀ t ∈ Set.Icc a b, H (t, 0) = γ₀ t) (hH1 : ∀ t ∈ Set.Icc a b, H (t, 1) = γ₁ t) (_hH_ends : ∀ s ∈ Set.Icc 0 1, H (a, s) = γ₀ a ∧ H (b, s) = γ₀ b) (hf_holo : ∀ t ∈ Set.Icc a b, ∀ s ∈ Set.Icc 0 1, DifferentiableAt ℂ f (H (t, s))) (hfH_cont : Continuous (f ∘ H)) (hH_smooth : ContDiff ℝ 2 H) (hH_deriv_s_zero_at_ends : ∀ s ∈ Set.Icc 0 1, deriv (fun (s' : ℝ) => H (a, s')) s = 0 ∧ deriv (fun (s' : ℝ) => H (b, s')) s = 0) (hf_differentiable : Differentiable ℂ f) : ∫ (t : ℝ) in a..b, f (γ₀ t) * deriv γ₀ t = ∫ (t : ℝ) in a..b, f (γ₁ t) * deriv γ₁ t

Contour integrals of a holomorphic function are equal along homotopic curves.