Uniqueness of actual smooth ordinary Euler evolutions, including their pressure force. No assumed energy inequality is needed.

theorem EulerOrdinarySobolev.smoothField_eq_of_toLp_eq (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (h : A.toLp = B.toLp) : A = B

theorem EulerOrdinarySobolev.Evolution.velocity_eq_of_initial {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (hinit : (V.velocity ⟨0, ⋯⟩).toLp = (U.velocity ⟨0, ⋯⟩).toLp) (t : ↑(Set.Icc 0 T)) : V.velocity t = U.velocity t

theorem EulerOrdinarySobolev.Evolution.pressure_eq_projected {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hpos : 0 < T) (t : ↑(Set.Icc 0 T)) : U.pressureForce t = pressureField (U.velocity t)

theorem EulerOrdinarySobolev.Evolution.pressure_eq_of_initial {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (hpos : 0 < T) (hinit : (V.velocity ⟨0, ⋯⟩).toLp = (U.velocity ⟨0, ⋯⟩).toLp) (t : ↑(Set.Icc 0 T)) : V.pressureForce t = U.pressureForce t