Compact support in the Carleman cylinder

The scalar cutoff support lies strictly inside the half-space and strictly between the shifted initial and final times.

theorem ESS.bu_short_cutoff_support_geometry (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) : IsCompact (buCutSupportSet (buShortFullCutoff scale R hR ε)) ∧ buCutSupportSet (buShortFullCutoff scale R hR ε) ⊆ halfSpaceDomain ∧ buCutSupportSet (buShortFullCutoff scale R hR ε) ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) 1)

The parabolic support of the short-time scalar cutoff is compact and lies inside the half-space Carleman cylinder.