The generalized winding number (Hungerbühler–Wasem Def 2.1)

For a curve γ : ℝ → ℂ on [a, b] and a point z₀, the generalized winding number windingNumber γ a b z₀ is the principal-value normalization of the index integral (2πi)⁻¹ · PV ∮_γ dz/(z − z₀) (Hungerbühler–Wasem Def 2.1); see windingNumber_eq_integral_of_avoidance for its reduction to the ordinary index integral under the hypotheses stated there. As an unconditional limUnder-based value it is junk when the principal value does not exist.

Main definitions

• TauCeti.Contour.windingNumber — the generalized winding number.
• TauCeti.Contour.IsNullHomologous — a curve whose winding number vanishes outside a set Ω.

Main results

• TauCeti.Contour.windingNumber_eq_cauchyPVAt — characteristic value lemma for the raw cauchyPVAt defining value.
• TauCeti.Contour.windingNumber_eq_of_hasCauchyPVAt — evaluate windingNumber from a Cauchy principal-value witness, without unfolding the definition.
• TauCeti.Contour.windingNumber_const — a constant curve has winding number zero on every parameter interval.
• TauCeti.Contour.windingNumber_congr_curve_ae — the winding number is unchanged when the curves agree almost everywhere on the integration interval and their derivatives agree almost everywhere where the curve misses z₀; TauCeti.Contour.windingNumber_congr_curve — the pointwise corollary, needing agreement only on the open interval Set.uIoo a b. This is what lets a piecewise contour be evaluated one piece at a time.
• TauCeti.Contour.windingNumber_same — the generalized winding number on [a, a] is 0.
• TauCeti.Contour.windingNumber_eq_zero_of_eq — if the two endpoints are equal, the generalized winding number is 0.
• TauCeti.Contour.isNullHomologous_iff — restates IsNullHomologous as its vanishing condition, so consumers use the predicate without unfolding its hidden body.
• TauCeti.Contour.intervalIntegrable_inv_sub_mul_deriv — integrability of the index integrand for a point off the curve.
• TauCeti.Contour.windingNumber_eq_integral_of_avoidance — reduces windingNumber to the ordinary index integral (2πi)⁻¹ · ∮_γ dz/(z − z₀) under the continuity, avoidance, and integrability hypotheses stated there.

This provides the foundation for the generalized residue theorem (Hungerbühler–Wasem, Thm 3.3).

Provenance

Adapted from the AINTLIB LeanModularForms project, file ForMathlib/GeneralizedWindingNumber.lean, specialised to the raw-function (γ : ℝ → ℂ on [a, b]) setting.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

noncomputable def TauCeti.Contour.windingNumber (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : ℂ

Generalized winding number (HW Def 2.1): n_{z₀}(γ) = (2πi)⁻¹ · PV ∮_γ dz/(z − z₀), the principal-value normalization of the index integral for a curve γ : ℝ → ℂ on [a, b] and any point z₀. See windingNumber_eq_integral_of_avoidance for its reduction to the ordinary index integral; as a limUnder-based value it is junk when the principal value does not exist.

Equations

• TauCeti.Contour.windingNumber γ a b z₀ = (2 * ↑Real.pi * Complex.I)⁻¹ * TauCeti.Contour.cauchyPVAt γ a b (fun (z : ℂ) => (z - z₀)⁻¹) z₀

theorem TauCeti.Contour.windingNumber_eq_cauchyPVAt {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} : windingNumber γ a b z₀ = (2 * ↑Real.pi * Complex.I)⁻¹ * cauchyPVAt γ a b (fun (z : ℂ) => (z - z₀)⁻¹) z₀

Characteristic value lemma. The generalized winding number is the normalized raw single-point principal-value value. This is the public, module-safe form of the definition for value-level rewrites.

theorem TauCeti.Contour.windingNumber_eq_of_hasCauchyPVAt {γ : ℝ → ℂ} {a b : ℝ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b (fun (z : ℂ) => (z - z₀)⁻¹) z₀ L) : windingNumber γ a b z₀ = (2 * ↑Real.pi * Complex.I)⁻¹ * L

Characteristic value lemma. From a Cauchy principal-value witness for (· − z₀)⁻¹ along γ, the generalized winding number is the normalized value (2πi)⁻¹ · L. This evaluates windingNumber through the HasCauchyPVAt predicate without unfolding the definition.

@[simp]

theorem TauCeti.Contour.windingNumber_same (γ : ℝ → ℂ) (a : ℝ) (z₀ : ℂ) : windingNumber γ a a z₀ = 0

The generalized winding number over a zero-length interval is 0.

@[simp]

theorem TauCeti.Contour.windingNumber_const (x : ℂ) (a b : ℝ) (z : ℂ) : windingNumber (fun (x_1 : ℝ) => x) a b z = 0

The generalized winding number of a constant curve is zero on every parameter interval.

theorem TauCeti.Contour.windingNumber_congr_curve_ae {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h_eq : γ₁ =ᵐ[MeasureTheory.volume.restrict (Set.uIoc a b)] γ₂) (h_deriv : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc a b), γ₁ t ≠ z₀ → deriv γ₁ t = deriv γ₂ t) : windingNumber γ₁ a b z₀ = windingNumber γ₂ a b z₀

