Whole-space pressure cancellation #
The pressure gradient has zero energy pairing with a smooth
divergence-free field. This is the scalar integration-by-parts step
in eq:lps-regularized-Hm-identity.
theorem
ESS.lps_solenoidal_pressure_pairing_zero
{h : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hh : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => h x i)
(hp : ContDiff ℝ (↑⊤) p)
(hh0 : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => h x i) 2 MeasureTheory.volume)
(hh1 :
∀ (i : Fin 3),
MeasureTheory.MemLp (CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => h x i) i) 2 MeasureTheory.volume)
(hp0 : MeasureTheory.MemLp p 2 MeasureTheory.volume)
(hp1 : ∀ (i : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv p i) 2 MeasureTheory.volume)
(hdiv :
∀ (x : CKN.Foundation.Parabolic.Vec3),
∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => h y i) i x = 0)
:
The pressure term vanishes when its energy test field is solenoidal
(eq:lps-regularized-Hm-identity).