Theorem C from the gradient criterion of Theorem B

This module derives the global nullity of the parabolic singular set (paper label thm:C) from the ε-regularity criterion of paper label thm:B, stated with the gradient limsup criterion. The analytic content is entirely in thm:B; the reduction from the criterion to vanishing one dimensional parabolic Hausdorff measure is CKN.singularSet_null_of_gradient_criterion_closed from CKN/Covering/TheoremCReductionClosed.lean.

The hypothesis hB below expresses the gradient criterion of thm:B for IsSuitableWeakSolutionIntegrable. The public theorem uses the equivalent suitable-solution class; the class-equivalence bridge supplies this version when assembling Theorem C.

theorem CKN.caffarelliKohnNirenberg_of_epsilonRegularityGradient (hB : ∀ (q : ℝ), 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₀) (q : ℝ) : 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), IsSuitableWeakSolutionIntegrable Ω I q u Du p f → (Foundation.Parabolic.parabolicHausdorffMeasure 1) (SingularSet Ω I u) = 0

Theorem C (paper label thm:C) follows from the gradient ε-regularity criterion of Theorem B (paper label thm:B). The criterion is taken as the hypothesis hB for IsSuitableWeakSolutionIntegrable, with the same gradient limsup condition and regular-point conclusion.