Gauge integrals along graph arcs

For a graph continuous on an interval and differentiable except at countably many points, the P dx integral along a vertical cell graph is the ordinary integral of P over the base interval. A horizontal cell graph satisfies the corresponding Q dy formula. These statements use the actual raw-curve derivative and the Henstock integral, without bounded graph speed or absolute continuity. Constant-coordinate arcs have zero integral in the unused direction. Graph reparametrization permits backtracking and unbounded speed, even when exceptional graph levels have uncountable preimages under the parametrization.

theorem TauCeti.Green.Coordinate.exists_graph_reparam_primitive (d : Coordinate) {a b c e : ℝ} {g θ θ' : ℝ → ℝ} {P : ℂ → ℝ} {s S : Set ℝ} (hs : s.Countable) (hS : S.Countable) (hg : ContinuousOn g (Set.Icc c e)) (hdg : ∀ x ∈ Set.Ioo c e \ S, DifferentiableAt ℝ g x) (hP : ContinuousOn P (d.graph g '' Set.Icc c e)) (hdθ : ∀ t ∈ Set.uIoo a b \ s, HasDerivAt θ (θ' t) t) (hmap : Set.MapsTo θ (Set.uIcc a b) (Set.Icc c e)) : ∃ (A : ℝ → ℝ), Continuous A ∧ (∀ x ∈ Set.Icc c e, ∀ y ∈ Set.Icc c e, A y - A x = ∫ (z : ℝ) in x..y, P (d.graph g z)) ∧ ∃ (T : Set ℝ), T.Countable ∧ ∀ t ∈ Set.uIoo a b \ T, HasDerivAt (A ∘ θ) (P (d.graph g (θ t)) * d.proj (deriv (d.graph g ∘ θ) t)) t

A graph-coordinate reparametrization has a continuous scalar primitive. Its increments are the coefficient integrals, and its composed derivative is the actual projected-curve integrand outside a countable exceptional set.

theorem TauCeti.Green.hasHenstockIntervalIntegral_graph_reparam (d : Coordinate) {a b c e : ℝ} {graph θ θ' : ℝ → ℝ} {P : ℂ → ℝ} {s S : Set ℝ} (hs : s.Countable) (hS : S.Countable) (hgraph : ContinuousOn graph (Set.Icc c e)) (hdgraph : ∀ t ∈ Set.Ioo c e \ S, DifferentiableAt ℝ graph t) (hP : ContinuousOn P (d.graph graph '' Set.Icc c e)) (hθ : ContinuousOn θ (Set.uIcc a b)) (hdθ : ∀ t ∈ Set.uIoo a b \ s, HasDerivAt θ (θ' t) t) (hmap : Set.MapsTo θ (Set.uIcc a b) (Set.Icc c e)) : BoxIntegral.HasHenstockIntervalIntegral (fun (t : ℝ) => P (d.graph graph (θ t)) * d.proj (deriv (d.graph graph ∘ θ) t)) a b (∫ (t : ℝ) in θ a..θ b, P (d.graph graph t))

Gauge integration on a graph depends only on the endpoint graph coordinates. The parametrization may backtrack and have unbounded speed, and exceptional graph levels may have uncountable preimages. Both coordinate directions use this same substitution theorem.