Concatenation API for the generalized winding number

This file records the additivity of Contour.windingNumber over adjacent parameter intervals. The contour-integration roadmap uses finite decompositions of a curve into an avoiding part and model sectors in Hungerbühler--Wasem Proposition 2.2; those decompositions need to add the corresponding generalized winding numbers after the principal values on the pieces have been constructed.

The results here are deliberately conditional on the relevant pointwise principal-value existence statements. The generalized winding number is a limUnder-based value, so without those witnesses it is a junk value; the characteristic lemmas below keep the additivity statement tied to honest principal values.

Main results

• Contour.windingNumber_eq_add_of_hasCauchyPVAt — additivity from explicit principal-value witnesses on two adjacent intervals.
• Contour.windingNumber_concat — additivity from principal-value existence on the two adjacent intervals, using the canonical cauchyPVAt values.
• Contour.IsNullHomologous.concat — if a curve is null-homologous on both adjacent intervals and the exterior pointwise principal values exist on those intervals, then it is null-homologous on their concatenation.
• Contour.IsNullHomologous.concat_of_avoidance — the same conclusion in the common case where both curve pieces lie in the domain, so exterior points are avoided and the principal values are ordinary integrals.

Provenance

This is routine API around the Hungerbühler--Wasem generalized winding number from the contour integration roadmap; no formal source is vendored.

theorem TauCeti.Contour.windingNumber_eq_add_of_hasCauchyPVAt {γ : ℝ → ℂ} {a b c : ℝ} {z₀ L₁ L₂ : ℂ} (h_ab : HasCauchyPVAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀ L₁) (h_bc : HasCauchyPVAt γ b c (fun (w : ℂ) => (w - z₀)⁻¹) z₀ L₂) : windingNumber γ a c z₀ = windingNumber γ a b z₀ + windingNumber γ b c z₀

Additivity of the generalized winding number from explicit principal-value witnesses. If the index-integrand principal values about z₀ on [a, b] and [b, c] are L₁ and L₂, then the winding number over [a, c] is the sum of the two winding numbers.

theorem TauCeti.Contour.windingNumber_concat {γ : ℝ → ℂ} {a b c : ℝ} {z₀ : ℂ} (h_ab : CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀) (h_bc : CauchyPVExistsAt γ b c (fun (w : ℂ) => (w - z₀)⁻¹) z₀) : windingNumber γ a c z₀ = windingNumber γ a b z₀ + windingNumber γ b c z₀

Additivity of the generalized winding number over adjacent intervals. It is enough to know that the principal values defining the two summand winding numbers exist; the principal value on the concatenated interval is then supplied by HasCauchyPVAt.concat.

theorem TauCeti.Contour.windingNumber_eq_zero_concat {γ : ℝ → ℂ} {a b c : ℝ} {z₀ : ℂ} (h_ab : windingNumber γ a b z₀ = 0) (h_bc : windingNumber γ b c z₀ = 0) (hpv_ab : CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀) (hpv_bc : CauchyPVExistsAt γ b c (fun (w : ℂ) => (w - z₀)⁻¹) z₀) : windingNumber γ a c z₀ = 0

If the winding numbers about z₀ vanish on two adjacent intervals, and the two corresponding principal values exist, then the winding number about z₀ also vanishes on the concatenated interval.

theorem TauCeti.Contour.IsNullHomologous.concat {γ : ℝ → ℂ} {a b c : ℝ} {Ω : Set ℂ} (h_ab : IsNullHomologous γ a b Ω) (h_bc : IsNullHomologous γ b c Ω) (hpv_ab : ∀ z ∉ Ω, CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z)⁻¹) z) (hpv_bc : ∀ z ∉ Ω, CauchyPVExistsAt γ b c (fun (w : ℂ) => (w - z)⁻¹) z) : IsNullHomologous γ a c Ω

Null-homology is preserved by concatenating adjacent parameter intervals, provided the pointwise principal values defining the exterior winding numbers exist on the two pieces. This is the form used by finite decomposition arguments: after proving the exterior winding numbers vanish piecewise, they vanish on the concatenation.

theorem TauCeti.Contour.IsNullHomologous.concat_of_avoidance {γ : ℝ → ℂ} {a b c : ℝ} {Ω : Set ℂ} (h_ab : IsNullHomologous γ a b Ω) (h_bc : IsNullHomologous γ b c Ω) (hγ_ab : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hγ_bc : ∀ t ∈ Set.uIcc b c, γ t ∈ Ω) (hcont_ab : ContinuousOn γ (Set.uIcc a b)) (hcont_bc : ContinuousOn γ (Set.uIcc b c)) (hint_ab : ∀ z ∉ Ω, IntervalIntegrable (fun (t : ℝ) => (γ t - z)⁻¹ * deriv γ t) MeasureTheory.volume a b) (hint_bc : ∀ z ∉ Ω, IntervalIntegrable (fun (t : ℝ) => (γ t - z)⁻¹ * deriv γ t) MeasureTheory.volume b c) : IsNullHomologous γ a c Ω

Null-homology is preserved by concatenating adjacent intervals in the ordinary avoided-pole case. If both pieces of the curve lie in Ω, then every exterior point is avoided; under continuity and interval-integrability of the exterior index integrands, the needed principal values are supplied by cauchyPVExistsAt_of_avoidance.