Time Zero Singular Set Null

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.timeZeroSingularSetNull (q : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (henergy : GlobalEnergyClass u Du p) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hMf : ForceC2Bounded f) : (MeasureTheory.Measure.hausdorffMeasure 1) (singularSlice u ∩ CKN.Foundation.Parabolic.vec3Ball 0 1) = 0

Partial regularity at the blow-up time (the manuscript's H¹(S₀) = 0, obtained there from Caffarelli–Kohn–Nirenberg / Gustafson–Kang–Tsai applied at points of the top boundary of Q): the set of points x ∈ B(1) near which u is unbounded as t ↑ 0 has one-dimensional Hausdorff measure zero.

This statement bundles CKN's partial regularity together with the Gustafson–Kang–Tsai criterion (their Theorem 1.1(ii)) applied at the points (x, 0) of the top boundary of Q, which the footnote in the proof of lem:aniso:annulus justifies from the structure of their proof (backward cylinders inside Q and a local energy inequality that, for a pair smooth on compact subsets of Q, is an identity at every s < 0); see design note R12. The proof uses less: see deviation D7 in docs/DEVIATIONS.md.