Winding Number: Definitions and Simple Results

Definitions for generalized winding numbers of piecewise C¹ curves, including the Hungerbühler-Wasem angle-based approach.

Main Definitions

• angleAtCrossing — angle at a crossing point where γ passes through z₀
• windingNumberWithAngles' — winding number via explicit angle sum
• PiecewiseC1Immersion.translate — translate an immersion
• externalWindingContribution — winding from the curve's global topology

Main Results

• windingNumber_smooth_crossing — smooth crossing contributes 1/2
• windingNumber_corner_crossing — corner with angle α contributes α/(2π)
• angleAtCrossing_translate — translation invariance of crossing angle

noncomputable def angleAtCrossing (γ : PiecewiseC1Immersion) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) : ℝ

The angle at a crossing point where γ passes through z₀. arg(L_out) - arg(-L_in) where L_in and L_out are one-sided derivative limits. At smooth points (not in partition), returns π.

Equations

• angleAtCrossing γ t₀ ht₀ = if h : t₀ ∈ γ.partition then have L_left := Classical.choose ⋯; have L_right := Classical.choose ⋯; L_right.arg - (-L_left).arg else Real.pi

theorem angleAtCrossing_smooth (γ : PiecewiseC1Immersion) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hsmooth : t₀ ∉ γ.partition) : angleAtCrossing γ t₀ ht₀ = Real.pi

noncomputable def windingNumberWithAngles' (γ : PiecewiseC1Immersion) (z₀ : ℂ) (crossings : Finset ℝ) (hcrossings_in : ∀ t ∈ crossings, t ∈ Set.Ioo γ.a γ.b) (hcrossings_at : ∀ t ∈ crossings, γ.toFun t = z₀) : ℂ

Winding number via explicit angle sum at crossings.

Equations

• windingNumberWithAngles' γ z₀ crossings hcrossings_in hcrossings_at = ∑ t : ↥crossings, ↑(angleAtCrossing γ ↑t ⋯) / (2 * ↑Real.pi)

theorem singleton_mem_Ioo (t₀ a b : ℝ) (ht₀ : t₀ ∈ Set.Ioo a b) (t : ℝ) : t ∈ {t₀} → t ∈ Set.Ioo a b

theorem singleton_at_crossing (γ : PiecewiseC1Immersion) (t₀ : ℝ) (z₀ : ℂ) (hcross : γ.toFun t₀ = z₀) (t : ℝ) : t ∈ {t₀} → γ.toFun t = z₀

theorem windingNumber_smooth_crossing (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (hsmooth : t₀ ∉ γ.partition) : windingNumberWithAngles' γ z₀ {t₀} ⋯ ⋯ = 1 / 2

A single smooth crossing contributes 1/2 to the winding number.

theorem windingNumber_corner_crossing (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ α : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (hangle : angleAtCrossing γ t₀ ht₀ = α) : windingNumberWithAngles' γ z₀ {t₀} ⋯ ⋯ = ↑α / (2 * ↑Real.pi)

A corner crossing with angle α contributes α/(2π).

theorem cauchyPrincipalValue_eq_classical_off_curve' (γ : PiecewiseC1Curve) (z₀ : ℂ) (hoff : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ z₀) : ∃ δ > 0, ∀ ε < δ, ∀ t ∈ Set.Icc γ.a γ.b, ‖γ.toFun t - z₀‖ > ε

When γ avoids z₀, the PV cutoff is trivial below minimum distance.

theorem integral_inv_real_axis (r ε : ℝ) (hr : 0 < r) (hε : 0 < ε) : ∫ (t : ℝ) in ε..r, (↑t)⁻¹ = Complex.log ↑r - Complex.log ↑ε

def PiecewiseC1Immersion.translate (γ : PiecewiseC1Immersion) (c : ℂ) : PiecewiseC1Immersion

Translate a piecewise C¹ immersion by a constant.

Equations

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

theorem angleAtCrossing_translate (γ : PiecewiseC1Immersion) (c : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) : angleAtCrossing (γ.translate c) t₀ ht₀ = angleAtCrossing γ t₀ ht₀

The angle at a crossing is invariant under translation.

noncomputable def externalWindingContribution (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) : ℂ

The external winding contribution at a single crossing point. For a closed piecewise C¹ immersion passing through z₀ exactly once, this measures the winding of the curve around z₀ apart from the local crossing angle. Mathematically, this is the classical winding number of the modified curve Λ that detours around z₀ (H-W Proposition 2.2).

The decomposition is n_{z₀}(γ) = N - α/(2π), so N = n_{z₀}(γ) + α/(2π). When N = 0, the generalized winding number equals -α/(2π).

Equations

• externalWindingContribution γ z₀ t₀ ht₀ = generalizedWindingNumber' γ.toFun γ.a γ.b z₀ + ↑(angleAtCrossing γ t₀ ht₀) / (2 * ↑Real.pi)