The axis-inclusive regular sphere of lem:aniso:annulus

This file derives, from the statement CIV.timeZeroSingularSetNull (the one-dimensional Hausdorff measure of the singular slice in the open unit ball is zero, axis included), the two steps of the regular-sphere argument of lem:aniso:annulus:

• hausdorffMeasure_singularSlice_closedBall_eq_zero: H¹(S₀) = 0 on closure (vec3Ball 0 R₀) for R₀ < 1, matching the manuscript's S₀ ⊆ closure B(R₀).
• exists_annulus_bound_of_timeZeroSingularSetNull: a uniform bound on a space-time annulus with radii in (R₁, R₀). The Euclidean radius vec3EuclideanNorm : Vec3 → ℝ is Lipschitz for the ambient (sup) metric on Vec3 that μH[1] is computed against (vec3EuclideanNorm_lipschitzWith, with the dimensional constant √3, since Vec3 carries the sup norm rather than the Euclidean one), so a null μH[1] set has a Lebesgue-null image under it (CIV.ae_notMem_image_of_hausdorffMeasure_one_eq_zero); almost every radius in (R₁, R₀) therefore carries no point of the singular slice, and the compactness step CIV.exists_annulus_bound_of_sphere_disjoint turns such a sphere into a uniform bound on a whole space-time annulus around it, shrunk to keep its radii inside (R₁, R₀).

The Euclidean radius is Lipschitz for the ambient (sup) metric on Vec3

theorem CIV.vec3EuclideanNorm_lipschitzWith : LipschitzWith (√3).toNNReal CKN.Foundation.Parabolic.vec3EuclideanNorm

vec3EuclideanNorm is Lipschitz for the ambient (sup) metric on Vec3 (Vec3 carries the sup norm, not the Euclidean one), with Lipschitz constant √3: the dimensional constant relating the two norms, CKN.Foundation.Parabolic.vec3EuclideanNorm_le_sqrt_three_mul_norm.

H¹(S₀) = 0 on closure B(R₀)

theorem CIV.hausdorffMeasure_singularSlice_closedBall_eq_zero (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) (R₀ : ℝ) (hR₀pos : 0 < R₀) (hR₀ : R₀ < 1) : (MeasureTheory.Measure.hausdorffMeasure 1) (singularSlice u ∩ closure (CKN.Foundation.Parabolic.vec3Ball 0 R₀)) = 0

The one-dimensional Hausdorff measure of the singular slice of the blow-up time, restricted to closure (vec3Ball 0 R₀) for R₀ < 1, is zero. An immediate corollary of the statement CIV.timeZeroSingularSetNull, since closure (vec3Ball 0 R₀) ⊆ vec3Ball 0 1 for 0 < R₀ < 1.

The axis-inclusive null radial projection

theorem CIV.ae_forall_vec3EuclideanNorm_ne_of_singularSlice (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) : ∀ᵐ (R : ℝ), ∀ x ∈ singularSlice u ∩ CKN.Foundation.Parabolic.vec3Ball 0 1, CKN.Foundation.Parabolic.vec3EuclideanNorm x ≠ R

Almost every radius carries no point of the (axis-inclusive) singular slice inside the open unit ball: the conclusion μH[1] (singularSlice u ∩ vec3Ball 0 1) = 0 of the statement CIV.timeZeroSingularSetNull pushed forward along the Lipschitz map vec3EuclideanNorm (vec3EuclideanNorm_lipschitzWith), using CIV.ae_notMem_image_of_hausdorffMeasure_one_eq_zero. This is the radial-projection step of lem:aniso:annulus.

A uniform bound on a space-time annulus in (R₁, R₀)

theorem CIV.exists_annulus_bound_of_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) (R₁ R₀ : ℝ) (hR₁ : 0 ≤ R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 1) : ∃ (Rlo : ℝ) (Rhi : ℝ) (t₀ : ℝ) (M : ℝ), R₁ < Rlo ∧ Rlo < Rhi ∧ Rhi < R₀ ∧ t₀ ∈ Set.Ioo (-1) 0 ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ M

The choice of radius in lem:aniso:annulus: given 0 ≤ R₁ < R₀ < 1, there are radii R₋ < R₊ inside (R₁, R₀), a time t₀ ∈ (-1, 0), and a bound M such that u is uniformly bounded, in Euclidean norm, on the cylindrical annulus {R₋ < |x| < R₊} × (t₀, 0). Almost every radius in (R₁, R₀) carries no point of the singular slice on its sphere (ae_forall_vec3EuclideanNorm_ne_of_singularSlice, from CIV.timeZeroSingularSetNull); since Ioo R₁ R₀ has positive Lebesgue measure such a radius R exists, and CIV.exists_annulus_bound_of_sphere_disjoint turns the sphere {|x| = R}, disjoint from the singular slice, into a uniform bound on an annulus around it by compactness; the annulus is finally shrunk so its inner and outer radii stay inside (R₁, R₀).