Joining an actual history with a forward elapsed-time path

The two continuous paths have matching traces. This wrapper uses the fixed linear gluing map, proves the true time derivative through the junction, and preserves the original ordered-word Sobolev radius.

Gluing matching continuous paths is one fixed linear contraction.

Genuine first-order evolution paths glue through a matching interior trace.

noncomputable def EulerTimeIntervalGlue.glue {E : Type u_1} (τ : ℝ) (f g : ℝ → E) (t : ℝ) : E

Glue, with branches according to t ≤ τ.

Equations

• EulerTimeIntervalGlue.glue τ f g t = if t ≤ τ then f t else g t

theorem EulerTimeIntervalGlue.glue_left {E : Type u_1} (τ : ℝ) (f g : ℝ → E) (t : ℝ) (ht : t ≤ τ) : glue τ f g t = f t

theorem EulerTimeIntervalGlue.glue_right {E : Type u_1} (τ : ℝ) (f g : ℝ → E) (hmatch : f τ = g τ) (t : ℝ) (ht : τ ≤ t) : glue τ f g t = g t

theorem EulerTimeIntervalGlue.glue_continuous {E : Type u_1} [NormedAddCommGroup E] (τ : ℝ) (f g : ℝ → E) (hmatch : f τ = g τ) (hf : Continuous f) (hg : Continuous g) : Continuous (glue τ f g)

theorem EulerTimeIntervalGlue.glue_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (f g f' g' : ℝ → E) (hmatch : f τ = g τ) (hmatch' : f' τ = g' τ) (hf : ∀ t ∈ Set.Icc 0 τ, HasDerivWithinAt f (f' t) (Set.Icc 0 τ) t) (hg : ∀ t ∈ Set.Icc τ S, HasDerivWithinAt g (g' t) (Set.Icc τ S) t) (t : ℝ) (ht : t ∈ Set.Icc 0 S) : HasDerivWithinAt (glue τ f g) (glue τ f' g' t) (Set.Icc 0 S) t

Matching the value and derivative gives the genuine derivative even at the joining time.

theorem EulerTimeIntervalGlue.glue_evolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (f g : ℝ → E) (rhs : ℝ → E → E) (hmatch : f τ = g τ) (hf : ∀ t ∈ Set.Icc 0 τ, HasDerivWithinAt f (rhs t (f t)) (Set.Icc 0 τ) t) (hg : ∀ t ∈ Set.Icc τ S, HasDerivWithinAt g (rhs t (g t)) (Set.Icc τ S) t) (t : ℝ) (ht : t ∈ Set.Icc 0 S) : HasDerivWithinAt (glue τ f g) (rhs t (glue τ f g t)) (Set.Icc 0 S) t

For the same first-order equation the derivative matching follows from value matching.

theorem EulerTimeIntervalGlue.glue_weighted_bound {E : Type u_1} [NormedAddCommGroup E] (S τ : ℝ) (f g : ℝ → E) (γ : ℝ → ℝ) (C : ℝ) (hf : ∀ t ∈ Set.Icc 0 τ, ‖f t‖ ≤ C * γ t) (hg : ∀ t ∈ Set.Icc τ S, ‖g t‖ ≤ C * γ t) (t : ℝ) (ht : t ∈ Set.Icc 0 S) : ‖glue τ f g t‖ ≤ C * γ t

Joining the intervals does not change a shared pointwise time-profile bound.

theorem EulerPacketTimePathGluing.compactInterval (a b : ℝ) : CompactSpace ↑(Set.Icc a b)

@[reducible, inline]

abbrev EulerPacketTimePathGluing.Pair (S τ : ℝ) (E : Type u_2) [TopologicalSpace E] : Type u_2

Pair: an abbreviation for C(Icc (0 : ℝ) τ,E) × C(Icc τ S,E).

Equations

• EulerPacketTimePathGluing.Pair S τ E = (C(↑(Set.Icc 0 τ), E) × C(↑(Set.Icc τ S), E))

def EulerPacketTimePathGluing.mismatch {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) : Pair S τ E →L[ℝ] E

Mismatch as an element of Pair S τ E →L[ℝ] E.

Equations

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

@[reducible, inline]

abbrev EulerPacketTimePathGluing.Matching {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) : Submodule ℝ (Pair S τ E)

Matching: an abbreviation for (mismatch (E := E) S τ hτ0 hτS).ker.

Equations

• EulerPacketTimePathGluing.Matching S τ hτ0 hτS = (↑(EulerPacketTimePathGluing.mismatch S τ hτ0 hτS)).ker

theorem EulerPacketTimePathGluing.matching_values {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : ↥(Matching S τ hτ0 hτS)) : (↑u).1 ⟨τ, ⋯⟩ = (↑u).2 ⟨τ, ⋯⟩

noncomputable def EulerPacketTimePathGluing.gluePath {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : ↥(Matching S τ hτ0 hτS)) : C(↑(Set.Icc 0 S), E)

Glue path as an element of C(Icc (0 : ℝ) S,E).

Equations

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

theorem EulerPacketTimePathGluing.gluePath_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : ↥(Matching S τ hτ0 hτS)) : ‖gluePath S τ hτ0 hτS u‖ ≤ ‖u‖

noncomputable def EulerPacketTimePathGluing.glueOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) : ↥(Matching S τ hτ0 hτS) →L[ℝ] C(↑(Set.Icc 0 S), E)

