Trace cylinder containing the compact cutoff

The spatial support of the cutoff lies strictly inside the ball used in the initial-time trace estimate.

theorem ESS.buShortCutSupport_subset_traceCylinder (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) : buCutSupportSet (buShortFullCutoff scale R hR ε) ⊆ CKN.spaceTimeSet (buShortTraceBall R) (Set.Ioo (1 / 2) 1)

The compact cutoff support lies in the open trace ball and shifted time interval.