Theorem A

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

theorem CKN.Main.epsilonRegularityL3 (q : ℝ) (hq : 5 / 2 < q) : ∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ), 0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : 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 → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀ → ∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

The quantitative small-data regularity theorem for suitable weak solutions.