The gradient regularity criterion from a small-cell majorant #
For thm:B, suitable-solution slice derivatives determine one measurable
pressure gradient. The slice majorant in sec:pressure transfers to this
field by uniqueness. Finite covering supplies its whole-carrier integral,
and the two cell regimes give the pressure-gradient input of the criterion.
theorem
CKN.Core.Endgame.theoremB_measurable_pressure_gradient_of_sws
{Ω : 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 : ℝ}
(hR : 0 < R)
(hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I)
:
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (z₀.2 - R ^ 2) (z₀.2 + R ^ 2)), ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball z₀.1 (3 * R / 4)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z₀.1 (3 * R / 4)) i (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) i
Suitability supplies one measurable weak pressure gradient on a larger
spatial carrier throughout the symmetric time window of thm:B.
theorem
CKN.Core.Endgame.theoremB_gradient_producer_of_small_cell_majorant
(hGaugeCorrectedSmallCellMajorant :
∀ (q τ : ℝ),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
∀ {Ω : 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 : ℝ),
0 < R →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
morreyVecMem 3 τ (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) →
∃ (A : ENNReal) (N : Fin 3 → Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal),
A < ⊤ ∧ (∀ (i : Fin 3) (c : Foundation.Parabolic.Vec3) (t ρ : ℝ),
0 < ρ →
closure (Foundation.Parabolic.parabolicCylinder c t ρ) ⊆ spaceTimeSet Ω I →
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - ρ ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2))
MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i
(fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N i c t ρ s) ∧ ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ),
0 < r →
r ≤ R / 16 →
(Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Metric.ball z₀ (R / 2)).Nonempty →
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2, N i z.1 z.2 (2 * r) s ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
:
A finite small-cell slice majorant supplies the full pressure-gradient
input of thm:B; the carrier integral follows by finite covering.
theorem
CKN.Core.Endgame.epsilonRegularityGradient_closer_of_small_cell_majorant
(q : ℝ)
(hq : 5 / 2 < q)
(hGaugeCorrectedSmallCellMajorant :
∀ (q τ : ℝ),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
∀ {Ω : 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 : ℝ),
0 < R →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
morreyVecMem 3 τ (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) →
∃ (A : ENNReal) (N : Fin 3 → Foundation.Parabolic.Vec3 → ℝ → ℝ → ℝ → ENNReal),
A < ⊤ ∧ (∀ (i : Fin 3) (c : Foundation.Parabolic.Vec3) (t ρ : ℝ),
0 < ρ →
closure (Foundation.Parabolic.parabolicCylinder c t ρ) ⊆ spaceTimeSet Ω I →
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t - ρ ^ 2) t), ∃ (g : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.LocallyIntegrableOn g (euclideanBall c (ρ / 2))
MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall c (ρ / 2)) i
(fun (y : Vec 3) => p (y, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall c (ρ / 2))) ≤ N i c t ρ s) ∧ ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ),
0 < r →
r ≤ R / 16 →
(Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Metric.ball z₀ (R / 2)).Nonempty →
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2, N i z.1 z.2 (2 * r) s ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
:
∃ (ε₁ : ℝ),
0 < ε₁ ∧ ∀ (Ω : 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₀ ∈ spaceTimeSet Ω I,
Filter.limsup
(fun (r : ℝ) =>
(ENNReal.ofReal r)⁻¹ * ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r, ENNReal.ofReal (spatialGradientSq u Du w))
(nhdsWithin 0 (Set.Ioi 0)) < ENNReal.ofReal (ε₁ ^ 2) →
IsRegularPoint Ω I u z₀
The gradient criterion thm:B, conditional only on the finite
small-cell majorant for the pressure-gradient slices in sec:pressure.