Restriction of integral flatness

Integral vanishing of every order persists when the allowed spatial radius or time length is shortened in lem:uc-gaussian.

theorem ESS.uc_integral_flatness_mono (x₀ : CKN.Foundation.Parabolic.Vec3) (R R' T T' : ℝ) (hR : R' ≤ R) (hT : T' ≤ T) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hflat : UCIntegralFlatness x₀ R T w) : UCIntegralFlatness x₀ R' T' w

Integral flatness at a center remains valid on a smaller admissible cylinder (thm:uc).