Ordered regularized energy identity

The differentiated pointwise momentum equation and the time derivative of the squared Sobolev energy give the exact high-order energy identity. The time differentiation is a separate Hilbert-space chain rule.

theorem ESS.lps_regularized_ordered_energy_identity (m : ℕ) (u v q : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.Vec3 → ℝ) (E' : ℝ) (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (hv : ∀ (j : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) (hp : ContDiff ℝ (↑⊤) p) (huL2 : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) (hvL2 : ∀ (j : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) 2 MeasureTheory.volume) (hpL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α p) 2 MeasureTheory.volume) (hdiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) i x = 0) (hPDE : ∀ (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), q x i = ∑ j : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j) j x - ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) j x - CKN.spatialDeriv p i x) (hchain : E' = 2 * ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => q y i) x) : E' + 2 * ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x ^ 2 = 2 * ∑ i : Fin 3, ∑ α ∈ CKN.sobolevWords m, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) x

The regularized pointwise equation and the squared-energy chain rule imply the exact ordered high-order identity (eq:lps-regularized-Hm-identity).