Square-integrability of ordered regularized momentum derivatives

Every ordered spatial derivative of the regularized momentum right-hand side belongs to spatial L² when the velocity and canonical pressure have square-integrable derivatives of all orders.

theorem ESS.lps_regularized_equation_all_word_memLp (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) (huL2 : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) (hvL2 : ∀ (j : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) 2 MeasureTheory.volume) (hpL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α p) 2 MeasureTheory.volume) (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)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => q x i) 2 MeasureTheory.volume

The differentiated heat, tensor-divergence and pressure terms are square-integrable at every ordered spatial word (eq:lps-regularized-Hm-identity).

theorem ESS.lps_regR12TimeRHS_all_word_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (t : ℝ) (hJ : CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) (hp : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) (huL2 : ∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume) (hpL2 : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) 2 MeasureTheory.volume) (i : Fin 3) (α : List (Fin 3)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regR12TimeRHS ρ ε hε u p (x, t) i) 2 MeasureTheory.volume

On a smooth regularized slice, every ordered spatial derivative of the actual momentum right-hand side belongs to spatial L² (eq:lps-regularized-Hm-identity).