The gradient regularity criterion for suitable weak solutions

theorem CKN.Core.Endgame.epsilonRegularityGradient_unconditional (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₀

Small scaled gradient energy implies regularity of a suitable weak solution.