Containment of parabolic cylinders inside the unit cylinder

The two theorems below establish that a parabolic cylinder based at (x, s) with s < 0 and radius r satisfying r ≤ r' and r² - s ≤ r'² is contained in the r'-thickened unit cylinder vec3Ball x r' ×ˢ (-r'², 0). The second theorem replaces the cylinder by its closure and uses the unit cylinder itself, the natural ambient set for the interior partial-regularity estimates of arXiv:2609.20803.

theorem CIV.parabolicCylinder_subset_topCylinder {x : CKN.Foundation.Parabolic.Vec3} {s r r' : ℝ} (hs : s < 0) (hrr' : r ≤ r') (hsq : r ^ 2 - s ≤ r' ^ 2) : CKN.Foundation.Parabolic.parabolicCylinder x s r ⊆ CKN.Foundation.Parabolic.vec3Ball x r' ×ˢ Set.Ioo (-r' ^ 2) 0

A parabolic cylinder based at (x, s) with s < 0 and radius r is contained in vec3Ball x r' ×ˢ (-r'², 0) whenever r ≤ r' and r² - s ≤ r'².

theorem CIV.closure_parabolicCylinder_subset_unitCylinder (x : CKN.Foundation.Parabolic.Vec3) (s r : ℝ) (hr : 0 < r) (hs : s < 0) (hlow : -1 < s - r ^ 2) (hball : ∀ (y : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ r → CKN.Foundation.Parabolic.vec3EuclideanNorm (y - 0) < 1) : closure (CKN.Foundation.Parabolic.parabolicCylinder x s r) ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)

The closure of a parabolic cylinder based at (x, s) with s < 0 is contained in the unit cylinder spaceTimeSet (vec3Ball 0 1) (Ioo (-1) 0) provided the cylinder itself is already trapped inside the unit ball in the spatial direction and its lower time boundary is above -1.