The L² size of the regularized transport term

Every slice of the transport term (J_ε U_ε · ∇) U_ε of the regularized velocity has square integrable derivatives, and its L² norm is bounded by S^{3/2} ‖∇U_ε‖₂^{3/2} ‖∇²U_ε‖₂^{1/2} (prop:lps-local-strong, the uniform time derivative bound).

theorem ESS.LPS.lps_smooth_mul_deriv_memLp {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf' : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) (hg : ContDiff ℝ (↑⊤) g) (hg' : ∀ (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) 2 MeasureTheory.volume ∧ ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) k) 2 MeasureTheory.volume

The product of two smooth functions with all ordered derivatives square integrable is square integrable, and so is its first derivative.

theorem ESS.LPS.lps_regR12_transportTerm_sq_le (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (k i : Fin 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsRegTransportTerm ρ ε hε b hb k i t x ^ 2 ≤ CKN.gagliardoNirenbergSobolevConstant.toReal ^ 3 * lpsRegGradEnergy ρ ε hε b hb t ^ (3 / 2) * lpsRegHessEnergy ρ ε hε b hb t ^ (1 / 2)

The L² size of one summand of the regularized transport term (prop:lps-local-strong).

theorem ESS.LPS.lps_regR12_transport_deriv_memLp (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) {t : ℝ} (ht : 0 ≤ t) (i k : Fin 3) : MeasureTheory.MemLp (CKN.spatialDeriv (lpsRegTransport ρ ε hε b hb i t) k) 2 MeasureTheory.volume

The transport term of the regularized momentum equation and its first derivatives are square integrable (prop:lps-local-strong).