Green's theorem and flux for simple closed absolutely continuous curves

Combining the Jordan index theorem (TauCeti.Analysis.Contour.Winding.AbsolutelyContinuous.Jordan) with the winding-weighted Green theorem (TauCeti.Green.green_ac_winding) yields Green's curl and flux-divergence formulas for an arbitrary simple closed absolutely continuous curve γ on [a, b] (a < b, γ a = γ b, InjOn γ (Ico a b)), with no supplied index hypothesis: the orientation sign TauCeti.Contour.jordanSign γ a b ∈ {1, -1} is a conclusion of simplicity.

Main results

• AbsolutelyContinuousOnInterval.windingWeight_eq_indicator_jordanSign: the winding weight of a simple closed AC curve is the indicator of filledHull C \ C times jordanSign γ a b.
• TauCeti.Green.green_ac_jordan: circulation around a simple closed AC curve equals jordanSign γ a b times the integral of curl P Q over filledHull C \ C, with both integrabilities deduced automatically.
• TauCeti.Green.green_ac_flux_jordan: flux-divergence form for a simple closed AC curve.

theorem AbsolutelyContinuousOnInterval.windingWeight_eq_indicator_jordanSign {γ : ℝ → ℂ} {a b : ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) : TauCeti.Green.windingWeight γ a b = (TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).indicator fun (x : ℂ) => ↑(TauCeti.Contour.jordanSign γ a b)

For a simple closed absolutely continuous curve on [a, b] (a < b), the winding weight is Contour.jordanSign γ a b times the indicator of the bounded inside filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).

theorem TauCeti.Green.green_ac_jordan {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {P Q : ℂ → ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (hU : IsOpen U) (hregion : filledHull (γ '' Set.uIcc a b) ⊆ U) (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U) : IntervalIntegrable (circulationFun P Q γ) MeasureTheory.volume a b ∧ MeasureTheory.IntegrableOn (curl P Q) (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b) MeasureTheory.volume ∧ ∫ (t : ℝ) in a..b, circulationFun P Q γ t = ↑(Contour.jordanSign γ a b) * ∫ (z : ℂ) in filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, curl P Q z

Green's theorem for a simple closed absolutely continuous curve: with no supplied index hypothesis, both the boundary circulation and the interior curl are integrable and the circulation equals Contour.jordanSign γ a b ∈ {1, -1} times the integral of curl P Q over the bounded inside filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).

theorem TauCeti.Green.green_ac_flux_jordan {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {X Y : ℂ → ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (hU : IsOpen U) (hregion : filledHull (γ '' Set.uIcc a b) ⊆ U) (hX : ContDiffOn ℝ 1 X U) (hY : ContDiffOn ℝ 1 Y U) : IntervalIntegrable (fun (t : ℝ) => X (γ t) * (deriv γ t).im - Y (γ t) * (deriv γ t).re) MeasureTheory.volume a b ∧ MeasureTheory.IntegrableOn (fun (z : ℂ) => (fderiv ℝ X z) 1 + (fderiv ℝ Y z) Complex.I) (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b) MeasureTheory.volume ∧ ∫ (t : ℝ) in a..b, X (γ t) * (deriv γ t).im - Y (γ t) * (deriv γ t).re = ↑(Contour.jordanSign γ a b) * ∫ (z : ℂ) in filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, (fderiv ℝ X z) 1 + (fderiv ℝ Y z) Complex.I

Flux-divergence form of Green's theorem for a simple closed absolutely continuous curve: the boundary integral of X dy - Y dx equals Contour.jordanSign γ a b ∈ {1, -1} times the divergence integral over filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).