Morrey Form Fixed Scale #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.step2_fixed_scale_integrals
{Ω : 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 M : ℝ}
(hR : 0 < R)
(hM : 1 ≤ M)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 (2 * R)) ⊆ spaceTimeSet Ω I)
(hdec : max (max (alpha u z R) (beta u Du z R)) (delta p z R ^ 2) ≤ M * R ^ (2 / 5))
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 R, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≤ ENNReal.ofReal (R ^ 2 * (2 * gagliardoConstant * (M * R ^ (2 / 5))) ^ 3) ∧ ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 R, ENNReal.ofReal (spatialGradientSq u Du w) ≤ ENNReal.ofReal (M ^ 2 * R ^ (9 / 5)) ∧ ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 R, ENNReal.ofReal |p w| ^ (3 / 2) ≤ ENNReal.ofReal (M ^ (3 / 2) * R ^ (13 / 5))
Fixed-scale localized integrals are controlled by the decay certificate. The scale and the constants in this statement are independent of the solution and of the centre.