Crossing finiteness for piecewise-C¹ immersions (HW Proposition 2.2)

A piecewise-C¹ immersion meets any given point z₀ ∈ ℂ at only finitely many parameters — Proposition 2.2 of Hungerbühler–Wasem (there stated with endpoint avoidance; the one-sided isolation lemmas here cover the endpoints, so no avoidance is needed), the geometric input that makes the on-cycle singularity set of the generalized residue theorem a finite crossing family. It discharges the finite_crossings field of Contour.ConditionAprime for immersed cycles.

The mechanism: at a crossing the one-sided tangent is non-zero, so a dual functional of it makes t ↦ γ t - z₀ strictly monotone in that functional on a one-sided neighbourhood, forbidding nearby crossings; crossings are therefore isolated, and an infinite crossing set inside the compact [[a, b]] would have an accumulation point.

Main results

• Contour.IsPwC1ImmersionOn.eventually_ne_nhdsNE — crossings of an immersion are isolated.
• Contour.IsPwC1ImmersionOn.finite_crossings — HW Proposition 2.2: the crossing set [[a, b]] ∩ γ ⁻¹' {z₀} of an immersion is finite.
• Contour.IsPwC1ImmersionOn.mem_toFinset_finite_crossings — membership in the resulting crossing finset.

Provenance

Migrated from CrossingAnalysis.lean (PwC1Immersion.crossingSet_finite and the isolation lemmas) of the AINTLIB LeanModularForms development, restated for the raw curve γ : ℝ → ℂ on [[a, b]]: the one-sided tangent data carried there by the left_deriv_limit / right_deriv_limit fields of the bundled PwC1Immersion comes from the IsPwC1ImmersionOn tangent-limit API (PwC1ImmersionOn.lean), which uniformises the smooth-point and breakpoint cases of the isolation argument. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, Proposition 2.2.

theorem TauCeti.Contour.IsPwC1ImmersionOn.eventually_ne_nhdsNE {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (min a b) (max a b)) (hcross : γ t₀ = z₀) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ {t₀}ᶜ, γ t ≠ z₀

Crossings of an immersion are isolated: at every interior crossing there is a punctured neighbourhood on which the immersion avoids z₀.

theorem TauCeti.Contour.IsPwC1ImmersionOn.finite_crossings {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : IsPwC1ImmersionOn γ a b) : (Set.uIcc a b ∩ γ ⁻¹' {z₀}).Finite

HW Proposition 2.2: the crossing set of a piecewise-C¹ immersion is finite — the geometric input that makes the on-cycle singularities of the generalized residue theorem a finite crossing family.

theorem TauCeti.Contour.IsPwC1ImmersionOn.mem_toFinset_finite_crossings {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : IsPwC1ImmersionOn γ a b) {t : ℝ} : t ∈ ⋯.toFinset ↔ t ∈ Set.uIcc a b ∧ γ t = z₀

Membership in the crossing finset. The finset supplied by IsPwC1ImmersionOn.finite_crossings consists of exactly the parameters of [[a, b]] at which γ takes the value z₀. Multi-crossing principal-value arguments index their windows by this finset, so they need the characterisation and not just the finiteness; for ordered endpoints follow with uIcc_of_le.

theorem TauCeti.Contour.IsPwC1ImmersionOn.mem_toFinset_finite_crossings_of_le {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) {t : ℝ} : t ∈ ⋯.toFinset ↔ t ∈ Set.Icc a b ∧ γ t = z₀

Crossings at ordered endpoints. The form of IsPwC1ImmersionOn.mem_toFinset_finite_crossings for a ≤ b, where the crossing parameters range over Icc a b rather than uIcc a b. Every multi-crossing principal-value argument indexes its windows this way.