Direct rescaling of the Gaussian target box

The weighted target box yields the unweighted Gaussian estimate after parabolic change of variables.

theorem ESS.uc_gaussian_target_box_direct_rescaling (x₀ x : CKN.Foundation.Parabolic.Vec3) (R T t ρ scale a C₀ : ℝ) (ht : 0 < t) (hscale : scale = √(2 * t)) (hρ : 4 ≤ ρ) (hC₀ : 0 < C₀) (hρdef : ρ = 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm ((√(2 / 100))⁻¹ • (x - x₀)) / scale) (ha : a = 1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2)))) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hsourceInt : 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) (hboxInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale⁻¹ • (x - x₀)) 1) (Set.Ioo (1 / 2) 1)) MeasureTheory.volume) (hweightedInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2 + CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z)) (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale⁻¹ • (x - x₀)) 1) (Set.Ioo (1 / 2) 1)) MeasureTheory.volume) (hweighted : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale⁻¹ • (x - x₀)) 1) (Set.Ioo (1 / 2) 1), ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2 + CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z) ≤ C₀ * Real.exp (-ρ ^ 2 / 100) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2 + CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z) (henergy : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2 + CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z ≤ 2 * scale.rpow (-5) * ucLocalEnergy x₀ R T w Dw) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x √(2 * t)) (Set.Ioo t (2 * t)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 ≤ 2 * Real.exp 1 * C₀ * ucLocalEnergy x₀ R T w Dw * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ^ 2 / (2 * t))

Rescaling the target-box weighted estimate gives the Gaussian box estimate in lem:uc-gaussian, with the absolute factor from the weight lower bound kept explicit.