The actual particle-parent Euler solution supplies the ordinary Sobolev evolution used by the H³ stability estimate. The solenoidal constraint at the endpoints follows by L² continuity from the interior.

theorem EulerParentPacketFrames.SobolevData.velocity_solenoidal {A : Parent} {E : Evolution A} (S : SobolevData E) (t : ↑(Set.Icc 0 A.T)) : (S.velocity t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

def EulerParentPacketFrames.SobolevData.ordinaryEvolution {A : Parent} {E : Evolution A} (S : SobolevData E) : EulerOrdinarySobolev.Evolution A.T ⋯

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

Equations

• S.ordinaryEvolution = { velocity := S.velocity, pressureForce := S.force, velocity_continuous := ⋯, pressure_continuous := ⋯, solenoidal := ⋯, gradient := ⋯, time_law := ⋯ }