Local quadratic energy after the final time change

The velocity and all specified weak derivatives retain finite quadratic energy on bounded subcylinders after the affine change of variables.

theorem ESS.bu_short_uc_affine_l2 (τ 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, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) (hK : K ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b)) (hKb : Bornology.IsBounded K) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, ‖buAffineField τ scale w z‖ₑ ^ 2 + ‖buAffineDw τ scale Dw z‖ₑ ^ 2 + ‖buAffineD2w τ scale D2w z‖ₑ ^ 2 + ‖buAffineDtw τ scale Dtw z‖ₑ ^ 2 < ⊤

Full local quadratic weak-derivative data transfers through an affine parabolic change of variables on the translated time interval.