The generalized winding number is unchanged when the curves agree almost everywhere and their derivatives agree almost everywhere off z₀. Derivative agreement is only needed where the curve misses z₀: the ε-truncation deletes the integrand at z₀ for every positive ε. Curve equality alone does not suffice — the index integrand contains deriv γ.

theorem TauCeti.Contour.windingNumber_congr_curve {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h_eq : Set.EqOn γ₁ γ₂ (Set.uIoo a b)) : windingNumber γ₁ a b z₀ = windingNumber γ₂ a b z₀

The generalized winding number depends on the curve only through its values on the open interval between a and b. Agreement on the open interval suffices even though the index integrand involves deriv γ, since an open set is a neighbourhood of each of its points. This is what lets a piecewise contour be evaluated one piece at a time: on each piece the assembled curve agrees with the simple curve computing that piece's contribution.

theorem TauCeti.Contour.windingNumber_eq_zero_of_eq (γ : ℝ → ℂ) {a b : ℝ} (hab : a = b) (z₀ : ℂ) : windingNumber γ a b z₀ = 0

If the two endpoints are equal, the generalized winding number is 0.

def TauCeti.Contour.IsNullHomologous (γ : ℝ → ℂ) (a b : ℝ) (Ω : Set ℂ) : Prop

A curve γ on [a, b] is null-homologous in Ω when its generalized winding number about every point outside Ω vanishes — the hypothesis of the homology form of Cauchy's theorem and of the Hungerbühler–Wasem residue theorem (HW Thm 3.3).

Equations

• TauCeti.Contour.IsNullHomologous γ a b Ω = ∀ w ∉ Ω, TauCeti.Contour.windingNumber γ a b w = 0

theorem TauCeti.Contour.isNullHomologous_iff {γ : ℝ → ℂ} {a b : ℝ} {Ω : Set ℂ} : IsNullHomologous γ a b Ω ↔ ∀ w ∉ Ω, windingNumber γ a b w = 0

Restatement of IsNullHomologous as its defining vanishing condition, so consumers can use the predicate without unfolding its hidden body.

theorem TauCeti.Contour.intervalIntegrable_inv_sub_mul_deriv {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b

Integrability of the index integrand for a point off the curve. If γ is continuous on Set.uIcc a b and avoids w there (so (γ · - w)⁻¹ is continuous) and deriv γ is interval-integrable, then (γ t - w)⁻¹ * deriv γ t is interval-integrable, being a continuous factor times an integrable one.

theorem TauCeti.Contour.windingNumber_eq_integral_of_avoidance {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h_cont : ContinuousOn γ (Set.uIcc a b)) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ z₀) (hf_int : IntervalIntegrable (fun (t : ℝ) => (γ t - z₀)⁻¹ * deriv γ t) MeasureTheory.volume a b) : windingNumber γ a b z₀ = (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (t : ℝ) in a..b, (γ t - z₀)⁻¹ * deriv γ t

If γ is continuous on [a, b], avoids z₀ there, and the index integrand is interval-integrable, the generalized winding number is the ordinary index integral: the principal value collapses to (2πi)⁻¹ · ∮_γ dz/(z − z₀).