Theorem BPaper

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Main.epsilonRegularityGradientPaper (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₀

The gradient regularity criterion, under the suitable weak-solution class of def:sws.