Admissibility of the short-time cutoff #
The smooth spatial and temporal cutoff of lem:bu-small-time supplies the
weak derivative and quadratic energy assumptions of the half-space estimate.
theorem
ESS.bu_short_cutoff_carleman_admissible
(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) ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), ‖W z‖ₑ ^ 2 + ‖DW z‖ₑ ^ 2 + ‖D2W z‖ₑ ^ 2 + ‖DtW z‖ₑ ^ 2 < ⊤
The short-time cutoff has precisely the weak data, support, and finite quadratic energy required for the half-space Sobolev Carleman inequality.