The spatial Vitali covering step of the statement CIV.timeZeroSingularSetNull

This file proves the spatial analogue of Caffarelli–Kohn–Nirenberg's covering step step:thmC-covering: if a set S of spatial points carries a uniform lower bound ε r on the finite Dirichlet integral ∫⁻ |∇u|² of backward parabolic cylinders B(x, r) × (-r², 0) at arbitrarily small radii, then S ∩ B(1) has one-dimensional Hausdorff measure zero. The route covers S ∩ B(1) at each scale by a disjoint (Vitali) subfamily of such cylinders, compares the sum of the lower bounds against the finite integral over a shrinking backward time slab, and lets the scale tend to zero.

theorem CIV.hausdorffMeasure_one_null_of_gradient_density : ∀ (x : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (S : Set CKN.Foundation.Parabolic.Vec3) (ε : ℝ) (hε : 0 < ε) (hfin : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in unitCylinder, ‖Du z‖ₑ ^ 2 < ⊤) (hdens : ∀ x ∈ S, ∀ (r₀ : ℝ), 0 < r₀ → ∃ (r : ℝ), 0 < r ∧ r < r₀ ∧ ENNReal.ofReal (ε * r) ≤ ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioo (-r ^ 2) 0, ‖Du z‖ₑ ^ 2), (MeasureTheory.Measure.hausdorffMeasure 1) (S ∩ CKN.Foundation.Parabolic.vec3Ball 0 1) = 0

Spatial Vitali covering lemma (the spatial analogue of CKN's step:thmC-covering). If S ⊆ Vec3 carries, at every point x ∈ S and every scale r₀ > 0, a radius r < r₀ with ε r ≤ ∫_{B(x,r) × (-r²,0)} |∇u|² (the same integrand and measure lintegral_gradSq_lt_top produces: ‖Du z‖ₑ ^ (2:ℝ) over the plain product-space volume measure, restricted to the stated set), and the total ∫_{Q} |∇u|² over the unit cylinder is finite, then S ∩ B(1) has one-dimensional Hausdorff measure zero.

The proof fixes a scale δ n = 1/(n+1) → 0, extracts at each n a disjoint (Vitali) family of cylinders B(x_i, r_i) × (-r_i², 0), r_i < δ n, from the density hypothesis, and covers S ∩ B(1) by the 5-enlarged spatial balls B(x_i, 5 r_i). The cylinders are disjoint, so the lower bounds ε r_i sum to at most the (shrinking) integral over B(1) × (-δ n, 0), which tendsto_lintegral_top_slab sends to 0; since each enlarged ball has sup-norm extended diameter at most 10 r_i, the Hausdorff premeasure of the cover tends to 0 as well.

From a strict limsup lower density to the covering lemma's density hypothesis

theorem CIV.density_of_le_limsup {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} {ε₁ : ℝ} (hε₁ : 0 < ε₁) (h : ENNReal.ofReal ε₁ ≤ Filter.limsup (fun (r : ℝ) => (ENNReal.ofReal r)⁻¹ * ∫⁻ (w : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioo (-r ^ 2) 0, ENNReal.ofReal (CKN.spatialGradientSq u Du w)) (nhdsWithin 0 (Set.Ioi 0))) (r₀ : ℝ) (hr₀ : 0 < r₀) : ∃ (r : ℝ), 0 < r ∧ r < r₀ ∧ ENNReal.ofReal (ε₁ / 18 * r) ≤ ∫⁻ (w : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x r ×ˢ Set.Ioo (-r ^ 2) 0, ‖Du w‖ₑ ^ 2

The bridge from a strict-limsup gradient density to hausdorffMeasure_one_null_of_gradient_density's hdens hypothesis. If ofReal ε₁ is at most the limsup, as the radius shrinks to 0 from the right, of (ofReal r)⁻¹ times the Dirichlet integral of spatialGradientSq u Du over the backward parabolic cylinder B(x,r) × (-r², 0), then at every scale r₀ > 0 there is a smaller radius r < r₀ with ofReal (ε₁/18 * r) ≤ ∫ ‖Du‖ₑ² over that same cylinder — exactly the form hausdorffMeasure_one_null_of_gradient_density consumes, at ε := ε₁ / 18. The constant loses a factor of 2 because a strict limsup bound only gives, at every neighbourhood of 0, a point where the halved level ε₁/2 is exceeded (not ε₁ itself), and a further factor of 9 bridging spatialGradientSq to the enorm-squared integrand of hausdorffMeasure_one_null_of_gradient_density (ofReal_spatialGradientSq_le_nine), so only ε₁/(2·9) = ε₁/18 survives.