Integrability on the Gaussian target box

The Gaussian weight is integrable on the positive-time box because the initial cutoff has already reached its plateau there.

theorem ESS.uc_target_box_weighted_integrable {ρ a : ℝ} (hρ : 4 ≤ ρ) (ha : 0 ≤ a) (center : CKN.Foundation.Parabolic.Vec3) (hbox : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1) ⊆ ucInnerRegion ρ) {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 0 2) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z)) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1)) MeasureTheory.volume

Weighted energy of the original field is integrable on a target box inside the Gaussian cutoff plateau.