Exact pasting of actual continuous solution paths on adjacent compact time intervals.

noncomputable def EulerTimePathGluing.glueFunction {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (t : ℝ) : E

The literal adjacent-interval pasting of two actual clamped paths.

Equations

• EulerTimePathGluing.glueFunction a b ha hb u v t = if t ≤ a then EulerVolterraConvolution.extendPath a ha u t else EulerVolterraConvolution.extendPath b hb v (t - a)

theorem EulerTimePathGluing.endpoint_match {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) : EulerVolterraConvolution.extendPath a ha u a = EulerVolterraConvolution.extendPath b hb v 0

Matching endpoint traces are exactly the equality needed by the clamped pasting.

theorem EulerTimePathGluing.glueFunction_continuous {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) : Continuous (glueFunction a b ha hb u v)

Matching actual endpoint traces make the pasted path continuous.

noncomputable def EulerTimePathGluing.gluePath {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) : C(↑(Set.Icc 0 (a + b)), E)

The actual continuous path on the union of the two adjacent time intervals.

Equations

• EulerTimePathGluing.gluePath a b ha hb u v hmatch = { toFun := fun (t : ↑(Set.Icc 0 (a + b))) => EulerTimePathGluing.glueFunction a b ha hb u v ↑t, continuous_toFun := ⋯ }

theorem EulerTimePathGluing.glueFunction_left {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (t : ℝ) (ht : t ≤ a) : glueFunction a b ha hb u v t = EulerVolterraConvolution.extendPath a ha u t

The pasted function preserves the original solution before the restart time.

theorem EulerTimePathGluing.glueFunction_right {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (t : ℝ) (ht : a ≤ t) : glueFunction a b ha hb u v t = EulerVolterraConvolution.extendPath b hb v (t - a)

The pasted function is the restarted solution after its matching endpoint.

theorem EulerTimePathGluing.gluePath_left {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (t : ℝ) (ht : t ∈ Set.Icc 0 a) : EulerVolterraConvolution.extendPath (a + b) ⋯ (gluePath a b ha hb u v hmatch) t = EulerVolterraConvolution.extendPath a ha u t

On the old interval the actual clamped union path is identical to the old clamped path.

theorem EulerTimePathGluing.gluePath_right {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (t : ℝ) (ht : t ∈ Set.Icc 0 b) : EulerVolterraConvolution.extendPath (a + b) ⋯ (gluePath a b ha hb u v hmatch) (a + t) = EulerVolterraConvolution.extendPath b hb v t

On the new interval the actual clamped union path is identical to the elapsed-time restart path.

theorem EulerTimePathGluing.gluePath_norm_le {E : Type u_1} [NormedAddCommGroup E] (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (R : ℝ) (hR : 0 ≤ R) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖gluePath a b ha hb u v hmatch‖ ≤ R

The actual pasted path is bounded by any common uniform bound for its two pieces.