Green's theorem for absolutely continuous curves

For a closed AC curve, a real C¹ field on an open neighborhood of the trace and winding support satisfies the winding-weighted circulation identity. Both integrability statements are conclusions. A cutoff is constructed before applying the global polygonal theorem; uniform, derivative L¹, and winding-weight L¹ approximation pass the identity to the curve.

theorem TauCeti.Green.green_ac_winding {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {P Q : ℂ → ℝ} (hab : a < b) (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, Contour.windingNumber γ a b z = 0) : IntervalIntegrable (circulationFun P Q γ) MeasureTheory.volume a b ∧ MeasureTheory.IntegrableOn (fun (z : ℂ) => windingWeight γ a b z * curl P Q z) U MeasureTheory.volume ∧ ∫ (t : ℝ) in a..b, circulationFun P Q γ t = ∫ (z : ℂ) in U, windingWeight γ a b z * curl P Q z

Green's theorem for a closed absolutely continuous curve with index vanishing outside the open field domain. The winding numbers may be unbounded and the curve may intersect itself.

theorem TauCeti.Green.green_ac {γ : ℝ → ℂ} {a b : ℝ} {P Q : ℂ → ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) : IntervalIntegrable (circulationFun P Q γ) MeasureTheory.volume a b ∧ MeasureTheory.Integrable (fun (z : ℂ) => windingWeight γ a b z * curl P Q z) MeasureTheory.volume ∧ ∫ (t : ℝ) in a..b, circulationFun P Q γ t = ∫ (z : ℂ), windingWeight γ a b z * curl P Q z

Global real C¹ fields satisfy Green's theorem for every closed AC curve, with both integrability conclusions. Compact support of the field is not required.