Products of whole-space Sobolev families of mixed order

The product of a function in H²(ℝ³) and a function in H¹(ℝ³) lies in H¹(ℝ³), its first-order weak derivatives are given by the Leibniz family of the two factors, and ‖fg‖²_{H¹} ≤ C ‖f‖²_{H²} ‖g‖²_{H¹}. This is the mixed-order form of the whole-space algebra inequality used in prop:lps-smoothing.

The undifferentiated factor f is essentially bounded by the embedding H²(ℝ³) → L^∞. The remaining Leibniz term ∂_j f · g pairs two functions of H¹(ℝ³); each lies in L⁴(ℝ³) by the whole-space Sobolev inequality and interpolation between L² and L⁶, and Hölder's inequality bounds the product in L². The weak Leibniz rule follows by approximating f in H² by smooth compactly supported functions.

theorem ESS.lpsMixedHolderTripleFourFourTwo : ENNReal.HolderTriple 4 4 2

theorem ESS.lps_sobolevFamily_mul_mixed : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ) (D E : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.IsSobolevFamilyOn 2 Set.univ f D → CKN.IsSobolevFamilyOn 1 Set.univ g E → (CKN.IsSobolevFamilyOn 1 Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α D E) ∧ (CKN.sobolevNormSqOn 1 Set.univ fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α D E) ≤ C * CKN.sobolevNormSqOn 2 Set.univ D * CKN.sobolevNormSqOn 1 Set.univ E

prop:lps-smoothing (the whole-space algebra inequality of mixed order): the product of a function in H²(ℝ³) and a function in H¹(ℝ³) lies in H¹(ℝ³), its first-order weak derivatives are the Leibniz family of the two factors' families, and ‖fg‖²_{H¹} ≤ C ‖f‖²_{H²} ‖g‖²_{H¹}.