Mixed-order products of space-time Sobolev families

A field in L²(I; H²(ℝ³)) whose H² slices are uniformly bounded in time multiplies L²(I; H¹(ℝ³)) into itself, and the space-time Leibniz family is the family of weak derivatives of the product. The slice estimate is the mixed-order whole-space product estimate H² × H¹ → H¹; it integrates in time as in the equal-order case. This is the product estimate for the nonlinear term at the base level of prop:lps-smoothing.

theorem ESS.lps_spaceTime_mul_family_mixed : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {a b : ℝ} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {Df Dg : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {K : ℝ}, CKN.IsL2SobolevFamilyOn 2 Set.univ (Set.Ioo a b) f Df → CKN.IsL2SobolevFamilyOn 1 Set.univ (Set.Ioo a b) g Dg → (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∑ α ∈ CKN.sobolevWords 2, ∫ (x : CKN.Foundation.Parabolic.Vec3), Df α (x, t) ^ 2 ≤ K) → (CKN.IsL2SobolevFamilyOn 1 Set.univ (Set.Ioo a b) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z * g z) fun (α : List (Fin 3)) => stLeibniz α Df Dg) ∧ (CKN.l2SobolevNormSqOn 1 Set.univ (Set.Ioo a b) fun (α : List (Fin 3)) => stLeibniz α Df Dg) ≤ C * K * CKN.l2SobolevNormSqOn 1 Set.univ (Set.Ioo a b) Dg

The mixed-order space-time product estimate (prop:lps-smoothing): a field f in L²(I; H²(ℝ³)) whose H² slices have squared norm at most K multiplies g ∈ L²(I; H¹(ℝ³)) into L²(I; H¹(ℝ³)); the product has the space-time Leibniz family and ‖fg‖²_{L²H¹} ≤ C K ‖g‖²_{L²H¹}.