Related estimates used together by the same construction modules.
The ordinary vorticity equation of a Comparator solution follows from its scalar-pressure, unforced Euler equation.
The ordinary curl identity for the Euler convection term on ℝ³.
Curl of the material convection term, including the compressible correction.
The form of curl transport used for incompressible Euler.
Ordinary gradients have zero ordinary curl.
Taking curl removes pressure and gives the Euler vorticity right-hand side.
Vorticity support along ordinary particle trajectories #
The ODE lemma only needs a bound on the coefficient along one compact trajectory. It does not assume a spatially uniform bound on the velocity or its derivatives. The transport theorem below uses an ordinary differential equation for vorticity, not a prescribed support condition.
Uniqueness of the zero solution of a continuous linear ODE, allowing only interior derivatives and continuity at the two endpoints.
A field satisfying the stretching equation along a genuine trajectory stays zero on that trajectory if it is initially zero. Coefficient boundedness follows from continuity on the compact time interval.
Compact initial support remains in its compact image whenever zero initial values are propagated along every trajectory and the flow has a right inverse at the specified time.
In particular each time slice has compact support.
The reference's joint smoothness in time-first coordinates.
The actual time derivative of vorticity, obtained by taking curl of the scalar-pressure Euler equation and commuting the ordinary derivatives.
The full spacetime derivative of ordinary curl satisfies the vorticity
stretching law in the material direction (1,v).
Joint smoothness in time-first coordinates, including the initial time.
Ordinary spatial derivatives remain jointly continuous at time zero.
Vorticity is jointly continuous through the initial time.
Zero vorticity is preserved on any genuine particle trajectory that exists on the whole compact time interval.
Vorticity support is contained in the image of its initial support under any complete continuous particle flow with a right inverse at the target time. The support propagation itself follows from the reference Euler equation.
Compact initial vorticity therefore stays compactly supported under a complete particle flow; no global bounds on spatial derivatives are assumed.
On a compact time interval all vorticity supports lie in one compact set: the image of the compact initial support swept out by the particle flow.
The actual radial-potential truncation of a Comparator Euler solution forms a smooth bounded coefficient family with uniformly bounded energy. No integrability of spatial derivatives of the original solution is needed.
Square-root reparametrization of the unit time interval.
Equations
- Euler.ComparatorBridge.unitSqrtTime = { toFun := fun (t : ↑(Set.Icc 0 1)) => ⟨√↑t, ⋯⟩, continuous_toFun := Euler.ComparatorBridge.unitSqrtTime._proof_4 }
Instances For
The square-time parametrization is jointly smooth and uniformly supported, so all its spatial jets form continuous bounded time paths.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reparametrizing by square root recovers the exact physical-time truncation, while retaining continuity of every bounded spatial jet.
Equations
Instances For
Every actual Comparator solution supplies the truncation family used by the finite-energy flow argument. The uniform energy is a fixed multiple of the reference solution's energy bound.
Equations
- One or more equations did not get rendered due to their size.