Gaussian target-box comparison

The positive-time target box permits direct comparison of weighted and unweighted integrals.

theorem ESS.uc_target_box_le_weighted_box (a : ℝ) (ha : 0 ≤ a) (center : CKN.Foundation.Parabolic.Vec3) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hboxInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1)) MeasureTheory.volume) (hweightedInt : 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) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ Real.exp (CKN.Foundation.Parabolic.vec3EuclideanNorm center ^ 2 + 1) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1), ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z)

The Gaussian weight on a positive-time target box controls its unweighted mass.