Flatness on the initial transition near the center

Integral flatness of every order bounds the mass in a fourth-root spatial ball during the initial cutoff transition.

theorem ESS.uc_initial_near_mass_le (ρ : ℝ) (hρ : 4 ≤ ρ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (ucCylinder ρ) MeasureTheory.volume) (hflat : UCIntegralFlatness 0 ρ 2 v) (N : ℕ) : ∃ (C : ℝ) (δ : ℝ), 0 < C ∧ 0 < δ ∧ ∀ (ε : ℝ), 0 < ε → ε < δ → have r := √√ε; ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Icc ε (2 * ε)), CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ C * ε ^ N

Every integral flatness order yields an arbitrarily high power of the initial transition length on a shrinking spatial ball.