Sobolev control of the regularized transport field #
The H¹ Sobolev estimate is stated for a vector field and its specified gradient. It will be applied to the mollified transport field in the regularized H¹ energy estimate.
The L⁶ norm of an H¹(ℝ³) function is bounded by the Gagliardo–Nirenberg–Sobolev constant
times the L² norm of its gradient (lem:lps-H1-estimate).
theorem
ESS.LPS.lps_regularised_h1_vector_six_bound
{w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume)
(hDw2 : MeasureTheory.MemLp Dw 2 MeasureTheory.volume)
(hH1 :
∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => w x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Dw x i j)
:
Componentwise whole-space Sobolev control for a vector field whose
components are represented by the supplied H¹ functions.
theorem
ESS.LPS.lps_regMollified_velocity_l6_bound
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume)
(hu6 : MeasureTheory.MemLp u 6 MeasureTheory.volume)
:
Convolution does not increase the vector L⁶ norm beyond a fixed
coordinate factor. The factor is independent of the regularization scale.