Weak data on the full half-space cylinder

The short-time cutoff field extends across its artificial lower time face while retaining compact support and global quadratic derivative data.

theorem ESS.bu_short_cutoff_carleman_data (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : have κ := buShortFullCutoff scale R hR ε; have v := buAffineField (-scale ^ 2 / 2) scale w; have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw; have D2v := buAffineD2w (-scale ^ 2 / 2) scale D2w; have Dtv := buAffineDtw (-scale ^ 2 / 2) scale Dtw; have W := buCutField κ v; have DW := buCutDw κ v Dv; have D2W := buCutD2 κ v Dv D2v; have DtW := buCutDt κ v Dtv; CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1) W DW D2W DtW ∧ HasCompactSupport W ∧ tsupport W ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1) ∧ MeasureTheory.MemLp W 2 MeasureTheory.volume ∧ MeasureTheory.MemLp DW 2 MeasureTheory.volume ∧ MeasureTheory.MemLp D2W 2 MeasureTheory.volume ∧ MeasureTheory.MemLp DtW 2 MeasureTheory.volume

The cutoff field has weak derivative data on the full half-space Carleman cylinder, with compact support and global L² bounds.