Squared metric stability with a viscosity-sized source, including zero energy.

theorem EulerSquaredMetricStability.metric_derivative_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (K : ℝ → H →L[ℝ] H) (e : ℝ → H) (t ν c β h L ε M : ℝ) (K' : H →L[ℝ] H) (e' transport pressure forcing lap : H) (hc : 0 < c) (hν : 0 ≤ ν) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hL : 0 ≤ L) (hK : HasDerivAt K K' t) (he : HasDerivAt e e' t) (hsym : ∀ (v w : H), inner ℝ ((K t) v) w = inner ℝ v ((K t) w)) (hcoer : c ^ 2 * ‖e t‖ ^ 2 ≤ inner ℝ ((K t) (e t)) (e t)) (heq : e' + transport + pressure = forcing + ν • lap) (hp : inner ℝ ((K t) (e t)) pressure = 0) (ht : |inner ℝ ((K t) (e t)) transport| ≤ β * ‖e t‖ ^ 2) (hlap : inner ℝ ((K t) (e t)) lap ≤ h * ‖e t‖ ^ 2) (hf : ‖forcing‖ ≤ L * ‖e t‖ + ε * M) : deriv (fun (s : ℝ) => inner ℝ ((K s) (e s)) (e s)) t ≤ (‖K'‖ + 2 * β + 2 * ν * h + 2 * ‖K t‖ * L + 1) / c ^ 2 * inner ℝ ((K t) (e t)) (e t) + (‖K t‖ * M) ^ 2 * ε ^ 2

A literal transport-pressure-heat equation gives a squared metric differential bound without differentiating a zero norm.

theorem EulerSquaredMetricStability.linear_growth_bound (E E' : ℝ → ℝ) (A B T : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hT : 0 ≤ T) (hcont : ContinuousOn E (Set.Icc 0 T)) (hzero : E 0 ≤ 0) (hder : ∀ t ∈ Set.Ioo 0 T, HasDerivAt E (E' t) t) (hineq : ∀ t ∈ Set.Ioo 0 T, E' t ≤ A * E t + B) (t : ℝ) : t ∈ Set.Icc 0 T → E t ≤ B * T * Real.exp (A * T)

A genuine interior differential inequality yields a finite-interval linear-growth bound, including both endpoints.