Gaussian mass outside the transition radius

The rescaled growth condition and Gaussian weight bound the radial mass that appears on the transition shell in lem:bu-gaussian.

theorem ESS.buGaussian_radial_mass_tail_bound {ρ a A barA scale : ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hρ : 4 < ρ) (ha : a = buGaussianBeta * ρ ^ 2 / buGaussianH) (hA : 0 ≤ A) (hA0 : A ≤ 1 / 10 ^ 12) (hAbar : A ≤ barA) (hscale : scale ^ 2 ≤ 1 / 4) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) (hgrowth : ∀ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ≤ Real.exp (2 * A * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2 + 2 * A * scale ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), buGaussianRadialWeightedMass ρ a v z ≤ 24 * ρ ^ 3 * Real.exp (8 * barA * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2) * Real.exp (-2 * buGaussianBeta * ρ ^ 2)

The radial weighted mass is bounded by its Gaussian tail times the volume of the localization cylinder (eq:bu-gaussian-collar).