Glue operator as an element of Matching (E := E) S τ hτ0 hτS →L[ℝ] C(Icc (0 : ℝ) S,E).

Equations

• EulerPacketTimePathGluing.glueOperator S τ hτ0 hτS = { toFun := EulerPacketTimePathGluing.gluePath S τ hτ0 hτS, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem EulerPacketTimePathGluing.glueOperator_norm_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) : ‖glueOperator S τ hτ0 hτS‖ ≤ 1

Smoothness of matching path pairs is derived from smoothness of the two paths. A fixed linear repair provides the subspace-valued map; it is the identity on matching data. The final word estimate uses the exact subtype norm, not the norm of this auxiliary repair.

Matching time paths glue without any external-word or fixed-Sobolev loss.

@[simp]

theorem EulerPacketTimePathGluing.glueOperator_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : ↥(Matching S τ hτ0 hτS)) : (glueOperator S τ hτ0 hτS) u = gluePath S τ hτ0 hτS u

theorem EulerPacketTimePathGluing.gluePath_left {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : ↥(Matching S τ hτ0 hτS)) (t : ↑(Set.Icc 0 τ)) : (gluePath S τ hτ0 hτS u) ⟨↑t, ⋯⟩ = (↑u).1 t

theorem EulerPacketTimePathGluing.gluePath_right {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : ↥(Matching S τ hτ0 hτS)) (t : ↑(Set.Icc τ S)) : (gluePath S τ hτ0 hτS u) ⟨↑t, ⋯⟩ = (↑u).2 t

