The oriented four-edge boundary of a graph cell

The graph edges are existing paths with affine base coordinate. The two endpoint fibers are straight segments. Swapping real and imaginary coordinates reverses orientation, so the horizontal cell uses the negative of the swapped vertical presentation. The endpoint boundary vanishes, and actual Henstock integrability follows from graph regularity and field continuity.

noncomputable def TauCeti.Green.BoundaryChain.cellBoundary (d : Coordinate) (a b : ℝ) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.uIcc a b)) (hu : ContinuousOn upper (Set.uIcc a b)) : BoundaryChain

The signed four-edge boundary of a graph cell, positive when a ≤ b and lower ≤ upper. Repeated edges and collapsed endpoint fibers are permitted.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Green.BoundaryChain.cellBoundary_def (d : Coordinate) (a b : ℝ) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.uIcc a b)) (hu : ContinuousOn upper (Set.uIcc a b)) : cellBoundary d a b lower upper hl hu = d.orientation • quadrilateral (graphPath d lower a b hl) (Path.segment (d.graph lower b) (d.graph upper b)) (graphPath d upper a b hu) (Path.segment (d.graph lower a) (d.graph upper a))

The four actual parameterized edges, with the coordinate-orientation sign.

@[simp]

theorem TauCeti.Green.BoundaryChain.boundary_cellBoundary (d : Coordinate) (a b : ℝ) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.uIcc a b)) (hu : ContinuousOn upper (Set.uIcc a b)) : boundary (cellBoundary d a b lower upper hl hu) = 0

The cell has zero endpoint boundary.

theorem TauCeti.Green.BoundaryChain.integrable_and_integral_cellBoundary (d : Coordinate) {a b : ℝ} {lower upper : ℝ → ℝ} (hab : a ≤ b) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hdl : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo a b \ S, DifferentiableAt ℝ lower t) (hdu : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo a b \ S, DifferentiableAt ℝ upper t) {P : ℂ → ℝ} (hPl : ContinuousOn P (d.graph lower '' Set.Icc a b)) (hPu : ContinuousOn P (d.graph upper '' Set.Icc a b)) : Integrable d.proj P (cellBoundary d a b lower upper ⋯ ⋯) ∧ (integral d.proj P) (cellBoundary d a b lower upper ⋯ ⋯) = d.orientation • ((∫ (t : ℝ) in a..b, P (d.graph lower t)) - ∫ (t : ℝ) in a..b, P (d.graph upper t))

The gauge boundary integral of a graph cell is the signed difference of its graph integrals. The statement also supplies genuine integrability of all four edges.

theorem TauCeti.Green.BoundaryChain.integrable_and_integral_cellBoundary_of_deriv (d : Coordinate) {a b : ℝ} {lower upper : ℝ → ℝ} (hab : a ≤ b) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hdl : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo a b \ S, DifferentiableAt ℝ lower t) (hdu : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo a b \ S, DifferentiableAt ℝ upper t) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) {P R : ℂ → ℝ} (hP : ContinuousOn P (d.region a b lower upper)) (hdP : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Ioo (lower x) (upper x), HasDerivAt (fun (y : ℝ) => P (d.graph (fun (x : ℝ) => y) x)) (R (d.graph (fun (x : ℝ) => y) x)) y) (hR : MeasureTheory.IntegrableOn R (d.region a b lower upper) MeasureTheory.volume) : Integrable d.proj P (cellBoundary d a b lower upper ⋯ ⋯) ∧ (integral d.proj P) (cellBoundary d a b lower upper ⋯ ⋯) = -↑d.orientation * ∫ (z : ℂ) in d.region a b lower upper, R z

Directional Green on a graph cell with countably many graph differentiability exceptions. The coordinate sign supplies the vertical/horizontal boundary convention.

theorem TauCeti.Green.BoundaryChain.cellBoundary_rectangle_re_eq_im (a b c e : ℝ) : cellBoundary Coordinate.re a b (fun (x : ℝ) => c) (fun (x : ℝ) => e) ⋯ ⋯ = cellBoundary Coordinate.im c e (fun (x : ℝ) => a) (fun (x : ℝ) => b) ⋯ ⋯

The type-I and type-II presentations of a rectangle have the same actual integer chain. This supplies a common boundary directly from geometry, before any field is chosen.