Flatness from a zero parabolic neighborhood

This is the elementary flatness estimate used in lem:flat-from-vanishing.

theorem ESS.flat_from_vanishing (R' T' r₀ M : ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hr₀ : 0 < r₀) (hM : 0 ≤ M) (hr₀R' : r₀ ≤ R') (hr₀T' : r₀ ^ 2 ≤ T') (hbound : ∀ z ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R' ×ˢ Set.Ico 0 T', CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ M) (hzero : ∀ (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ), x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ r₀ → 0 < s → s < r₀ ^ 2 → (x, s) ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R' ×ˢ Set.Ico 0 T' → w (x, s) = 0) (k : ℕ) (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : (x, s) ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R' ×ˢ Set.Ioo 0 T' → CKN.Foundation.Parabolic.vec3EuclideanNorm (w (x, s)) ≤ M * r₀⁻¹ ^ k * (CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) + √s) ^ k

A bounded field that vanishes on a past neighborhood of its top point has the corresponding pointwise flatness bounds.