Weak derivatives on affine time intervals

The weak spatial and time derivatives transport between corresponding half-space time intervals in lem:bu-small-time.

theorem ESS.bu_affine_weak_derivatives_interval (τ scale a b : ℝ) (hscale : 0 < scale) (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 (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)) w Dw D2w Dtw) : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b) (buAffineField τ scale w) (buAffineDw τ scale Dw) (buAffineD2w τ scale D2w) (buAffineDtw τ scale Dtw)

Weak derivatives transport through an affine parabolic change of variables between corresponding positive half-space time intervals.