Theorem B #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Theorem BProvider #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The gradient criterion from neighborhood regularity #
The lower-level conditional reduction consumes a local Hölder conclusion; it is not a proof of the gradient criterion. The producer theorem instead derives local regularity from the explicit pressure-gradient, velocity-improvement, localized-equation, and source estimates. Both use the extended-real neighborhood decay theorem.
theorem
CKN.epsilonRegularityGradient_provider_of_producers
(q C₁₂_p1 : ℝ)
(hq : 5 / 2 < q)
(hCZ_p1 :
∀ (Ω : 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 (C₁₂_p1 * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ))
(hG :
∀ (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) →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆
⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (R / 2) →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ morreyVecMem (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (Metric.ball z₀ (R / 2)) Dp)
(hL :
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ},
φ ∈ spaceTimeTestFunction Ω I →
∀ {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ},
localBox Ω I Ω' J →
tsupport φ ⊆ Ω' ×ˢ J →
∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
(∀ (i : Fin 3),
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) →
(∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Ω' ×ˢ J →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) →
Core.Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume]
fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
Core.HeatPotential.heatPotential
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
Core.Step4.localizedGradientSourceG φ u Du f Dp w i)
(fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) =>
Core.Step4.localizedGradientSourceH φ u j w i)
z)
:
∃ (ε₁ : ℝ),
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 extended-real gradient criterion follows from the explicit theta, pressure-gradient, velocity-improvement, localized-equation, and source estimates. No local regularity conclusion is assumed.
theorem
CKN.Main.epsilonRegularityGradient
(q : ℝ)
(hq : 5 / 2 < 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 regularity criterion for suitable weak solutions.