High-order pressure cancellation

The pressure-gradient pairing vanishes at every ordered Sobolev derivative because the differentiated velocity remains solenoidal.

theorem ESS.lps_wordDeriv_pressure_pairing_zero {u : 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) (hp : ContDiff ℝ (↑⊤) p) (hdiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) i x = 0) (α : List (Fin 3)) (hu0 : ∀ (i : Fin 3), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) (hu1 : ∀ (i : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) i) 2 MeasureTheory.volume) (hp0 : MeasureTheory.MemLp (CKN.wordDeriv α p) 2 MeasureTheory.volume) (hp1 : ∀ (i : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.wordDeriv α p) i) 2 MeasureTheory.volume) : ∑ i : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) x * CKN.spatialDeriv (CKN.wordDeriv α p) i x = 0

Every ordered derivative has zero whole-space pressure pairing (eq:lps-regularized-Hm-identity).