Leibniz rules for local Sobolev families

Smooth scalar multipliers act on the ordered weak derivative families used to define the local integer Sobolev spaces.

def CKN.sobolevLeibnizFamily : List (Fin 3) → (List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ) → (List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ

Leibniz family of a product; the first letter of the word is applied first.

Equations

• One or more equations did not get rendered due to their size.
• CKN.sobolevLeibnizFamily [] x✝¹ x✝ = fun (x : CKN.Foundation.Parabolic.Vec3) => x✝¹ [] x * x✝ [] x

theorem CKN.IsSobolevFamilyOn.smooth_mul {m : ℕ} {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {χ f : Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχb : ∀ (α : List (Fin 3)), α.length ≤ m → ∃ (L : ℝ), ∀ (x : Foundation.Parabolic.Vec3), |wordDeriv α χ x| ≤ L) (h : IsSobolevFamilyOn m U f D) : IsSobolevFamilyOn m U (fun (x : Foundation.Parabolic.Vec3) => χ x * f x) fun (α : List (Fin 3)) => sobolevLeibnizFamily α (fun (β : List (Fin 3)) => wordDeriv β χ) D

Multiplication by a smooth function with bounded derivatives preserves a local Sobolev family, with the ordered Leibniz formula for every derivative.

theorem CKN.IsSobolevFamilyOn.smooth_mul_univ {m : ℕ} {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {χ f : Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχU : tsupport χ ⊆ U) (h : IsSobolevFamilyOn m U f D) : IsSobolevFamilyOn m Set.univ (fun (x : Foundation.Parabolic.Vec3) => χ x * f x) fun (α : List (Fin 3)) => sobolevLeibnizFamily α (fun (β : List (Fin 3)) => wordDeriv β χ) D

A compactly supported smooth multiplier supported in an open set produces a whole-space Sobolev family by zero extension.

theorem CKN.sobolevLeibnizFamily_normSq_le (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (U V : Set Foundation.Parabolic.Vec3) (A B : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ) (L : ℝ), MeasurableSet U → MeasurableSet V → U ⊆ V → (∀ (α : List (Fin 3)), α.length ≤ m → ∀ (x : Foundation.Parabolic.Vec3), |A α x| ≤ L) → (∀ (α : List (Fin 3)), α.length ≤ m → ∀ x ∉ U, A α x = 0) → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.AEStronglyMeasurable (A α) (MeasureTheory.volume.restrict V)) → (∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (B α) 2 (MeasureTheory.volume.restrict V)) → (sobolevNormSqOn m V fun (α : List (Fin 3)) => sobolevLeibnizFamily α A B) ≤ C * L ^ 2 * sobolevNormSqOn m (U ∩ V) B

The squared Sobolev norm of a Leibniz family is controlled by the squared norm of its second factor when all derivatives of the first factor are bounded and supported in U.