Proximity invariance for absolutely continuous curves

Two absolutely continuous curves with equal endpoint ratios have equal winding numbers when their pointwise separation is smaller than the first curve's distance to that point. Their comparison quotient lies in the right half-plane, where the principal logarithm is smooth. The fundamental theorem for its absolutely continuous logarithm evaluates the difference of their index integrals.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_of_dist_lt_dist_of_eq_endpoint_ratios {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (h₀ : AbsolutelyContinuousOnInterval γ₀ a b) (h₁ : AbsolutelyContinuousOnInterval γ₁ a b) (hends : (γ₁ a - z) / (γ₀ a - z) = (γ₁ b - z) / (γ₀ b - z)) (hlt : ∀ t ∈ Set.uIcc a b, dist (γ₁ t) (γ₀ t) < dist (γ₀ t) z) : TauCeti.Contour.windingNumber γ₁ a b z = TauCeti.Contour.windingNumber γ₀ a b z

A pointwise leash preserves the winding number when the comparison quotient has equal endpoint values. The curves themselves need not be closed.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_of_dist_lt_dist {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (h₀ : AbsolutelyContinuousOnInterval γ₀ a b) (h₁ : AbsolutelyContinuousOnInterval γ₁ a b) (h₀closed : γ₀ a = γ₀ b) (h₁closed : γ₁ a = γ₁ b) (hlt : ∀ t ∈ Set.uIcc a b, dist (γ₁ t) (γ₀ t) < dist (γ₀ t) z) : TauCeti.Contour.windingNumber γ₁ a b z = TauCeti.Contour.windingNumber γ₀ a b z

A pointwise leash preserves winding numbers of closed absolutely continuous curves.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_of_dist_lt_dist_of_eq_endpoints {γ₀ γ₁ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (h₀ : AbsolutelyContinuousOnInterval γ₀ a b) (h₁ : AbsolutelyContinuousOnInterval γ₁ a b) (ha : γ₀ a = γ₁ a) (hb : γ₀ b = γ₁ b) (hlt : ∀ t ∈ Set.uIcc a b, dist (γ₁ t) (γ₀ t) < dist (γ₀ t) z) : TauCeti.Contour.windingNumber γ₁ a b z = TauCeti.Contour.windingNumber γ₀ a b z

A pointwise leash preserves winding numbers of AC paths with common endpoints.

theorem AbsolutelyContinuousOnInterval.eventually_windingNumber_eq_on_compl {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {γn : ℕ → ℝ → ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b) (hclosed : γ a = γ b) (hclosedn : ∀ (n : ℕ), γn n a = γn n b) (hconv : TendstoUniformlyOn γn γ Filter.atTop (Set.uIcc a b)) (hU : IsOpen U) (htrace : γ '' Set.uIcc a b ⊆ U) : ∀ᶠ (n : ℕ) in Filter.atTop, γn n '' Set.uIcc a b ⊆ U ∧ ∀ z ∉ U, TauCeti.Contour.windingNumber (γn n) a b z = TauCeti.Contour.windingNumber γ a b z

Uniform approximation of closed AC curves preserves the trace domain and every index outside that domain once the approximation is sufficiently close.

theorem TauCeti.Contour.eventually_sum_windingNumber_eq_on_compl_of_tendstoUniformlyOn {ι : Type u_1} {s : Finset ι} {γ : ι → ℝ → ℂ} {γn : ℕ → ι → ℝ → ℂ} {a b : ι → ℝ} {w : ι → ℤ} {U : Set ℂ} (hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i)) (hγn : ∀ (n : ℕ), ∀ i ∈ s, AbsolutelyContinuousOnInterval (γn n i) (a i) (b i)) (hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i)) (hclosedn : ∀ (n : ℕ), ∀ i ∈ s, γn n i (a i) = γn n i (b i)) (hconv : ∀ i ∈ s, TendstoUniformlyOn (fun (n : ℕ) => γn n i) (γ i) Filter.atTop (Set.uIcc (a i) (b i))) (hU : IsOpen U) (htrace : ∀ i ∈ s, γ i '' Set.uIcc (a i) (b i) ⊆ U) : ∀ᶠ (n : ℕ) in Filter.atTop, (∀ i ∈ s, γn n i '' Set.uIcc (a i) (b i) ⊆ U) ∧ ∀ z ∉ U, ∑ i ∈ s, ↑(w i) * windingNumber (γn n i) (a i) (b i) z = ∑ i ∈ s, ↑(w i) * windingNumber (γ i) (a i) (b i) z

Joint uniform approximation preserves every off-domain index eventually, so it preserves the total integer-weighted index without any individual index-vanishing assumption.