theorem EulerPacketTimePathGluing.glue_family_contDiff {X : Type u_1} {E : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (f : X → ↥(Matching S τ hτ0 hτS)) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ ↑⊤ fun (x : X) => gluePath S τ hτ0 hτS (f x)

theorem EulerPacketTimePathGluing.glue_word_derivative {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (directions : ι → X) (f : X → ↥(Matching S τ hτ0 hτS)) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) (x : X) : EulerParameterWordGevrey.wordDerivative directions (fun (y : X) => gluePath S τ hτ0 hτS (f y)) w x = gluePath S τ hτ0 hτS (EulerParameterWordGevrey.wordDerivative directions f w x)

theorem EulerPacketTimePathGluing.glue_word_bound {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (directions : ι → X) (f : X → ↥(Matching S τ hτ0 hτS)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.wordSum directions (fun (y : X) => gluePath S τ hτ0 hτS (f y)) n x ≤ EulerParameterWordGevrey.wordSum directions f n x

theorem EulerPacketTimePathGluing.glue_block_bound {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (directions : ι → X) (q : ℕ) (f : X → ↥(Matching S τ hτ0 hτS)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => gluePath S τ hτ0 hτS (f y)) n x ≤ EulerParameterWordGevrey.block directions q f n x

Fixed H6 is the specialization q=6; no tensor-to-word conversion occurs.

def EulerPacketTimePathGluing.repairPair {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) : Pair S τ E →L[ℝ] Pair S τ E

Repair pair as an element of Pair S τ E →L[ℝ] Pair S τ E.

Equations

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

theorem EulerPacketTimePathGluing.repairPair_mem {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : Pair S τ E) : (repairPair S τ hτ0 hτS) u ∈ Matching S τ hτ0 hτS

def EulerPacketTimePathGluing.matchingProjection {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) : Pair S τ E →L[ℝ] ↥(Matching S τ hτ0 hτS)

Matching projection, given by (repairPair S τ hτ0 hτS).codRestrict (Matching S τ hτ0 hτS) (repairPair_mem S τ hτ0 hτS).

Equations

• EulerPacketTimePathGluing.matchingProjection S τ hτ0 hτS = (EulerPacketTimePathGluing.repairPair S τ hτ0 hτS).codRestrict (EulerPacketTimePathGluing.Matching S τ hτ0 hτS) ⋯

theorem EulerPacketTimePathGluing.matchingProjection_value {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : Pair S τ E) (hu : u.1 ⟨τ, ⋯⟩ = u.2 ⟨τ, ⋯⟩) : ↑((matchingProjection S τ hτ0 hτS) u) = u

def EulerPacketTimePathGluing.matchingFamily {X : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : X → C(↑(Set.Icc 0 τ), E)) (v : X → C(↑(Set.Icc τ S), E)) : X → ↥(Matching S τ hτ0 hτS)

Matching family, defined pointwise by matchingProjection S τ hτ0 hτS (u x,v x).

Equations

• EulerPacketTimePathGluing.matchingFamily S τ hτ0 hτS u v x = (EulerPacketTimePathGluing.matchingProjection S τ hτ0 hτS) (u x, v x)

theorem EulerPacketTimePathGluing.matchingFamily_contDiff {X : Type u_1} {E : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : X → C(↑(Set.Icc 0 τ), E)) (v : X → C(↑(Set.Icc τ S), E)) (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) : ContDiff ℝ (↑⊤) (matchingFamily S τ hτ0 hτS u v)

theorem EulerPacketTimePathGluing.wordSum_subtype {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (directions : ι → X) (f : X → ↥(Matching S τ hτ0 hτS)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.wordSum directions (fun (y : X) => ↑(f y)) n x = EulerParameterWordGevrey.wordSum directions f n x

theorem EulerPacketTimePathGluing.wordSum_pair_le {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (directions : ι → X) (f : X → E × F) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.wordSum directions f n x ≤ EulerParameterWordGevrey.wordSum directions (fun (y : X) => (f y).1) n x + EulerParameterWordGevrey.wordSum directions (fun (y : X) => (f y).2) n x

theorem EulerPacketTimePathGluing.matchingFamily_glue_block {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (directions : ι → X) (q : ℕ) (u : X → C(↑(Set.Icc 0 τ), E)) (v : X → C(↑(Set.Icc τ S), E)) (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hmatch : ∀ (x : X), (u x) ⟨τ, ⋯⟩ = (v x) ⟨τ, ⋯⟩) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => gluePath S τ hτ0 hτS (matchingFamily S τ hτ0 hτS u v y)) n x ≤ EulerParameterWordGevrey.block directions q u n x + EulerParameterWordGevrey.block directions q v n x

Independently smooth matching inputs give the same-radius glued block bound.

The actual affine time shift used by the forward transverse solve.

def EulerPacketTimePathGluing.elapsedTime (S τ : ℝ) : C(↑(Set.Icc τ S), ↑(Set.Icc 0 (S - τ)))

Elapsed time as an element of C(Icc τ S, Icc (0 : ℝ) (S-τ)).

Equations

• EulerPacketTimePathGluing.elapsedTime S τ = { toFun := fun (t : ↑(Set.Icc τ S)) => ⟨↑t - τ, ⋯⟩, continuous_toFun := ⋯ }

def EulerPacketTimePathGluing.shiftPath {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) : C(↑(Set.Icc 0 (S - τ)), E) →L[ℝ] C(↑(Set.Icc τ S), E)

Shift path, given by ContinuousMap.compCLM ℝ E (elapsedTime S τ).

Equations

• EulerPacketTimePathGluing.shiftPath S τ = ContinuousMap.compCLM ℝ E (EulerPacketTimePathGluing.elapsedTime S τ)

theorem EulerPacketTimePathGluing.shiftPath_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (u : C(↑(Set.Icc 0 (S - τ)), E)) (t : ↑(Set.Icc τ S)) : ((shiftPath S τ) u) t = u ⟨↑t - τ, ⋯⟩

theorem EulerPacketTimePathGluing.shiftPath_norm_le_one {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) : ‖shiftPath S τ‖ ≤ 1

theorem EulerPacketTimePathGluing.shiftPath_initial {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 (S - τ)), E)) : ((shiftPath S τ) u) ⟨τ, ⋯⟩ = u ⟨0, ⋯⟩

theorem EulerPacketTimePathGluing.shiftPath_block_bound {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (S τ : ℝ) (directions : ι → X) (q : ℕ) (f : X → C(↑(Set.Icc 0 (S - τ)), E)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (shiftPath S τ) (f y)) n x ≤ EulerParameterWordGevrey.block directions q f n x

Literal elapsed-time paths retain the same fixed-Sobolev word bound.

def EulerElapsedTimePathGluing.pair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) : ↥(EulerPacketTimePathGluing.Matching S τ hτ0 hτS)

Pair, given by ⟨(u,shiftPath S τ v),by change u ⟨τ,hτ0,le_rfl⟩-shiftPath S τ v ⟨τ,le_rfl,hτS⟩ = 0 rw [shiftPath_initial S τ hτS,hmatch,sub_self]⟩.

Equations

• EulerElapsedTimePathGluing.pair S τ hτ0 hτS u v hmatch = ⟨(u, (EulerPacketTimePathGluing.shiftPath S τ) v), ⋯⟩

noncomputable def EulerElapsedTimePathGluing.join {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) : C(↑(Set.Icc 0 S), E)

Join, given by gluePath S τ hτ0 hτS (pair S τ hτ0 hτS u v hmatch).

Equations

• EulerElapsedTimePathGluing.join S τ hτ0 hτS u v hmatch = EulerPacketTimePathGluing.gluePath S τ hτ0 hτS (EulerElapsedTimePathGluing.pair S τ hτ0 hτS u v hmatch)

theorem EulerElapsedTimePathGluing.join_eq_projection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) : join S τ hτ0 hτS u v hmatch = EulerPacketTimePathGluing.gluePath S τ hτ0 hτS ((EulerPacketTimePathGluing.matchingProjection S τ hτ0 hτS) (u, (EulerPacketTimePathGluing.shiftPath S τ) v))

theorem EulerElapsedTimePathGluing.join_extend {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) (t : ℝ) (ht : t ∈ Set.Icc 0 S) : EulerVolterraConvolution.extendPath S ⋯ (join S τ hτ0 hτS u v hmatch) t = EulerTimeIntervalGlue.glue τ (EulerVolterraConvolution.extendPath τ hτ0 u) (fun (r : ℝ) => EulerVolterraConvolution.extendPath (S - τ) ⋯ v (r - τ)) t

theorem EulerElapsedTimePathGluing.join_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) (t : ↑(Set.Icc 0 τ)) : (join S τ hτ0 hτS u v hmatch) ⟨↑t, ⋯⟩ = u t

theorem EulerElapsedTimePathGluing.join_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) (t : ↑(Set.Icc τ S)) : (join S τ hτ0 hτS u v hmatch) ⟨↑t, ⋯⟩ = v ⟨↑t - τ, ⋯⟩

theorem EulerElapsedTimePathGluing.join_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) (u' : C(↑(Set.Icc 0 τ), E)) (v' : C(↑(Set.Icc 0 (S - τ)), E)) (hmatch' : u' ⟨τ, ⋯⟩ = v' ⟨0, ⋯⟩) (hu : ∀ (t : ↑(Set.Icc 0 τ)), HasDerivWithinAt (EulerVolterraConvolution.extendPath τ hτ0 u) (u' t) (Set.Icc 0 τ) ↑t) (hv : ∀ (t : ↑(Set.Icc 0 (S - τ))), HasDerivWithinAt (EulerVolterraConvolution.extendPath (S - τ) ⋯ v) (v' t) (Set.Icc 0 (S - τ)) ↑t) (t : ↑(Set.Icc 0 S)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath S ⋯ (join S τ hτ0 hτS u v hmatch)) ((join S τ hτ0 hτS u' v' hmatch') t) (Set.Icc 0 S) ↑t

