The centred pressure-gradient estimate from suitable-solution data #
All slice inputs to the unconditional gradient selector are supplied by
def:sws and cylinder containment. The numerical constants precede the
solution, and the source is the force-free centred tensor source.
theorem
CKN.Core.Step4.centredSWS_selected_gradient_ae
(C₁₇ C_P1 C₈ : ℝ)
(hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇)
(hC_P1 : 0 ≤ C_P1)
(hoperator : Foundation.Euclidean.czP1OperatorConstant ≤ C_P1)
(hC₈ : sliceForceGradientConstant ≤ C₈)
{Ω : Set Foundation.Parabolic.Vec3}
{I : 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)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) (euclideanBall z.1 (ρ / 2))
MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ∧ (∀ (k : Fin 3),
HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) =>
D x k) ∧ ∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x k) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal Foundation.Euclidean.czGradientOperatorConstant * ∑ _i : Fin 3, centredSWSCentredMajorant z.1 ρ q u Du f s + ENNReal.ofReal
(C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + 9 * C_P1 * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3) + harmonicRemainderForceBound z hρ f s) * ρ ^ (-1 / 2)) + ENNReal.ofReal (sliceForceGradientBound Foundation.Euclidean.czGradientOperatorConstant C₈ z.1 hρ f s)
Display (3.5) with the force-free centred source and every analytic slice input extracted from the suitable weak solution and cylinder geometry.