Whole-space gradient fourth-power bound #
The Gagliardo–Nirenberg estimate for smooth compactly supported
functions extends to smooth H² functions by whole-space integration
by parts. The L⁴ membership of the first derivatives supplies the
integrability needed at infinity.
theorem
ESS.lps_gradL4_sq_le_smooth_h2
(f : CKN.Foundation.Parabolic.Vec3 → ℝ)
(M : ℝ)
(hf : ContDiff ℝ (↑⊤) f)
(hL2 : ∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume)
(hM : ∀ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ M)
:
MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (∑ j : Fin 3, CKN.spatialDeriv f j x ^ 2) ^ 2)
MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ j : Fin 3, CKN.spatialDeriv f j x ^ 2) ^ 2 ≤ 28 * M ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ k : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv f j) k x ^ 2
A smooth whole-space H² scalar field with bound |f| ≤ M
satisfies the gradient L⁴ estimate without a support assumption
(eq:lps-Hm-energy).
theorem
ESS.lps_smooth_h2_gradient_four_energy :
∃ (C : ℝ),
0 ≤ C ∧ ∀ (f : CKN.Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) f →
(∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) →
MeasureTheory.Integrable
(fun (x : CKN.Foundation.Parabolic.Vec3) => (∑ j : Fin 3, CKN.spatialDeriv f j x ^ 2) ^ 2)
MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ j : Fin 3, CKN.spatialDeriv f j x ^ 2) ^ 2 ≤ C * (CKN.sobolevNormSqOn 2 Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α f) ^ 2
The fourth-power gradient integral of a smooth whole-space H²
function is bounded by the square of its ordered H² energy
(eq:lps-Hm-energy).
theorem
ESS.lps_smooth_h2_middle_product_energy :
∃ (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) →
∀ (α β : 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 ≤ (C * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ f) * CKN.sobolevNormSqOn 2 Set.univ fun (γ : List (Fin 3)) => CKN.wordDeriv γ g
The two-first-derivative Leibniz term in the whole-space H²
product estimate has one constant independent of the two fields
(eq:lps-Hm-energy).