Genuine within-time differentiation holds even at the joining time.

theorem EulerElapsedTimePathGluing.join_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : X → C(↑(Set.Icc 0 τ), E)) (q : X → C(↑(Set.Icc 0 (S - τ)), E)) (hp : ContDiff ℝ (↑⊤) p) (hq : ContDiff ℝ (↑⊤) q) (hm : ∀ (x : X), (p x) ⟨τ, ⋯⟩ = (q x) ⟨0, ⋯⟩) : ContDiff ℝ ↑⊤ fun (x : X) => join S τ hτ0 hτS (p x) (q x) ⋯

theorem EulerElapsedTimePathGluing.join_block_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) {X : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] (p : X → C(↑(Set.Icc 0 τ), E)) (q : X → C(↑(Set.Icc 0 (S - τ)), E)) (hp : ContDiff ℝ (↑⊤) p) (hq : ContDiff ℝ (↑⊤) q) (hm : ∀ (x : X), (p x) ⟨τ, ⋯⟩ = (q x) ⟨0, ⋯⟩) (directions : ι → X) (k n : ℕ) (x : X) : EulerParameterWordGevrey.block directions k (fun (y : X) => join S τ hτ0 hτS (p y) (q y) ⋯) n x ≤ EulerParameterWordGevrey.block directions k p n x + EulerParameterWordGevrey.block directions k q n x

The fixed Sobolev block is bounded by the sum of the input blocks, with no new radius or derivative factor from the time junction.