The actual physical velocity and pressure force in every Sobolev order. Strong time evolution follows from their classical Euler equation and continuous L² jets, including both endpoint derivatives.

structure EulerParentPacketFrames.SobolevData {A : Parent} (E : Evolution A) : Type

Sobolev data, collecting velocity, force, velocity_match, force_match, velocity_continuous, force_continuous.

• velocity : ↑(Set.Icc 0 A.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Velocity field of SobolevData, of type Icc (0 : ℝ) A.T → SmoothL2Field Space.

• force : ↑(Set.Icc 0 A.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Force of SobolevData, of type Icc (0 : ℝ) A.T → SmoothL2Field Space.

• velocity_match (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : E.velocity (↑t, x) = (self.velocity t).field x
• force_match (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : E.force t x = (self.force t).field x
• velocity_continuous (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 A.T)) => (self.velocity t).jetLp n
• force_continuous (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 A.T)) => (self.force t).jetLp n

theorem EulerParentPacketFrames.SobolevData.strong_euler {A : Parent} {E : Evolution A} (S : SobolevData E) (q : ℕ) (t : ↑(Set.Icc 0 A.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath A.T ⋯ (EulerSmoothFieldSobolevTime.sobolevPath S.velocity ⋯ q)) ((EulerSmoothFieldSobolevTime.sobolevPath (EulerSmoothEulerEvolution.rhs S.velocity ⋯ S.force) ⋯ q) t) (Set.Icc 0 A.T) ↑t

def EulerParentPacketFrames.SobolevData.restrictTime {A : Parent} {E : Evolution A} (S : SobolevData E) (T : ℝ) (hT : 0 < T) (hTA : T ≤ A.T) : SobolevData (E.restrictTime T hT hTA)

Restrict time, bundling velocity, force, velocity_match, force_match and the required compatibility proofs.

Equations

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