Green and flux for index-one AC curves #
Index one on all bounded complementary components identifies the winding weight with the
indicator of the filled hull minus the trace. Green's theorem then gives the unweighted curl
formula without simplicity or a finite division. Substitution of (-Y, X) gives flux with
the outward sign X dy − Y dx and divergence ∂x X + ∂y Y.
theorem
TauCeti.Green.green_ac_index_one
{γ : ℝ → ℂ}
{a b : ℝ}
{U : Set ℂ}
{P Q : ℂ → ℝ}
(hab : a < b)
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hclosed : γ a = γ b)
(hU : IsOpen U)
(hregion : filledHull (γ '' Set.uIcc a b) ⊆ U)
(hP : ContDiffOn ℝ 1 P U)
(hQ : ContDiffOn ℝ 1 Q U)
(hindex : ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, Contour.windingNumber γ a b z = 1)
:
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 = ∫ (z : ℂ) in filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, curl P Q z
The index-one AC Green theorem over the entire bounded complementary region. Both integrabilities are conclusions, with no simplicity or finite-component hypothesis.
theorem
TauCeti.Green.green_ac_flux
{γ : ℝ → ℂ}
{a b : ℝ}
{U : Set ℂ}
{X Y : ℂ → ℝ}
(hab : a < b)
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hclosed : γ a = γ b)
(hU : IsOpen U)
(hregion : filledHull (γ '' Set.uIcc a b) ⊆ U)
(hX : ContDiffOn ℝ 1 X U)
(hY : ContDiffOn ℝ 1 Y U)
(hindex : ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, Contour.windingNumber γ a b z = 1)
:
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 = ∫ (z : ℂ) in filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, (fderiv ℝ X z) 1 + (fderiv ℝ Y z) Complex.I
The flux form of index-one AC Green: the boundary sign is outward and no unit tangent or nonzero speed is required.