The singly centred pressure estimate #
For ext:CZ and thm:B, the nine tensor components contribute a factor
of nine to the pressure constant. The suitable-solution slice and residual
estimates supply every analytic input of the scalar extension estimate.
theorem
CKN.Core.Endgame.theoremB_pressureP1_slice_of_sws
(C_CZ : ℝ)
(hC_CZ : 0 ≤ C_CZ)
(hoperator : Foundation.Euclidean.czP1OperatorConstant ≤ C_CZ)
{Ω : 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), MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s x)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ 9 * C_CZ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3)
The singly centred pressure slice bound of ext:CZ, including the
nine-component constant, from a suitable weak solution.
theorem
CKN.Core.Endgame.theoremB_hCZ_p1_of_sws
(q : ℝ)
(Ω : Set Foundation.Parabolic.Vec3)
(I : Set ℝ)
(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)
:
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} (hρ : 0 < ρ),
0 < r →
r ≤ ρ / 2 →
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm'
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f w.2 w.1)
(3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal
(9 * max Foundation.Euclidean.czP1OperatorConstant 0 * (9 * sobolevPoincareL6Constant.toReal) * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)
The solution-uniform pressure input for thm:B and ext:CZ, with
an explicit constant absorbing all nine tensor components.