Products of whole-space Sobolev families

For an integer m ≥ 3, the product of two functions in H^m(ℝ³) lies in H^m(ℝ³), its ordered weak derivatives are given by the Leibniz family of the two factors, and ‖fg‖²_{H^m} ≤ C ‖f‖²_{H^m} ‖g‖²_{H^m}. This is the whole-space algebra inequality used in prop:lps-smoothing.

Each Leibniz term pairs two derivative orders with sum at most m, so one factor has at least two orders to spare and is essentially bounded by the embedding H^{k+2}(ℝ³) → L^∞. The weak Leibniz rule follows by approximating the first factor by smooth compactly supported functions: the Leibniz family of the difference is controlled by the same estimate. This reduction holds at every order where the weak Leibniz estimate is available.

theorem ESS.lps_sobolevFamily_ae_abs_le {m : ℕ} (hm : 2 ≤ m) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.IsSobolevFamilyOn m Set.univ f D → ∀ (β : List (Fin 3)), β.length + 2 ≤ m → ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), |D β x| ≤ C * √(CKN.sobolevNormSqOn m Set.univ D)

A slot of a whole-space Sobolev family at least two orders below m is essentially bounded by the Sobolev norm of the family (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_sobolevFamily_pair_bound_low {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 → ∀ (β γ : List (Fin 3)), β.length + γ.length ≤ m → β.length + 2 ≤ m ∨ γ.length + 2 ≤ m → 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 ≤ C ^ 2 * CKN.sobolevNormSqOn m Set.univ D * CKN.sobolevNormSqOn m Set.univ E

A product of two slots of total order at most m, one of which lies at least two orders below m, is square integrable, bounded by the two squared Sobolev norms (eq:lps-Hm-energy).

theorem ESS.lps_sobolevFamily_leibniz_normSq_le {m : ℕ} {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} {D E : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : CKN.IsSobolevFamilyOn m Set.univ f D) (hg : CKN.IsSobolevFamilyOn m Set.univ g E) (K : ℝ) (hpair : ∀ (β γ : List (Fin 3)), β.length + γ.length ≤ m → 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 ≤ K) : (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.sobolevLeibnizFamily α D E) 2 MeasureTheory.volume) ∧ (CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.sobolevLeibnizFamily α D E) ≤ (∑ α ∈ CKN.sobolevWords m, ↑(lpsLeibnizSplits α).length ^ 2) * K

If every product of two slots of total order at most m is square integrable with square integral at most K, then the Leibniz family of the two families is square integrable through order m, and its squared Sobolev norm is at most K times the number of Leibniz terms (eq:lps-Hm-energy).

theorem ESS.lps_sobolevFamily_mul_of_leibniz_bound {m : ℕ} (C : ℝ) (hbound : ∀ (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 → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (CKN.sobolevLeibnizFamily α D E) 2 MeasureTheory.volume) ∧ (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) {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} {D E : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : CKN.IsSobolevFamilyOn m Set.univ f D) (hg : 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

The weak Leibniz rule on ℝ³ (prop:lps-smoothing): if the Leibniz family of any two whole-space Sobolev families of order m is square integrable with the algebra bound, then the Leibniz family of D and E is a Sobolev family of the product f g. The first factor is approximated by smooth compactly supported functions, and the bound controls the Leibniz family of the difference.

theorem ESS.lps_sobolevFamily_mul {m : ℕ} (hm : 3 ≤ 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 an integer m ≥ 3, 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}.