Solenoidal ordered derivatives

Every ordered spatial derivative of a smooth divergence-free field is divergence free. This permits the pressure cancellation in eq:lps-regularized-Hm-identity at every Sobolev order.

theorem ESS.lps_wordDeriv_solenoidal {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (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)) (x : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, CKN.spatialDeriv (CKN.wordDeriv α fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) i x = 0

Ordered spatial derivatives preserve classical solenoidality (eq:lps-regularized-Hm-identity).