Ordered derivatives of the regularized equation

For smooth fields, every ordered spatial derivative commutes with the heat, tensor-divergence and pressure-gradient terms in the regularized momentum equation.

theorem ESS.lps_regularized_equation_wordDeriv (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) (hPDE : ∀ (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), q x i = ∑ j : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) j) j x - ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j * u y i) j x - CKN.spatialDeriv p i x) (i : Fin 3) (α : List (Fin 3)) (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

The pointwise regularized momentum equation differentiates to every ordered spatial word (eq:lps-regularized-Hm-identity).