Directional Green identities on graph cells

Fubini slices the area integral over a vertical cell into integrals over its vertical fibers. Area integrability supplies both almost-everywhere fiber integrability and measurability of the zero-extended fiber integral. Applying the one-dimensional FTC gives the directional Green identity, requiring only the vertical derivative of the horizontal field component.

The horizontal identity follows by interchanging the coordinates, with its corresponding sign.

References

• M. Abdulaziz and L. C. Paulson, Green's Theorem, Archive of Formal Proofs.

theorem TauCeti.Green.ae_integrableOn_verticalRegion_fiber {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hR : MeasureTheory.IntegrableOn R (verticalRegion a b lower upper) MeasureTheory.volume) : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), MeasureTheory.IntegrableOn (fun (y : ℝ) => R { re := x, im := y }) (Set.Icc (lower x) (upper x)) MeasureTheory.volume

An area-integrable function is integrable on almost every vertical fiber of a graph cell.

theorem TauCeti.Green.intervalIntegrable_verticalRegion_graph {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {P : ℂ → E} {graph : ℝ → ℝ} (hab : a ≤ b) (hgraph : ContinuousOn graph (Set.Icc a b)) (hbetween : ∀ x ∈ Set.Icc a b, graph x ∈ Set.Icc (lower x) (upper x)) (hP : ContinuousOn P (verticalRegion a b lower upper)) : IntervalIntegrable (fun (x : ℝ) => P { re := x, im := graph x }) MeasureTheory.volume a b

A continuous graph lying inside a vertical cell has a Bochner-integrable field value along its base interval. It applies to both boundary graphs when lower ≤ upper on [a,b], without any graph-speed bound.

theorem TauCeti.Green.integrable_verticalRegion_fiberIntegral {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} [NormedSpace ℝ E] (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hR : MeasureTheory.IntegrableOn R (verticalRegion a b lower upper) MeasureTheory.volume) : MeasureTheory.Integrable ((Set.Icc a b).indicator fun (x : ℝ) => ∫ (y : ℝ) in Set.Icc (lower x) (upper x), R { re := x, im := y }) MeasureTheory.volume

The zero-extended fiber integral is integrable, so no extra fiber-measurability hypothesis is needed for an area-integrable function.

theorem TauCeti.Green.integral_verticalRegion {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} [NormedSpace ℝ E] (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hR : MeasureTheory.IntegrableOn R (verticalRegion a b lower upper) MeasureTheory.volume) : ∫ (z : ℂ) in verticalRegion a b lower upper, R z = ∫ (x : ℝ) in Set.Icc a b, ∫ (y : ℝ) in Set.Icc (lower x) (upper x), R { re := x, im := y }

Fubini's slicing formula for the area integral over a vertical graph cell.

theorem TauCeti.Green.integrableOn_comp_coordinateSwapCLE {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} (hR : MeasureTheory.IntegrableOn R (horizontalRegion a b lower upper) MeasureTheory.volume) : MeasureTheory.IntegrableOn (R ∘ ⇑Complex.coordinateSwapCLE) (verticalRegion a b lower upper) MeasureTheory.volume

Coordinate swap transports integrability from a horizontal cell to its vertical cell.

theorem TauCeti.Green.integral_comp_coordinateSwapCLE_verticalRegion {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} [NormedSpace ℝ E] : ∫ (z : ℂ) in verticalRegion a b lower upper, (R ∘ ⇑Complex.coordinateSwapCLE) z = ∫ (z : ℂ) in horizontalRegion a b lower upper, R z

Coordinate swap transports the set integral from a vertical cell to its horizontal cell.

theorem TauCeti.Green.integral_horizontalRegion {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} [NormedSpace ℝ E] (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hR : MeasureTheory.IntegrableOn R (horizontalRegion a b lower upper) MeasureTheory.volume) : ∫ (z : ℂ) in horizontalRegion a b lower upper, R z = ∫ (y : ℝ) in Set.Icc a b, ∫ (x : ℝ) in Set.Icc (lower y) (upper y), R { re := x, im := y }

Fubini's slicing formula for a horizontal graph cell, obtained by interchanging coordinates.

theorem TauCeti.Green.integral_graphs_sub_eq_neg_integral_verticalRegion {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} [NormedSpace ℝ E] [CompleteSpace E] {P : ℂ → E} (hab : a ≤ b) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) (hP : ContinuousOn P (verticalRegion a b lower upper)) (hdP : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Ioo (lower x) (upper x), HasDerivAt (fun (y : ℝ) => P { re := x, im := y }) (R { re := x, im := y }) y) (hR : MeasureTheory.IntegrableOn R (verticalRegion a b lower upper) MeasureTheory.volume) : ∫ (x : ℝ) in a..b, P { re := x, im := lower x } - P { re := x, im := upper x } = -∫ (z : ℂ) in verticalRegion a b lower upper, R z

The directional Green identity on a vertical graph cell. The positively oriented graph boundary contributes the bottom graph minus the top graph; the vertical sides contribute zero to P dx. Only the vertical derivative is assumed, and no continuity of that derivative is required.

theorem TauCeti.Green.integral_graphs_sub_eq_integral_horizontalRegion {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {lower upper : ℝ → ℝ} {R : ℂ → E} [NormedSpace ℝ E] [CompleteSpace E] {Q : ℂ → E} (hab : a ≤ b) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ y ∈ Set.Icc a b, lower y ≤ upper y) (hQ : ContinuousOn Q (horizontalRegion a b lower upper)) (hdQ : ∀ y ∈ Set.Icc a b, ∀ x ∈ Set.Ioo (lower y) (upper y), HasDerivAt (fun (x : ℝ) => Q { re := x, im := y }) (R { re := x, im := y }) x) (hR : MeasureTheory.IntegrableOn R (horizontalRegion a b lower upper) MeasureTheory.volume) : ∫ (y : ℝ) in a..b, Q { re := upper y, im := y } - Q { re := lower y, im := y } = ∫ (z : ℂ) in horizontalRegion a b lower upper, R z

The directional Green identity on a horizontal graph cell. The positively oriented graph boundary contributes the right graph minus the left graph; the horizontal sides contribute zero to Q dy. Only the horizontal derivative is assumed.