Weak data on the cutoff plateau

On the open plateau, the cutoff field and its specified weak derivatives agree with the shifted source field.

theorem ESS.bu_short_cutoff_data_eq_on_core (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortCoreRegion scale R ε) : buCutField (buShortFullCutoff scale R hR ε) v z = v z ∧ buCutDw (buShortFullCutoff scale R hR ε) v Dv z = Dv z ∧ buCutD2 (buShortFullCutoff scale R hR ε) v Dv D2v z = D2v z ∧ buCutDt (buShortFullCutoff scale R hR ε) v Dtv z = Dtv z

The complete cutoff weak data agree with the shifted field on the open plateau of lem:bu-small-time.