Returning from the Gaussian rescaling

The normalized space-time box maps onto the physical averaging box in lem:bu-gaussian with parabolic Jacobian scale⁻⁵.

def ESS.buGaussianAverageScaledField (x : CKN.Foundation.Parabolic.Vec3) (scale σ : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The original field expressed in the translated Gaussian coordinates.

Equations

• ESS.buGaussianAverageScaledField x scale σ w z = w (ESS.buGaussianScaledPoint x scale σ z)

theorem ESS.buGaussian_change_back_integral (x : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (hscale : 0 < scale) (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 (scale ^ 2 / 3) (5 * scale ^ 2 / 6))) MeasureTheory.volume) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianAverageScaledField x scale (1 / 6) w z) ^ 2 = (scale ^ 5)⁻¹ * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x scale) (Set.Ioo (scale ^ 2 / 3) (5 * scale ^ 2 / 6)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2

The normalized Gaussian box integral changes variables to its physical space-time average (lem:bu-gaussian#change-back).

theorem ESS.buGaussian_change_back_factor {t : ℝ} (ht : 0 < t) : t.rpow (-(5 / 2)) * √(3 * t) ^ 5 = Real.rpow 3 (5 / 2)

The averaging normalization and the parabolic Jacobian combine to the absolute factor 3^(5/2) in lem:bu-gaussian#change-back.

theorem ESS.buGaussian_change_back_average (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (ht : 0 < 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 √(3 * t)) (Set.Ioo t (5 * t / 2))) MeasureTheory.volume) : t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(3 * t)) (Set.Ioo t (5 * t / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 = Real.rpow 3 (5 / 2) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianAverageScaledField x (√(3 * t)) (1 / 6) w z) ^ 2

The source average is the normalized Gaussian box integral times 3^(5/2) (lem:bu-gaussian#change-back).