Support of the short-time cutoff field

The compact scalar cutoff gives compact support to the vector field and keeps its topological support inside the half-space Carleman cylinder.

theorem ESS.bu_short_cutoff_field_support {scale R ε : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : HasCompactSupport (buCutField (buShortFullCutoff scale R hR ε) v) ∧ tsupport (buCutField (buShortFullCutoff scale R hR ε) v) ⊆ CKN.spaceTimeSet {y : CKN.Foundation.Parabolic.Vec3 | 1 < y 2} (Set.Ioo 0 1)

Pulling back a compact scalar cutoff through the parabolic coordinate homeomorphism preserves its compact support and spatial-time support bound.