Green's theorem for independent finite directional divisions

Each division contributes one directional identity. Geometric null-chain certificates compare its actual boundary with a common boundary presentation, modulo the unused coordinate. The vertical and horizontal divisions need not have the same cells, parametrizations, or edges. The field assumptions are continuity, existence of the used fiber derivatives, and cellwise area integrability of those derivatives. The curve-integral specialization also assumes arcwise circulation integrability. No Fréchet differentiability or continuity of the derivatives is needed.

References

• Mohammad Abdulaziz and Lawrence C. Paulson, An Isabelle/HOL formalisation of Green's Theorem, Archive of Formal Proofs, 2018: the directional division and path-equivalence formulation.

theorem TauCeti.Green.Division.integrable_and_integral_boundary {d : Coordinate} {D : Set ℂ} (V : Division d D) {P R : ℂ → ℝ} (hP : ContinuousOn P D) (hdP : ∀ K ∈ V.cells, ∀ x ∈ Set.Icc K.a K.b, ∀ y ∈ Set.Ioo (K.lowerFun x) (K.upperFun x), HasDerivAt (fun (y : ℝ) => P (d.graph (fun (x : ℝ) => y) x)) (R (d.graph (fun (x : ℝ) => y) x)) y) (hR : ∀ K ∈ V.cells, MeasureTheory.IntegrableOn R (K.region d) MeasureTheory.volume) : BoundaryChain.Integrable d.proj P V.boundary ∧ MeasureTheory.IntegrableOn R D MeasureTheory.volume ∧ (BoundaryChain.integral d.proj P) V.boundary = -↑d.orientation * ∫ (z : ℂ) in D, R z

Summing the cell identities gives directional Green and genuine gauge integrability on the finite division boundary. Cellwise area integrability is promoted to the whole region.

theorem TauCeti.Green.Division.integrable_and_integral_add_integral_eq_integral_sub {D U : Set ℂ} (V : Division Coordinate.re D) (H : Division Coordinate.im D) {c : BoundaryChain} (hV : BoundaryChain.NullChain Coordinate.re U (V.boundary - c)) (hH : BoundaryChain.NullChain Coordinate.im U (H.boundary - c)) (hDU : D ⊆ U) {P Q RP RQ : ℂ → ℝ} (hP : ContinuousOn P U) (hQ : ContinuousOn Q U) (hdP : ∀ K ∈ V.cells, ∀ x ∈ Set.Icc K.a K.b, ∀ y ∈ Set.Ioo (K.lowerFun x) (K.upperFun x), HasDerivAt (fun (y : ℝ) => P { re := x, im := y }) (RP { re := x, im := y }) y) (hdQ : ∀ K ∈ H.cells, ∀ y ∈ Set.Icc K.a K.b, ∀ x ∈ Set.Ioo (K.lowerFun y) (K.upperFun y), HasDerivAt (fun (x : ℝ) => Q { re := x, im := y }) (RQ { re := x, im := y }) x) (hRP : ∀ K ∈ V.cells, MeasureTheory.IntegrableOn RP (K.region Coordinate.re) MeasureTheory.volume) (hRQ : ∀ K ∈ H.cells, MeasureTheory.IntegrableOn RQ (K.region Coordinate.im) MeasureTheory.volume) : BoundaryChain.Integrable Complex.reCLM P c ∧ BoundaryChain.Integrable Complex.imCLM Q c ∧ MeasureTheory.IntegrableOn (fun (z : ℂ) => RQ z - RP z) D MeasureTheory.volume ∧ (BoundaryChain.integral Complex.reCLM P) c + (BoundaryChain.integral Complex.imCLM Q) c = ∫ (z : ℂ) in D, RQ z - RP z

Full Green from separate type-I and type-II divisions and geometric comparisons to a common boundary. Gauge boundary integrability and integrability of the directional curl are conclusions. In particular no equality of boundary integrals is assumed.

theorem TauCeti.Green.Division.integrableOn_and_linearCombination_curveIntegral_eq_integral_sub {D U : Set ℂ} (V : Division Coordinate.re D) (H : Division Coordinate.im D) {c : BoundaryChain} (hV : BoundaryChain.NullChain Coordinate.re U (V.boundary - c)) (hH : BoundaryChain.NullChain Coordinate.im U (H.boundary - c)) (hDU : D ⊆ U) {P Q RP RQ : ℂ → ℝ} (hP : ContinuousOn P U) (hQ : ContinuousOn Q U) (hdP : ∀ K ∈ V.cells, ∀ x ∈ Set.Icc K.a K.b, ∀ y ∈ Set.Ioo (K.lowerFun x) (K.upperFun x), HasDerivAt (fun (y : ℝ) => P { re := x, im := y }) (RP { re := x, im := y }) y) (hdQ : ∀ K ∈ H.cells, ∀ y ∈ Set.Icc K.a K.b, ∀ x ∈ Set.Ioo (K.lowerFun y) (K.upperFun y), HasDerivAt (fun (x : ℝ) => Q { re := x, im := y }) (RQ { re := x, im := y }) x) (hRP : ∀ K ∈ V.cells, MeasureTheory.IntegrableOn RP (K.region Coordinate.re) MeasureTheory.volume) (hRQ : ∀ K ∈ H.cells, MeasureTheory.IntegrableOn RQ (K.region Coordinate.im) MeasureTheory.volume) (hc : ∀ γ ∈ c.support, IntervalIntegrable (circulationFun P Q ⇑γ.snd.snd.extend) MeasureTheory.volume 0 1) : MeasureTheory.IntegrableOn (fun (z : ℂ) => RQ z - RP z) D MeasureTheory.volume ∧ (Finsupp.linearCombination ℤ fun (γ : Arc) => curveIntegral (oneForm P Q) γ.snd.snd) c = ∫ (z : ℂ) in D, RQ z - RP z

The Bochner specialization retains genuine integrability of the circulation on every supported arc and concludes the identity for Mathlib's existing curve integral.