Finiteness of the centered majorant on a local box #
The source membership required in eq:pressure-gradient-morrey follows on
any local box from the spatial Sobolev data of def:sws, at almost every
time of that box.
theorem
CKN.Core.Step4.origin_centered_source_memLp_ae_on_local_box
{Ω U : Set Foundation.Parabolic.Vec3}
{I J : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hbox : localBox Ω I U J)
{x : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hball : Foundation.Parabolic.vec3Ball x ρ ⊆ U)
(c : ℝ → Foundation.Parabolic.Vec3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (y : Foundation.Parabolic.Vec3) =>
pressureDivergenceCutoffSourceCentredTensor (mollifiedBallCutoff x hρ) (spatialDeriv (mollifiedBallCutoff x hρ))
(fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) y
i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume
The centered tensor source belongs to the global spatial L^{6/5}
space for almost every time in any local box containing its cutoff.