Derivative energy on affine time intervals

The three quadratic derivative terms used in lem:bu-small-time remain finite on bounded subsets after the translated parabolic change of variables.

theorem ESS.bu_affine_derivative_l2_interval (τ scale a b : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (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) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) : K ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b) → Bornology.IsBounded K → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, ‖buAffineDw τ scale Dw z‖ₑ ^ 2 + ‖buAffineD2w τ scale D2w z‖ₑ ^ 2 + ‖buAffineDtw τ scale Dtw z‖ₑ ^ 2 < ⊤

The three quadratic weak-derivative terms remain finite on bounded subsets after a subunit affine parabolic change of variables.