Sobolev Global H2Core #
Supporting estimates for the Navier–Stokes development.
The radius-two spatial ball on which the global H² core estimates are formulated.
Equations
Instances For
theorem
CKN.smooth_global_linf_uniform :
∃ (C : ℝ),
0 ≤ C ∧ ∀ {f : Foundation.Parabolic.Vec3 → ℝ},
ContDiff ℝ (↑⊤) f →
MeasureTheory.MemLp f 2 MeasureTheory.volume →
(∀ (i : Fin 3),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => (fderiv ℝ f x) (basisVec i))
(ENNReal.ofReal 6) MeasureTheory.volume) →
∀ (x : Foundation.Parabolic.Vec3),
|f x| ≤ C * (MeasureTheory.lpNorm f 2 MeasureTheory.volume + ∑ i : Fin 3,
MeasureTheory.lpNorm (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ f y) (basisVec i)) 6
MeasureTheory.volume)
Smooth functions with an L² value and coordinate L⁶ derivatives obey
the global pointwise estimate used by the weak embedding.