Weak derivatives of the short-time cutoff field #
The product field formed from the shifted solution and the smooth compact cutoff has the exact weak derivative data required by the half-space estimate.
theorem
ESS.bu_short_cutoff_weak_derivatives
(scale R ε : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hR : 0 < R)
(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)
(hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw)
:
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) 1)
(buCutField (buShortFullCutoff scale R hR ε) (buAffineField (-scale ^ 2 / 2) scale w))
(buCutDw (buShortFullCutoff scale R hR ε) (buAffineField (-scale ^ 2 / 2) scale w)
(buAffineDw (-scale ^ 2 / 2) scale Dw))
(buCutD2 (buShortFullCutoff scale R hR ε) (buAffineField (-scale ^ 2 / 2) scale w)
(buAffineDw (-scale ^ 2 / 2) scale Dw) (buAffineD2w (-scale ^ 2 / 2) scale D2w))
(buCutDt (buShortFullCutoff scale R hR ε) (buAffineField (-scale ^ 2 / 2) scale w)
(buAffineDtw (-scale ^ 2 / 2) scale Dtw))
The short-time cut-off field has the expected weak spatial and time derivatives on the shifted positive half-space cylinder.