Integral flatness under parabolic scaling

The all-orders integral condition in lem:uc-gaussian is invariant under a fixed positive parabolic dilation.

theorem ESS.uc_integral_flatness_scaled (x₀ : CKN.Foundation.Parabolic.Vec3) (R T scale ρ : ℝ) (hR : 0 < R) (hT : 0 < T) (hscale : 0 < scale) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hwloc : MeasureTheory.LocallyIntegrableOn w (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T)) MeasureTheory.volume) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 < ⊤) (hflat : UCIntegralFlatness x₀ R T w) : UCIntegralFlatness 0 ρ 2 (ucScaledField x₀ scale w)

Parabolic dilation preserves integral vanishing of every order at the initial point (eq:uc-integral-vanishing).