L² stability with the actual time integral of the reference gradient. The spatial cancellation is exact; no energy differential inequality is assumed.

theorem EulerOrdinarySobolev.Evolution.l2EnergyDerivative_gradient {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : U.l2EnergyDerivative V t ≤ 2 * U.gradientNormPath t * (U.l2EnergyPath V) t

theorem EulerOrdinarySobolev.Evolution.l2_energy_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : ‖(U.difference V t).toLp‖ ^ 2 ≤ ‖(U.difference V ⟨0, ⋯⟩).toLp‖ ^ 2 * Real.exp (2 * U.gradientIntegral t)

theorem EulerOrdinarySobolev.Evolution.l2_stability_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : ‖(U.difference V t).toLp‖ ≤ ‖(U.difference V ⟨0, ⋯⟩).toLp‖ * Real.exp (U.gradientIntegral t)

theorem EulerOrdinarySobolev.Evolution.velocityPath_norm_sub_le_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (G : ℝ) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.gradientIntegral t ≤ G) : ‖V.velocityPath - U.velocityPath‖ ≤ ‖V.velocityPath ⟨0, ⋯⟩ - U.velocityPath ⟨0, ⋯⟩‖ * Real.exp G