Ordered Sobolev bound for the transport tensor

The scalar H^m algebra estimate applies componentwise to the advecting-velocity tensor, with one constant independent of the regularizing scale.

theorem ESS.lps_smooth_transport_tensor_normSq (m : ℕ) (hm : 2 ≤ m) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (v u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (j : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) → (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) → (∀ (j : Fin 3) (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) 2 MeasureTheory.volume) → (∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) 2 MeasureTheory.volume) → (∀ (i j : Fin 3) (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j * u x i) 2 MeasureTheory.volume) ∧ (∑ i : Fin 3, ∑ j : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j * u x i) ≤ (C * ∑ j : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => v x j) * ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u x i

For m ≥ 2, the ordered H^m energy of v ⊗ u is bounded by the product of the componentwise energies of v and u (eq:lps-Hm-energy).