Theorem B #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.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),
IsSuitableWeakSolution Ω 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₀
Theorem B from paper label thm:B, with the gradient limsup taken in ℝ≥0∞.