Local trace integrability from quadratic growth

The quadratic growth bound makes the rescaled field square integrable on each bounded strip used in the initial-time cutoff estimate.

theorem ESS.bu_short_shifted_trace_integrable (M scale R ε : ℝ) (hM : 0 < M) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (hεsmall : ε < 1 / 4) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) (hgrowth : ∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField (-scale ^ 2 / 2) scale w z) ^ 2) (CKN.spaceTimeSet (buShortTraceBall R) (Set.Icc (1 / 2 + ε) (1 / 2 + 2 * ε))) MeasureTheory.volume

The shifted rescaling has integrable quadratic mass on a bounded closed early-time strip.