Square integrability of products of smooth H¹ functions #
Hölder's inequality with exponents (6, 3, 2), the interpolation of L³ between L² and L⁶,
and the homogeneous H¹ → L⁶ inequality bound the L² norm of the product of two smooth functions
with square integrable gradients (prop:lps-local-strong, the time derivative bound of the
regularized solutions).
theorem
ESS.LPS.lps_smooth_mul_memLp_two_norm_le
{V d : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hV : ContDiff ℝ (↑⊤) V)
(hV2 : MeasureTheory.MemLp V 2 MeasureTheory.volume)
(hVd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv V k) 2 MeasureTheory.volume)
(hd : ContDiff ℝ (↑⊤) d)
(hd2 : MeasureTheory.MemLp d 2 MeasureTheory.volume)
(hdd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv d k) 2 MeasureTheory.volume)
:
MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => V x * d x) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => V x * d x) 2 MeasureTheory.volume).toReal ≤ CKN.gagliardoNirenbergSobolevConstant.toReal * √(∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv V k x ^ 2) * (√(∫ (x : CKN.Foundation.Parabolic.Vec3), d x ^ 2) ^ (1 / 2) * (CKN.gagliardoNirenbergSobolevConstant.toReal * √(∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv d k x ^ 2)) ^ (1 / 2))
The product of two smooth functions with square integrable gradients is square integrable,
with the
L² norm bounded by S ‖∇V‖₂ ‖d‖₂^{1/2} (S ‖∇d‖₂)^{1/2}, S the Sobolev constant.
theorem
ESS.LPS.lps_smooth_mul_sq_integral_le
{V d : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hV : ContDiff ℝ (↑⊤) V)
(hV2 : MeasureTheory.MemLp V 2 MeasureTheory.volume)
(hVd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv V k) 2 MeasureTheory.volume)
(hd : ContDiff ℝ (↑⊤) d)
(hd2 : MeasureTheory.MemLp d 2 MeasureTheory.volume)
(hdd : ∀ (k : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv d k) 2 MeasureTheory.volume)
{y0 h0 : ℝ}
(hy : 0 ≤ y0)
(hh : 0 ≤ h0)
(h1 : ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv V k x ^ 2 ≤ y0)
(h2 : ∫ (x : CKN.Foundation.Parabolic.Vec3), d x ^ 2 ≤ y0)
(h3 : ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv d k x ^ 2 ≤ h0)
:
The squared L² norm of the product of two smooth functions with square integrable gradients,
in integral form.