Concatenation of complete Sobolev trajectories

Two continuous trajectories with matching endpoint values form one continuous trajectory on the sum of their time intervals.

noncomputable def CKN.Leray.regularisedBesselAppendPath (k : ℕ) (T S : ℝ) (hT : 0 ≤ T) (hS : 0 ≤ S) (u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (v : C(↑(RegularizedMildTimeInterval S), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (_hend : u ⟨T, ⋯⟩ = v ⟨0, ⋯⟩) : C(↑(RegularizedMildTimeInterval (T + S)), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)

Join two complete Sobolev paths at a common endpoint.

Equations

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

theorem CKN.Leray.regularisedBesselAppendPath_left (k : ℕ) (T S : ℝ) (hT : 0 ≤ T) (hS : 0 ≤ S) (u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (v : C(↑(RegularizedMildTimeInterval S), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (hend : u ⟨T, ⋯⟩ = v ⟨0, ⋯⟩) (t : ↑(RegularizedMildTimeInterval (T + S))) (ht : ↑t ≤ T) : (regularisedBesselAppendPath k T S hT hS u v hend) t = u ⟨↑t, ⋯⟩

Before the joining time, the concatenated path equals the first path.

theorem CKN.Leray.regularisedBesselAppendPath_right (k : ℕ) (T S : ℝ) (hT : 0 ≤ T) (hS : 0 ≤ S) (u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (v : C(↑(RegularizedMildTimeInterval S), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (hend : u ⟨T, ⋯⟩ = v ⟨0, ⋯⟩) (t : ↑(RegularizedMildTimeInterval (T + S))) (ht : T ≤ ↑t) : (regularisedBesselAppendPath k T S hT hS u v hend) t = v ⟨↑t - T, ⋯⟩

After the joining time, the concatenated path equals the translated second path.