A fixed cylinder for the lower-time limit

For fixed spatial radius all lower-time cutoff supports lie in one compact cylinder. This keeps the spatial-phase derivative bounds independent of the lower-time transition width.

def ESS.buShortFixedCylinder (R : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

Compact cylinder containing all supports at a fixed spatial radius.

Equations

• ESS.buShortFixedCylinder R = ⇑CKN.Foundation.Parabolic.parabolicHomeomorph ⁻¹' (CKN.euclideanClosedBall 0 (2 * R) ∩ {x : CKN.Foundation.Parabolic.Vec3 | 1 ≤ x 2}) ×ˢ Set.Icc (1 / 2) 1

theorem ESS.buShortFixedCylinder_isCompact {R : ℝ} (hR : 0 < R) : IsCompact (buShortFixedCylinder R)

The fixed cylinder is compact for positive radius.

theorem ESS.buShortCutSupport_subset_fixedCylinder (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) : buCutSupportSet (buShortFullCutoff scale R hR ε) ⊆ buShortFixedCylinder R

Every compact cutoff support at radius R lies in the same closed spatial ball and time interval, independently of ε.