Corrected ordered energy inequality

The scale-independent transport estimate and the exact regularized energy identity imply the corrected high-order differential inequality. The identity is supplied by differentiating the regularized projected equation; its heat and pressure pairings are handled separately.

theorem ESS.lps_corrected_ordered_energy_of_identity (m : ℕ) (hm : 2 ≤ m) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t E' : ℝ), (CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) → (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) → (∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume) → have W := CKN.sobolevWords m; have N := ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i; have D := ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x ^ 2; have K := ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (y, t) j * u (y, t) i) x; E' + 2 * D = 2 * K → E' + D ≤ C * N ^ 2

The exact regularized energy identity yields the corrected H^m differential inequality once the transport tensor is bounded (eq:lps-Hm-energy).