Localization of planar Green fields

The union of a closed absolutely continuous curve's trace and winding support is compact. The same holds for finitely many closed AC traces and their total weighted winding support, without any index-vanishing assumption. If every trace lies in an open field domain and the single or total index vanishes outside that domain, the compact union is contained in the domain. Smooth cutoffs then give globally C¹ fields preserving circulation along each curve and the single or total winding-weighted curl integral.

theorem TauCeti.Green.exists_contDiff_localization_sum {ι : Type u_1} {s : Finset ι} {γ : ι → ℝ → ℂ} {a b : ι → ℝ} {w : ι → ℤ} {U : Set ℂ} {P Q : ℂ → ℝ} (hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i)) (hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i)) (hU : IsOpen U) (htrace : ∀ i ∈ s, γ i '' Set.uIcc (a i) (b i) ⊆ U) (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) (hindex : ∀ z ∉ U, ∑ i ∈ s, ↑(w i) * Contour.windingNumber (γ i) (a i) (b i) z = 0) : ∃ (P' : ℂ → ℝ) (Q' : ℂ → ℝ), ContDiff ℝ 1 P' ∧ ContDiff ℝ 1 Q' ∧ HasCompactSupport P' ∧ HasCompactSupport Q' ∧ tsupport P' ⊆ U ∧ tsupport Q' ⊆ U ∧ (∀ i ∈ s, Set.EqOn P' P (γ i '' Set.uIcc (a i) (b i))) ∧ (∀ i ∈ s, Set.EqOn Q' Q (γ i '' Set.uIcc (a i) (b i))) ∧ (∀ (z : ℂ), (∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) * curl P' Q' z = (∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) * curl P Q z) ∧ (∀ i ∈ s, ∫ (t : ℝ) in a i..b i, circulationFun P' Q' (γ i) t = ∫ (t : ℝ) in a i..b i, circulationFun P Q (γ i) t) ∧ ∫ (z : ℂ) in U, (∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) * curl P' Q' z = ∫ (z : ℂ) in U, (∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) * curl P Q z

Finite weighted cycles can be localized using their total index and every trace. The localized fields preserve every boundary integral and the total winding-weighted area integral.

theorem AbsolutelyContinuousOnInterval.exists_contDiff_localization {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {P Q : ℂ → ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hU : IsOpen U) (htrace : γ '' Set.uIcc a b ⊆ U) (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) (hindex : ∀ z ∉ U, TauCeti.Contour.windingNumber γ a b z = 0) : ∃ (P' : ℂ → ℝ) (Q' : ℂ → ℝ), ContDiff ℝ 1 P' ∧ ContDiff ℝ 1 Q' ∧ HasCompactSupport P' ∧ HasCompactSupport Q' ∧ tsupport P' ⊆ U ∧ tsupport Q' ⊆ U ∧ Set.EqOn P' P (γ '' Set.uIcc a b) ∧ Set.EqOn Q' Q (γ '' Set.uIcc a b) ∧ (∀ (z : ℂ), TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P' Q' z = TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P Q z) ∧ ∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P' Q' γ t = ∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q γ t ∧ ∫ (z : ℂ) in U, TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P' Q' z = ∫ (z : ℂ) in U, TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P Q z

A locally C¹ field can be cut off to a globally C¹, compactly supported field without changing circulation or the winding-weighted curl integral.