Whole-space Sobolev control for smoothing

The local smooth Sobolev inequality gives an H² → L∞ bound for smooth fields with square-integrable derivatives on all of ℝ³. The source uses this bound when estimating the high-order transport tensor.

theorem ESS.lps_wordDeriv_append_words (α β : List (Fin 3)) (f : CKN.Foundation.Parabolic.Vec3 → ℝ) : CKN.wordDeriv β (CKN.wordDeriv α f) = CKN.wordDeriv (α ++ β) f

Applying two ordered derivative words in sequence is the derivative indexed by their concatenation (eq:lps-Hm-energy).

theorem ESS.lps_smooth_h2_uniform_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → MeasureTheory.MemLp f 2 MeasureTheory.volume → (∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv f j) 2 MeasureTheory.volume) → (∀ (j k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv f j) k) 2 MeasureTheory.volume) → ∀ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ C * √(CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f)

The whole-space H² norm bounds a smooth scalar field uniformly, without a compact-support assumption (eq:lps-Hm-energy).

theorem ESS.lps_lower_word_uniform_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ) (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (α : List (Fin 3)), ContDiff ℝ (↑⊤) f → (∀ (β : List (Fin 3)), β.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv β f) 2 MeasureTheory.volume) → α.length + 2 ≤ m → ∀ (x : CKN.Foundation.Parabolic.Vec3), |CKN.wordDeriv α f x| ≤ C * √(CKN.sobolevNormSqOn m Set.univ fun (β : List (Fin 3)) => CKN.wordDeriv β f)

An ordered derivative at least two orders below m is uniformly bounded by the full H^m energy (eq:lps-Hm-energy).

theorem ESS.lps_lower_word_product_integral_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ) (f g : CKN.Foundation.Parabolic.Vec3 → ℝ) (α β : List (Fin 3)), ContDiff ℝ (↑⊤) f → (∀ (γ : List (Fin 3)), γ.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv γ f) 2 MeasureTheory.volume) → (∀ (γ : List (Fin 3)), γ.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv γ g) 2 MeasureTheory.volume) → α.length + 2 ≤ m → β.length ≤ m → MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2 ≤ (C ^ 2 * CKN.sobolevNormSqOn m Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ f) * ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv β g x ^ 2

A lower derivative times any derivative through order m has a square-integrable product, controlled by the two ordered Sobolev energies (eq:lps-Hm-energy).

theorem ESS.lps_wordDeriv_integral_le_sobolev (m : ℕ) (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (α : List (Fin 3)) (hα : α.length ≤ m) : ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv α f x ^ 2 ≤ CKN.sobolevNormSqOn m Set.univ fun (β : List (Fin 3)) => CKN.wordDeriv β f

Each ordered derivative contributes a nonnegative summand to the whole H^m energy (eq:lps-Hm-energy).

theorem ESS.lps_word_pair_integral_bound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ) (f g : CKN.Foundation.Parabolic.Vec3 → ℝ) (α β : List (Fin 3)), 3 ≤ m → α.length + β.length ≤ m → ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (γ : List (Fin 3)), γ.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv γ f) 2 MeasureTheory.volume) → (∀ (γ : List (Fin 3)), γ.length ≤ m → MeasureTheory.MemLp (CKN.wordDeriv γ g) 2 MeasureTheory.volume) → MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2 ≤ (C ^ 2 * CKN.sobolevNormSqOn m Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ f) * CKN.sobolevNormSqOn m Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ g

At order at least three, each Leibniz split of total degree at most m has a factor with at least two unused derivatives. Its product is therefore controlled by the two H^m energies (eq:lps-Hm-energy).

theorem ESS.lps_word_pair_integral_bound_two_of_middle : ∃ (C₀ : ℝ), 0 ≤ C₀ ∧ ∀ (f g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) f → ContDiff ℝ (↑⊤) g → (∀ (γ : List (Fin 3)), γ.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv γ f) 2 MeasureTheory.volume) → (∀ (γ : List (Fin 3)), γ.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv γ g) 2 MeasureTheory.volume) → ∀ (M : ℝ), 0 ≤ M → (∀ (α β : List (Fin 3)), α.length = 1 → β.length = 1 → MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2 ≤ (M * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ f) * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ g) → ∀ (α β : List (Fin 3)), α.length + β.length ≤ 2 → MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.wordDeriv α f x * CKN.wordDeriv β g x) ^ 2 ≤ ((C₀ ^ 2 + M) * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ f) * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ g

At order two, the only Leibniz split outside the lower-derivative bound assigns one derivative to each factor. A quantitative bound for that middle split completes the termwise estimate (eq:lps-Hm-energy).