Weighted mass on the initial time transition

A bounded Gaussian weight turns unweighted integral flatness and finite quadratic mass into bounds for the initial cutoff error.

theorem ESS.uc_initial_weighted_transition_bound (ρ : ℝ) (hρ : 4 ≤ ρ) (a : ℝ) (ha : 0 ≤ a) (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 := √√ε; have B := (ε * Real.exp (-(1 / 3))) ^ (-2 * a); ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Icc ε (2 * ε)), ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ B * (C * ε ^ N + Real.exp (-(r ^ 2 / (8 * ε))) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2)

The weighted mass during the initial cutoff transition has a polynomially flat near part and an exponentially suppressed far part.