Winding Number Integrality

Definitions for piecewise and smooth homotopies, plus the exp trick proof that winding numbers of closed curves avoiding a point are integers.

Main Definitions

• PiecewiseCurvesHomotopicAvoiding — piecewise C¹ homotopy avoiding z₀
• ClosedCurvesHomotopicAvoiding — smooth closed homotopy avoiding z₀

Main Results

• windingNumber_integer_of_piecewise_closed_avoiding — winding number is an integer for piecewise C¹ closed curves
• windingNumber_integer_of_closed_avoiding — winding number is an integer for smooth closed curves
• exp_integral_eq_endpoint_ratio — exponential of the log-derivative integral equals endpoint ratio
• integral_closed_curve_eq_two_pi_int — closed curve integral is 2πi times an integer

def PiecewiseCurvesHomotopicAvoiding (γ₀ γ₁ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (P : Finset ℝ) : Prop

Piecewise C¹ homotopy between closed curves (i.e. γ₀ a = γ₀ b and γ₁ a = γ₁ b) avoiding z₀, where P is the finite partition set of points at which the derivative of the homotopy may be discontinuous or undefined.

Use this when working with closed piecewise-smooth curves; it is strictly stronger than CurvesHomotopicAvoiding (which handles open-endpoint curves fixed at z₀) but weaker than ClosedCurvesHomotopicAvoiding (which requires a globally continuous derivative without a partition).

Equations

• One or more equations did not get rendered due to their size.

def ClosedCurvesHomotopicAvoiding (γ₀ γ₁ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : Prop

Smooth closed homotopy between closed curves avoiding z₀.

This is the strongest of the four homotopy notions: the homotopy H is everywhere continuously differentiable (no partition needed). Use this when the curves and homotopy are genuinely smooth; it implies PiecewiseCurvesHomotopicAvoiding (via ClosedCurvesHomotopicAvoiding.toPiecewise) but does not directly imply CurvesHomotopicAvoiding, which has a different endpoint condition (endpoints fixed at z₀ rather than identified).

Equations

• One or more equations did not get rendered due to their size.

Conversion lemmas between homotopy definitions

The four homotopy notions form the following hierarchy (stronger → weaker):

ClosedCurvesHomotopicAvoiding
        |
        v  (toPiecewise)
PiecewiseCurvesHomotopicAvoiding   CurvesHomotopicAvoiding
        |                                   ^
        v  (toBasic, when endpoints = z₀)   |
        (structurally different endpoint conditions)

CurvesHomotopicAvoiding (from Basic.lean) requires H(a,s) = z₀ and H(b,s) = z₀ (endpoints are the fixed point z₀), while the Closed/Piecewise variants require H(a,s) = H(b,s) (the curve is merely closed). These are different conditions, so there is no general implication between the two groups.

theorem ClosedCurvesHomotopicAvoiding.toPiecewise {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : ClosedCurvesHomotopicAvoiding γ₀ γ₁ a b z₀) : PiecewiseCurvesHomotopicAvoiding γ₀ γ₁ a b z₀ ∅

A smooth closed homotopy is a piecewise homotopy with empty partition.

The empty partition ∅ means no breakpoints are needed: differentiability holds everywhere in Ioo a b (vacuously, the partition condition is void), and the global continuity of the derivative supplies the required local continuity on every sub-interval. The bound on ‖deriv H‖ is obtained from compactness of Icc a b × Icc 0 1 together with continuity of the derivative.

theorem PiecewiseCurvesHomotopicAvoiding.toBasic {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} {P : Finset ℝ} (h : PiecewiseCurvesHomotopicAvoiding γ₀ γ₁ a b z₀ P) (hpts : ∀ (H : ℝ × ℝ → ℂ), Continuous H → (∀ t ∈ Set.Icc a b, H (t, 0) = γ₀ t) → (∀ t ∈ Set.Icc a b, H (t, 1) = γ₁ t) → ∀ s ∈ Set.Icc 0 1, H (a, s) = z₀ ∧ H (b, s) = z₀) : CurvesHomotopicAvoiding γ₀ γ₁ a b z₀

A piecewise homotopy (forgetting derivative bounds) gives a basic homotopy.

Note: this conversion requires an extra hypothesis hpts asserting that the homotopy H (from h) satisfies H(a,s) = z₀ and H(b,s) = z₀ for all s. This is the endpoint condition required by CurvesHomotopicAvoiding (Basic.lean). The piecewise/closed variants only require H(a,s) = H(b,s) (closed curves), which is a strictly weaker condition — so no hypothesis-free conversion exists.

theorem limUnder_eventually_eq_const {α : Type u_1} {f : α → ℂ} {l : Filter α} {c : ℂ} [l.NeBot] (hf : ∀ᶠ (x : α) in l, f x = c) : l.limUnder f = c

If f is eventually equal to a constant, limUnder equals that constant.

theorem exists_ball_avoiding_finset {P : Finset ℝ} {t : ℝ} (ht : t ∉ P) : ∃ ε > 0, ∀ x ∈ Set.Ioo (t - ε) (t + ε), x ∉ P

At a point not in a finite set, there is an open ball disjoint from the set.

theorem windingNumber_integer_of_piecewise_closed_avoiding (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (P : Finset ℝ) (hab : a < b) (hγ_closed : γ a = γ b) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b, t ∉ P → DifferentiableAt ℝ γ t) (hγ_deriv_cont : ∀ (p₁ p₂ : ℝ), p₁ < p₂ → (∀ t ∈ Set.Ioo p₁ p₂, t ∉ P) → Set.Ioo p₁ p₂ ⊆ Set.Ioo a b → ContinuousOn (deriv γ) (Set.Ioo p₁ p₂)) (hγ_avoids : ∀ t ∈ Set.Icc a b, γ t ≠ z₀) (hγ_deriv_bound_ex : ∃ (M : ℝ), ∀ t ∈ Set.Icc a b, ‖deriv γ t‖ ≤ M) : ∃ (n : ℤ), generalizedWindingNumber' γ a b z₀ = ↑n

theorem exp_integral_eq_endpoint_ratio_piecewise (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (P : Finset ℝ) (hab : a < b) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b, t ∉ P → DifferentiableAt ℝ γ t) (hγ_deriv_cont : ∀ (p₁ p₂ : ℝ), p₁ < p₂ → (∀ t ∈ Set.Ioo p₁ p₂, t ∉ P) → Set.Ioo p₁ p₂ ⊆ Set.Ioo a b → ContinuousOn (deriv γ) (Set.Ioo p₁ p₂)) (hγ_avoids : ∀ t ∈ Set.Icc a b, γ t ≠ z₀) (hγ_deriv_bound : ∃ (M : ℝ), ∀ t ∈ Set.Icc a b, ‖deriv γ t‖ ≤ M) : Complex.exp (∫ (t : ℝ) in a..b, deriv γ t / (γ t - z₀)) = (γ b - z₀) / (γ a - z₀)

Piecewise generalization of exp_integral_eq_endpoint_ratio: for a piecewise C¹ curve avoiding z₀ with bounded derivative, the exponential of the log-derivative integral equals the endpoint ratio. Uses the G-function technique.

theorem winding_integrand_bounded_of_uniform_avoidance {H : ℝ × ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} {δ M : ℝ} (hδ_pos : 0 < δ) (hδ_bound : ∀ t ∈ Set.Icc a b, ∀ s ∈ Set.Icc 0 1, δ ≤ ‖H (t, s) - z₀‖) (hM_bound : ∀ t ∈ Set.Icc a b, ∀ s ∈ Set.Icc 0 1, ‖deriv (fun (t' : ℝ) => H (t', s)) t‖ ≤ M) (t : ℝ) : t ∈ Set.Icc a b → ∀ s ∈ Set.Icc 0 1, ‖(H (t, s) - z₀)⁻¹ * deriv (fun (t' : ℝ) => H (t', s)) t‖ ≤ M / δ

Uniform bound for winding number integrand from homotopy avoidance.

theorem exp_integral_eq_endpoint_ratio (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (hab : a < b) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ γ t) (hγ_avoid : ∀ t ∈ Set.Icc a b, γ t ≠ z₀) (hγ'_cont : ContinuousOn (deriv γ) (Set.Icc a b)) : Complex.exp (∫ (t : ℝ) in a..b, deriv γ t / (γ t - z₀)) = (γ b - z₀) / (γ a - z₀)

theorem windingNumber_integer_of_closed_avoiding (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) (hab : a < b) (hγ_closed : γ a = γ b) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ γ t) (hγ'_cont : ContinuousOn (deriv γ) (Set.Icc a b)) (hγ_avoid : ∀ t ∈ Set.Icc a b, γ t ≠ z₀) : ∃ (n : ℤ), generalizedWindingNumber' γ a b z₀ = ↑n

The winding number of a smooth closed curve avoiding z₀ is an integer.