Theorem C

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

theorem CKN.caffarelliKohnNirenberg (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

Theorem C, paper label thm:C; as explained in docs/DESIGN_NOTES.md, it uses Mathlib's parabolic Hausdorff measure.