Quadratic weak-derivative data under scaling

The parabolic dilation used in lem:uc-gaussian preserves finite quadratic energy on the normalized cylinder.

theorem ESS.uc_scaled_l2_data (x₀ : CKN.Foundation.Parabolic.Vec3) (R T scale ρ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hball : scale * ρ ≤ R) (htime : 2 * scale ^ 2 ≤ T) (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 (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T) w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖ucScaledField x₀ scale w z‖ₑ ^ 2 + ‖ucScaledDw x₀ scale Dw z‖ₑ ^ 2 + ‖ucScaledD2w x₀ scale D2w z‖ₑ ^ 2 + ‖ucScaledDtw x₀ scale Dtw z‖ₑ ^ 2 < ⊤

Finite quadratic weak-derivative data transfers to the normalized Gaussian cylinder.