Identification CZP1 Unconditional #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The global indexed extension is used for the pressure term. The local slice estimate is the only interface needed by the cylinder bridge.
theorem
CKN.pressureP1_thetaDecay_hCZ_of_global_slice
(C₁₂_p1 C_CZ : ℝ)
(hC_CZ : 0 ≤ C_CZ)
(hconst : C_CZ * (9 * sobolevPoincareL6Constant.toReal) ≤ C₁₂_p1)
{Ω : 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}
{ρ r : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hCZ_p1 :
∀ᵐ (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 ≤ C_CZ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, utensorNorm u z.1 ρ s y ^ (3 / 2)) ^ (2 / 3))
:
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 (C₁₂_p1 * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)
Transfer the singly-centred slice certificate to the exact pressure input
of the theta-decay display (paper label: ext:CZ).