Theorem CPaper

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

theorem CKN.Main.caffarelliKohnNirenbergPaper (q : ℝ) (hq : 5 / 2 < q) (Ω : 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 → (Foundation.Parabolic.parabolicHausdorffMeasure 1) (SingularSet Ω I u) = 0

The parabolic singular set of a suitable weak solution of def:sws has zero one dimensional Hausdorff measure.