Conditional nullity of the singular set #
This module formalizes the reduction from the gradient criterion to vanishing parabolic one dimensional Hausdorff measure. The criterion is supplied as a hypothesis so that a later regularity theorem can instantiate it directly.
theorem
CKN.singularSet_null_of_gradient_criterion_closed
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
(hq : 5 / 2 < q)
(ε₁ : ℝ)
(hε : 0 < ε₁)
{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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hcrit :
∀ 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₀)
: