Products of whole-space Sobolev families at order two

At order two, the Leibniz term ∂_i f ∂_j g pairs two first derivatives, neither of which is bounded by the H² norm. The smooth Gagliardo–Nirenberg estimate bounds this term for smooth fields; Fatou's lemma along an almost everywhere convergent subsequence of smooth approximations transfers the bound to whole-space Sobolev families. The other Leibniz terms contain an undifferentiated factor, which is essentially bounded. Together with the order m ≥ 3 case, the product of two H^m(ℝ³) functions lies in H^m(ℝ³) for every m ≥ 2, with the Leibniz family as its weak derivatives.

theorem ESS.lps_sobolevFamily_middle_bound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ) (D E : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.IsSobolevFamilyOn 2 Set.univ f D → CKN.IsSobolevFamilyOn 2 Set.univ g E → ∀ (β γ : List (Fin 3)), β.length = 1 → γ.length = 1 → MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => D β x * E γ x) 2 MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (D β x * E γ x) ^ 2 ≤ M * CKN.sobolevNormSqOn 2 Set.univ D * CKN.sobolevNormSqOn 2 Set.univ E

The product of two first-order slots of whole-space H² families is square integrable, bounded by the two squared H² norms with a universal constant (eq:lps-Hm-energy).

theorem ESS.lps_sobolevFamily_mul_two : ∃ (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 2 Set.univ g E → (CKN.IsSobolevFamilyOn 2 Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α D E) ∧ (CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α D E) ≤ C * CKN.sobolevNormSqOn 2 Set.univ D * CKN.sobolevNormSqOn 2 Set.univ E

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

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

prop:lps-smoothing (the whole-space algebra inequality): for every integer m ≥ 2, the product of two functions in H^m(ℝ³) lies in H^m(ℝ³), its ordered weak derivatives are the Leibniz family of the two factors' families, and ‖fg‖²_{H^m} ≤ C ‖f‖²_{H^m} ‖g‖²_{H^m}.