Polygonal approximation preserving an index domain

Uniformly close closed absolutely continuous curves have the same index outside any open neighborhood of the original trace. Endpoint-preserving polygonal approximation therefore preserves an index-vanishing domain eventually, while the winding weights converge in L¹.

theorem TauCeti.Green.exists_polygonal_approximation_winding {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hU : IsOpen U) (htrace : γ '' Set.uIcc a b ⊆ U) (hindex : ∀ z ∉ U, Contour.windingNumber γ a b z = 0) : ∃ (γn : ℕ → ℝ → ℂ), (∀ (n : ℕ), IsPolygonalOnInterval (γn n) a b ∧ AbsolutelyContinuousOnInterval (γn n) a b ∧ γn n a = γ a ∧ γn n b = γ b ∧ γn n a = γn n b) ∧ TendstoUniformlyOn γn γ Filter.atTop (Set.Icc a b) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, ‖deriv (γn n) t - deriv γ t‖) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), |windingWeight (γn n) a b z - windingWeight γ a b z|) Filter.atTop (nhds 0) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, γn n '' Set.uIcc a b ⊆ U ∧ ∀ z ∉ U, Contour.windingNumber (γn n) a b z = 0

A closed AC curve with index vanishing outside its field domain has closed polygonal approximants converging uniformly, in derivative L¹, and in winding-weight L¹. Eventually their traces lie in the domain and their indices also vanish outside it.