Spatial pairing of a differentiated momentum equation

For one scalar component and one ordered derivative, whole-space integration by parts converts the Laplacian into gradient dissipation and moves tensor divergence onto the test derivative.

theorem ESS.lps_spatial_energy_component {h q p : CKN.Foundation.Parabolic.Vec3 → ℝ} {F : Fin 3 → CKN.Foundation.Parabolic.Vec3 → ℝ} (i : Fin 3) (hh : ContDiff ℝ (↑⊤) h) (hF : ∀ (j : Fin 3), ContDiff ℝ (↑⊤) (F j)) (h0 : MeasureTheory.MemLp h 2 MeasureTheory.volume) (h1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv h j) 2 MeasureTheory.volume) (h2 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv h j) j) 2 MeasureTheory.volume) (hF0 : ∀ (j : Fin 3), MeasureTheory.MemLp (F j) 2 MeasureTheory.volume) (hF1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (F j) j) 2 MeasureTheory.volume) (hp1 : MeasureTheory.MemLp (CKN.spatialDeriv p i) 2 MeasureTheory.volume) (hPDE : ∀ (x : CKN.Foundation.Parabolic.Vec3), q x = ∑ j : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv h j) j x - ∑ j : Fin 3, CKN.spatialDeriv (F j) j x - CKN.spatialDeriv p i x) : (∫ (x : CKN.Foundation.Parabolic.Vec3), h x * q x) + ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv h j x ^ 2 = (∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv h j x * F j x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), h x * CKN.spatialDeriv p i x

The spatial energy pairing of a differentiated momentum component (eq:lps-regularized-Hm-identity).