Initial trace from a Gaussian box estimate

The exponential box estimate in lem:uc-gaussian gives a zero trace at every output point away from its center.

theorem ESS.uc_gaussian_box_bound_to_trace (R T : ℝ) (hT : 0 < T) (x₀ x : CKN.Foundation.Parabolic.Vec3) (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ico 0 T))) (hwloc : MeasureTheory.LocallyIntegrableOn w (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T)) MeasureTheory.volume) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 < ⊤) (b A γ : ℝ) (hb : 0 < b) (hγ : 0 < γ) (hbox : ∀ (t : ℝ), 0 < t → t < γ → ∫ (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 ≤ A * Real.exp (-(b / t))) : w (x, 0) = 0

A positive Gaussian exponent in the shrinking-box estimate forces a zero boundary value (thm:uc).