Scalar Grönwall estimate for vorticity energy

This scalar estimate is the time integration step in the smooth energy argument for lem:localized-vorticity-energy.

theorem ESS.vorticityEnergyGronwallCore {a b K e₀ : ℝ} {e de f : ℝ → ℝ} (hab : a ≤ b) (hK : 0 ≤ K) (hecont : ContinuousOn e (Set.Icc a b)) (hfcont : Continuous f) (hepos : ∀ t ∈ Set.Icc a b, 0 ≤ e t) (hfpos : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hederiv : ∀ t ∈ Set.Ico a b, HasDerivAt e (de t) t) (hineq : ∀ t ∈ Set.Ico a b, de t ≤ K * e t + f t) (hinit : e a ≤ e₀) (t : ℝ) : t ∈ Set.Icc a b → e t ≤ Real.exp (K * (b - a)) * (e₀ + ∫ (s : ℝ) in a..b, f s)

A nonnegative energy with a differential upper bound has the expected exponential control by its initial value and the total forcing.

theorem ESS.vorticityEnergyGronwallDissipation {a b K e₀ : ℝ} {e de d f : ℝ → ℝ} (hab : a ≤ b) (hK : 0 ≤ K) (hecont : ContinuousOn e (Set.Icc a b)) (hdecont : Continuous de) (hdcont : Continuous d) (hfcont : Continuous f) (hepos : ∀ t ∈ Set.Icc a b, 0 ≤ e t) (hdpos : ∀ t ∈ Set.Icc a b, 0 ≤ d t) (hfpos : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hederiv : ∀ t ∈ Set.Ico a b, HasDerivAt e (de t) t) (hineq : ∀ t ∈ Set.Icc a b, de t + d t ≤ K * e t + f t) (hinit : e a ≤ e₀) : (∀ t ∈ Set.Icc a b, e t ≤ Real.exp (K * (b - a)) * (e₀ + ∫ (s : ℝ) in a..b, f s)) ∧ ∫ (t : ℝ) in a..b, d t ≤ e₀ + K * (b - a) * (Real.exp (K * (b - a)) * (e₀ + ∫ (s : ℝ) in a..b, f s)) + ∫ (s : ℝ) in a..b, f s

The scalar differential energy inequality controls both the supremum of the energy and the time integral of a nonnegative dissipation term.