Whole-space ordered Sobolev algebra

Smooth H^m multiplication is bounded at every integer order m ≥ 2, including the critical middle Leibniz split at order two.

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

The ordered whole-space H^m energy is an algebra for every integer m ≥ 2 (eq:lps-Hm-energy).