Intermediate integrability of smooth Sobolev derivatives #
The first derivatives of a smooth whole-space H² function belong to
L⁴. This is the integrability part of the middle Leibniz split at
order two in eq:lps-Hm-energy.
theorem
ESS.lps_eLpNorm_four_le_two_six
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
:
MeasureTheory.eLpNorm f 4 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume ^ (1 / 4) * MeasureTheory.eLpNorm f 6 MeasureTheory.volume ^ (3 / 4)
Interpolation between the whole-space L² and L⁶ norms at
the L⁴ exponent (eq:lps-Hm-energy).
theorem
ESS.lps_smooth_first_derivative_memLp_four
(f : CKN.Foundation.Parabolic.Vec3 → ℝ)
(hf : ContDiff ℝ (↑⊤) f)
(hL2 : ∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume)
(j : Fin 3)
:
A smooth scalar field with all ordered derivatives through order two
in L² has every first derivative in L⁴ (eq:lps-Hm-energy).
theorem
ESS.lps_smooth_first_derivative_four_bound
(f : CKN.Foundation.Parabolic.Vec3 → ℝ)
(hf : ContDiff ℝ (↑⊤) f)
(hL2 : ∀ (α : List (Fin 3)), α.length ≤ 2 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume)
(j : Fin 3)
:
MeasureTheory.eLpNorm (CKN.spatialDeriv f j) 4 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (CKN.spatialDeriv f j) 2 MeasureTheory.volume ^ (1 / 4) * (CKN.gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm fun (k : Fin 3) => CKN.spatialDeriv (CKN.spatialDeriv f j) k x)
2 MeasureTheory.volume) ^ (3 / 4)
The first derivative's L⁴ norm is quantitatively controlled by
its L² norm and the L² norm of its full gradient
(eq:lps-Hm-energy).