Two actual ordinary Euler solutions with matching endpoint data concatenate to an actual solution. The projected equation identifies their time derivatives at the seam; the scalar pressure is canonical.

Concatenation of two paths on closed time intervals. Matching endpoint values and derivatives give a genuine derivative at the seam.

noncomputable def EulerIntervalConcatenation.join {E : Type u_1} (T S : ℝ) (hT : 0 ≤ T) (hS : 0 ≤ S) (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) (t : ℝ) : E

Join, with branches according to t ≤ T.

Equations

• EulerIntervalConcatenation.join T S hT hS f g t = if t ≤ T then f (Set.projIcc 0 T hT t) else g (Set.projIcc 0 S hS (t - T))

theorem EulerIntervalConcatenation.join_left {E : Type u_1} {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) {t : ℝ} (ht : t ≤ T) : join T S hT hS f g t = f (Set.projIcc 0 T hT t)

theorem EulerIntervalConcatenation.join_right {E : Type u_1} {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) (hfg : f ⟨T, ⋯⟩ = g ⟨0, ⋯⟩) {t : ℝ} (ht : T ≤ t) : join T S hT hS f g t = g (Set.projIcc 0 S hS (t - T))

theorem EulerIntervalConcatenation.map_join {E : Type u_1} {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) {F : Type u_2} (A : E → F) (t : ℝ) : A (join T S hT hS f g t) = join T S hT hS (fun (s : ↑(Set.Icc 0 T)) => A (f s)) (fun (s : ↑(Set.Icc 0 S)) => A (g s)) t

theorem EulerIntervalConcatenation.join_continuous {E : Type u_1} {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) [TopologicalSpace E] (hf : Continuous f) (hg : Continuous g) (hfg : f ⟨T, ⋯⟩ = g ⟨0, ⋯⟩) : Continuous (join T S hT hS f g)

theorem EulerIntervalConcatenation.join_hasDerivAt_seam {E : Type u_1} {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) [NormedAddCommGroup E] [NormedSpace ℝ E] (df : ↑(Set.Icc 0 T) → E) (dg : ↑(Set.Icc 0 S) → E) (hTpos : 0 < T) (hSpos : 0 < S) (hfg : f ⟨T, ⋯⟩ = g ⟨0, ⋯⟩) (hdf : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (fun (r : ℝ) => f (Set.projIcc 0 T hT r)) (df t) (Set.Icc 0 T) ↑t) (hdg : ∀ (t : ↑(Set.Icc 0 S)), HasDerivWithinAt (fun (r : ℝ) => g (Set.projIcc 0 S hS r)) (dg t) (Set.Icc 0 S) ↑t) (hderiv : df ⟨T, ⋯⟩ = dg ⟨0, ⋯⟩) : HasDerivAt (join T S hT hS f g) (df ⟨T, ⋯⟩) T

theorem EulerIntervalConcatenation.join_hasDerivAt {E : Type u_1} {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (f : ↑(Set.Icc 0 T) → E) (g : ↑(Set.Icc 0 S) → E) [NormedAddCommGroup E] [NormedSpace ℝ E] (df : ↑(Set.Icc 0 T) → E) (dg : ↑(Set.Icc 0 S) → E) (hTpos : 0 < T) (hSpos : 0 < S) (hfg : f ⟨T, ⋯⟩ = g ⟨0, ⋯⟩) (hdf : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (fun (r : ℝ) => f (Set.projIcc 0 T hT r)) (df t) (Set.Icc 0 T) ↑t) (hdg : ∀ (t : ↑(Set.Icc 0 S)), HasDerivWithinAt (fun (r : ℝ) => g (Set.projIcc 0 S hS r)) (dg t) (Set.Icc 0 S) ↑t) (hderiv : df ⟨T, ⋯⟩ = dg ⟨0, ⋯⟩) (t : ℝ) (ht : t ∈ Set.Ioo 0 (T + S)) : HasDerivAt (join T S hT hS f g) (join T S hT hS df dg t) t

noncomputable def EulerOrdinarySobolev.Evolution.joinedVelocity {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (t : ↑(Set.Icc 0 (T + S))) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Joined velocity, given by join T S hT hS U.velocity V.velocity t.

Equations

• U.joinedVelocity V t = EulerIntervalConcatenation.join T S hT hS U.velocity V.velocity ↑t

theorem EulerOrdinarySobolev.Evolution.joinedVelocity_continuous {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (hmatch : U.velocity ⟨T, ⋯⟩ = V.velocity ⟨0, ⋯⟩) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 (T + S))) => (U.joinedVelocity V t).jetLp n

theorem EulerOrdinarySobolev.Evolution.velocity_toLp_hasDerivWithinAt_projected {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hpos : 0 < T) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => (U.velocity (Set.projIcc 0 T hT r)).toLp) (projectedRhs (U.velocity t)).toLp (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.joinedVelocity_derivative {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (hTpos : 0 < T) (hSpos : 0 < S) (hmatch : U.velocity ⟨T, ⋯⟩ = V.velocity ⟨0, ⋯⟩) (t : ℝ) (ht : t ∈ Set.Ioo 0 (T + S)) : HasDerivAt (fun (r : ℝ) => (U.joinedVelocity V (Set.projIcc 0 (T + S) ⋯ r)).toLp) (projectedRhs (U.joinedVelocity V ⟨t, ⋯⟩)).toLp t

theorem EulerOrdinarySobolev.Evolution.joinedVelocity_solenoidal {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (t : ↑(Set.Icc 0 (T + S))) : (U.joinedVelocity V t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

noncomputable def EulerOrdinarySobolev.Evolution.concatenate {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (hTpos : 0 < T) (hSpos : 0 < S) (hmatch : U.velocity ⟨T, ⋯⟩ = V.velocity ⟨0, ⋯⟩) : Evolution (T + S) ⋯

Concatenate, bundling velocity, pressureForce, velocity_continuous, pressure_continuous and the required compatibility proofs.

Equations

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

theorem EulerOrdinarySobolev.Evolution.concatenate_initial {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (hTpos : 0 < T) (hSpos : 0 < S) (hmatch : U.velocity ⟨T, ⋯⟩ = V.velocity ⟨0, ⋯⟩) : (U.concatenate V hTpos hSpos hmatch).velocity ⟨0, ⋯⟩ = U.velocity ⟨0, ⋯⟩

theorem EulerOrdinarySobolev.Evolution.concatenate_left {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (hTpos : 0 < T) (hSpos : 0 < S) (hmatch : U.velocity ⟨T, ⋯⟩ = V.velocity ⟨0, ⋯⟩) (t : ↑(Set.Icc 0 T)) : (U.concatenate V hTpos hSpos hmatch).velocity ⟨↑t, ⋯⟩ = U.velocity t

theorem EulerOrdinarySobolev.Evolution.concatenate_right {T S : ℝ} {hT : 0 ≤ T} {hS : 0 ≤ S} (U : Evolution T hT) (V : Evolution S hS) (hTpos : 0 < T) (hSpos : 0 < S) (hmatch : U.velocity ⟨T, ⋯⟩ = V.velocity ⟨0, ⋯⟩) (t : ↑(Set.Icc 0 S)) : (U.concatenate V hTpos hSpos hmatch).velocity ⟨T + ↑t, ⋯⟩ = V.velocity t