Exact conservation of kinetic energy for the ordinary smooth Euler class, using the genuine noncompact transport and pressure cancellations.

theorem EulerOrdinarySobolev.Evolution.velocity_derivative_inner_zero {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : inner ℝ (U.velocity t).toLp (U.derivative t).toLp = 0

theorem EulerOrdinarySobolev.Evolution.kineticEnergy_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => ‖(U.velocity (Set.projIcc 0 T hT r)).toLp‖ ^ 2) 0 (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.kineticEnergy_conserved {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : ‖(U.velocity t).toLp‖ ^ 2 = ‖(U.velocity ⟨0, ⋯⟩).toLp‖ ^ 2

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