Spatial part of the regularized Sobolev identity

Pair each ordered derivative of the momentum equation with the corresponding velocity derivative. Heat integration by parts produces the gradient energy, tensor integration by parts produces the transport pairing, and solenoidality cancels pressure.

theorem ESS.lps_ordered_spatial_energy_identity (m : ℕ) (u v q : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.Vec3 → ℝ) (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), ∀ α ∈ CKN.sobolevWords m, ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => q y i) x = ∑ j : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv (CKN.wordDeriv α fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j) j x - ∑ j : Fin 3, CKN.spatialDeriv (CKN.wordDeriv α fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) j x - CKN.spatialDeriv (CKN.wordDeriv α p) i x) : (∑ 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) + ∑ 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 = ∑ 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 spatial pairings in the ordered regularized energy identity (eq:lps-regularized-Hm-identity). The derivative-level momentum equation is the output of differentiating the regularized evolution.