Graph certificates for path integrals

A graph certificate records the trace and regularity of a path, independently of any field or integral value. Either real coordinate can be the graph parameter. The parameter may backtrack or have unbounded speed. The resulting coordinate integral is the ordinary base-interval integral, by Henstock substitution.

noncomputable def TauCeti.Green.BoundaryChain.graphPath (d : Coordinate) (g : ℝ → ℝ) (a b : ℝ) (hg : ContinuousOn g (Set.uIcc a b)) : Path (d.graph g a) (d.graph g b)

The graph path with affine base coordinate from a to b, in either orientation.

Equations

• TauCeti.Green.BoundaryChain.graphPath d g a b hg = Path.ofLine ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.Green.BoundaryChain.graphPath_apply (d : Coordinate) (g : ℝ → ℝ) (a b : ℝ) (hg : ContinuousOn g (Set.uIcc a b)) (t : ↑unitInterval) : (graphPath d g a b hg) t = d.graph g ((AffineMap.lineMap a b) ↑t)

@[simp]

theorem TauCeti.Green.BoundaryChain.graphPath_const (d : Coordinate) (c a b : ℝ) : graphPath d (fun (x : ℝ) => c) a b ⋯ = Path.segment (d.graph (fun (x : ℝ) => c) a) (d.graph (fun (x : ℝ) => c) b)

A constant graph with affine base parametrization is exactly the existing straight path.

structure TauCeti.Green.BoundaryChain.GraphArc (d : Coordinate) (g : ℝ → ℝ) (a b : ℝ) (γ : Arc) : Prop

A path on a regular graph, with a continuous graph coordinate differentiable outside countably many exceptions. These are geometric and differential conditions only.

• continuous_graph : ContinuousOn g (Set.Icc a b)
• differentiable_graph : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo a b \ S, DifferentiableAt ℝ g t
• on_graph (t : ↑unitInterval) : γ.snd.snd t = d.graph g (d.proj (γ.snd.snd t))
• coordinate_mem (t : ↑unitInterval) : d.proj (γ.snd.snd t) ∈ Set.Icc a b
• differentiable_coordinate : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo 0 1 \ S, DifferentiableAt ℝ (fun (t : ℝ) => d.proj (γ.snd.snd.extend t)) t

theorem TauCeti.Green.BoundaryChain.graphArc_graphPath (d : Coordinate) {g : ℝ → ℝ} {a b c e : ℝ} (hg : ContinuousOn g (Set.Icc c e)) (hdg : ∃ (S : Set ℝ), S.Countable ∧ ∀ t ∈ Set.Ioo c e \ S, DifferentiableAt ℝ g t) (ha : a ∈ Set.Icc c e) (hb : b ∈ Set.Icc c e) : GraphArc d g c e ⟨d.graph g a, ⟨d.graph g b, graphPath d g a b ⋯⟩⟩

Affinely parametrized graph paths give graph certificates for every subinterval and for both orientations. This includes nonconstant arcs on nonsmooth continuous graphs.

theorem TauCeti.Green.BoundaryChain.GraphArc.symm {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {p q : ℂ} {γ : Path p q} (h : GraphArc d g a b ⟨p, ⟨q, γ⟩⟩) : GraphArc d g a b ⟨q, ⟨p, γ.symm⟩⟩

Reversal preserves a graph certificate and reverses its endpoint order.

theorem TauCeti.Green.BoundaryChain.GraphArc.trans_left {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {p q r : ℂ} {γ : Path p q} {δ : Path q r} (h : GraphArc d g a b ⟨p, ⟨r, γ.trans δ⟩⟩) : GraphArc d g a b ⟨p, ⟨q, γ⟩⟩

The left piece of an actual joined graph arc inherits its geometric and countable coordinate-regularity certificate.

theorem TauCeti.Green.BoundaryChain.GraphArc.trans_right {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {p q r : ℂ} {γ : Path p q} {δ : Path q r} (h : GraphArc d g a b ⟨p, ⟨r, γ.trans δ⟩⟩) : GraphArc d g a b ⟨q, ⟨r, δ⟩⟩

The right piece of a joined graph arc inherits its graph certificate.

theorem TauCeti.Green.BoundaryChain.coordinate_constant_trans_iff (d : Coordinate) {p q r : ℂ} (γ : Path p q) (δ : Path q r) : (∀ (t : ↑unitInterval), d.proj ((γ.trans δ) t) = d.proj p) ↔ (∀ (t : ↑unitInterval), d.proj (γ t) = d.proj p) ∧ ∀ (t : ↑unitInterval), d.proj (δ t) = d.proj q

Constant selected-coordinate certificates restrict to both pieces of an actual join, and conversely the two piece certificates imply the whole-arc certificate.

theorem TauCeti.Green.BoundaryChain.GraphArc.extend_eq {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (h : GraphArc d g a b γ) (t : ℝ) : γ.snd.snd.extend t = d.graph g (d.proj (γ.snd.snd.extend t))

The constant endpoint extension still lies on the same graph.

theorem TauCeti.Green.BoundaryChain.GraphArc.source_mem {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (h : GraphArc d g a b γ) : d.proj γ.fst ∈ Set.Icc a b

The graph coordinate of the initial endpoint lies in the base interval.

theorem TauCeti.Green.BoundaryChain.GraphArc.target_mem {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (h : GraphArc d g a b γ) : d.proj γ.snd.fst ∈ Set.Icc a b

The graph coordinate of the terminal endpoint lies in the base interval.

theorem TauCeti.Green.BoundaryChain.GraphArc.hasIntegral {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (h : GraphArc d g a b γ) {P : ℂ → ℝ} (hP : ContinuousOn P (d.graph g '' Set.Icc a b)) : BoxIntegral.HasIntegral (BoxIntegral.intervalBox 0 1 ⋯) BoxIntegral.IntegrationParams.Henstock (fun (t : Fin 1 → ℝ) => P (γ.snd.snd.extend (t 0)) * d.proj (deriv (⇑γ.snd.snd.extend) (t 0))) BoxIntegral.BoxAdditiveMap.volume (∫ (t : ℝ) in d.proj γ.fst..d.proj γ.snd.fst, P (d.graph g t))

A graph certificate gives the genuine Henstock integral, including backtracking.

theorem TauCeti.Green.BoundaryChain.GraphArc.integrable {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (h : GraphArc d g a b γ) {P : ℂ → ℝ} (hP : ContinuousOn P (d.graph g '' Set.Icc a b)) : Integrable d.proj P (ofPath γ.snd.snd)

Graph arcs have the required chain integrability witness.

theorem TauCeti.Green.BoundaryChain.GraphArc.arcIntegral_eq {d : Coordinate} {g : ℝ → ℝ} {a b : ℝ} {γ : Arc} (h : GraphArc d g a b γ) {P : ℂ → ℝ} (hP : ContinuousOn P (d.graph g '' Set.Icc a b)) : arcIntegral d.proj P γ = ∫ (t : ℝ) in d.proj γ.fst..d.proj γ.snd.fst, P (d.graph g t)

The coordinate integral of a certified graph arc depends only on its endpoints.