Scalar high-order energy bounds

The corrected high-order inequality in eq:lps-Hm-energy dissipates the spatial-gradient Sobolev norm. The lemmas here isolate its Young inequality and integrating-factor estimates for the regularized smoothing argument.

theorem ESS.lps_corrected_energy_from_transport {A B C K E' : ℝ} (hheat : E' + 2 * B ^ 2 ≤ 2 * K) (htransport : K ≤ C * A ^ 2 * B) : E' + B ^ 2 ≤ C ^ 2 * A ^ 4

Young's inequality turns the regularized transport pairing into the corrected spatial-gradient dissipation (eq:lps-Hm-energy).

theorem ESS.lps_corrected_energy_from_tensor {E' D N C K : ℝ} (hD : 0 ≤ D) (hN : 0 ≤ N) (hC : 0 ≤ C) (hheat : E' + 2 * D ≤ 2 * K) (htransport : K ≤ √C * N * √D) : E' + D ≤ C * N ^ 2

The transport-tensor estimate and the heat identity yield exactly the corrected inhomogeneous H^m energy inequality (eq:lps-Hm-energy).

theorem ESS.lps_high_order_energy_gronwall {a T C : ℝ} {y dy d b : ℝ → ℝ} (haT : a ≤ T) (hy : Continuous y) (hb : Continuous b) (hderiv : ∀ t ∈ Set.Ioo a T, HasDerivAt y (dy t) t) (hd : ∀ t ∈ Set.Ioo a T, 0 ≤ d t) (henergy : ∀ t ∈ Set.Ioo a T, dy t + d t ≤ C * b t * y t) (t : ℝ) : t ∈ Set.Icc a T → y t ≤ y a * Real.exp (C * ∫ (s : ℝ) in a..t, b s)

The scalar integrating-factor step used by the corrected high-order energy estimate (eq:lps-Hm-energy).

theorem ESS.lps_high_order_energy_dissipation_gronwall {a T C : ℝ} {y dy d b : ℝ → ℝ} (haT : a ≤ T) (hC : 0 ≤ C) (hy : Continuous y) (hdcont : Continuous d) (hbcont : Continuous b) (hderiv : ∀ t ∈ Set.Ioo a T, HasDerivAt y (dy t) t) (hd : ∀ (t : ℝ), 0 ≤ d t) (hb : ∀ (t : ℝ), 0 ≤ b t) (henergy : ∀ t ∈ Set.Ioo a T, dy t + d t ≤ C * b t * y t) (t : ℝ) : t ∈ Set.Icc a T → y t + ∫ (s : ℝ) in a..t, d s ≤ y a * Real.exp (C * ∫ (s : ℝ) in a..t, b s)

The corrected high-order energy inequality controls both the energy and the integrated spatial-gradient dissipation (eq:lps-Hm-energy).

theorem ESS.lps_high_order_energy_uniform_bound {a T C M₀ M₁ : ℝ} {y dy d b : ℝ → ℝ} (haT : a ≤ T) (hC : 0 ≤ C) (hM₀ : 0 ≤ M₀) (hy : Continuous y) (hdcont : Continuous d) (hbcont : Continuous b) (hderiv : ∀ t ∈ Set.Ioo a T, HasDerivAt y (dy t) t) (hd : ∀ (t : ℝ), 0 ≤ d t) (hb : ∀ (t : ℝ), 0 ≤ b t) (henergy : ∀ t ∈ Set.Ioo a T, dy t + d t ≤ C * b t * y t) (hinit : y a ≤ M₀) (hcoeff : ∀ t ∈ Set.Icc a T, ∫ (s : ℝ) in a..t, b s ≤ M₁) (t : ℝ) : t ∈ Set.Icc a T → y t + ∫ (s : ℝ) in a..t, d s ≤ M₀ * Real.exp (C * M₁)

Bounds on the initial Sobolev energy and lower-order coefficient give a scale-independent higher-order estimate (eq:lps-Hm-energy).

theorem ESS.lps_high_order_bound_of_heat_transport {a T C M₀ M₁ : ℝ} {A B K E' : ℝ → ℝ} (haT : a ≤ T) (hM₀ : 0 ≤ M₀) (hA : Continuous A) (hB : Continuous B) (hderiv : ∀ t ∈ Set.Ioo a T, HasDerivAt (fun (s : ℝ) => A s ^ 2) (E' t) t) (hheat : ∀ t ∈ Set.Ioo a T, E' t + 2 * B t ^ 2 ≤ 2 * K t) (htransport : ∀ t ∈ Set.Ioo a T, K t ≤ C * A t ^ 2 * B t) (hinit : A a ^ 2 ≤ M₀) (hcoeff : ∀ t ∈ Set.Icc a T, ∫ (s : ℝ) in a..t, A s ^ 2 ≤ M₁) (t : ℝ) : t ∈ Set.Icc a T → A t ^ 2 + ∫ (s : ℝ) in a..t, B s ^ 2 ≤ M₀ * Real.exp (C ^ 2 * M₁)

A regularized high-order heat pairing and tensor transport bound give a uniform energy and gradient-dissipation bound (eq:lps-Hm-energy). The two pairing bounds are proved from the regularized equation in the ordered-energy step.