All-order smooth product integrability

The integer Sobolev algebra estimate gives square integrability for every ordered derivative of a product when both factors have it.

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

Products of smooth fields with all ordered derivatives in L² retain that property (eq:lps-regularized-Hm-identity).