Returning the Gaussian target box to the source variables

The target box under parabolic dilation is the box appearing in eq:uc-gaussian-box.

theorem ESS.uc_target_box_preimage (x₀ x : CKN.Foundation.Parabolic.Vec3) (scale t : ℝ) (hscale : 0 < scale) (hscaleSq : scale ^ 2 = 2 * t) : CKN.spaceTimeSet (CKN.rescaledSpace scale x₀ (CKN.Foundation.Parabolic.vec3Ball x scale)) (CKN.rescaledTime scale 0 (Set.Ioo t (2 * t))) = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale⁻¹ • (x - x₀)) 1) (Set.Ioo (1 / 2) 1)

The normalized target box is the inverse image of the source box under the Gaussian parabolic dilation (lem:uc-gaussian).

theorem ESS.uc_target_box_integral_scaling (x₀ x : CKN.Foundation.Parabolic.Vec3) (scale t : ℝ) (hscale : 0 < scale) (hscaleSq : scale ^ 2 = 2 * t) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x scale) (Set.Ioo t (2 * t))) MeasureTheory.volume) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale⁻¹ • (x - x₀)) 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2 = scale.rpow (-5) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x scale) (Set.Ioo t (2 * t)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2

Parabolic change of variables for the target-box integral in eq:uc-gaussian-box.