From pointwise to integral flatness

The all-orders pointwise hypothesis in thm:uc implies the local integral condition used by lem:uc-gaussian.

theorem ESS.uc_pointwise_to_integral_flatness (R T : ℝ) (hT : 0 < T) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hvanish : ∀ (k : ℕ), ∃ (C : ℝ), ∀ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 T), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ C * (CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 + √z.2) ^ k) : UCIntegralFlatness 0 R (min T 1) w

Pointwise vanishing of every order implies the integral vanishing condition at the origin.