Compact support of the short-time cutoff #
For fixed spatial radius and lower-time parameter, the smooth cutoff stays inside a compact subset of the shifted half-space Carleman domain.
theorem
ESS.buShortFullCutoff_compact_support
{scale R ε : ℝ}
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hR : 0 < R)
(hε : 0 < ε)
:
HasCompactSupport (buShortFullCutoff scale R hR ε) ∧ tsupport (buShortFullCutoff scale R hR ε) ⊆ {y : CKN.Foundation.Parabolic.Vec3 | 1 < y 2} ×ˢ Set.Ioo (1 / 2) 1
The scalar cutoff is supported in a compact spatial ball, above the normal transition height, and below a time level strictly smaller than one.