Transfer of integral flatness to a nearby center

The Gaussian estimate, a finite spatial cover, and overlapping time slabs propagate infinite-order integral vanishing within its spatial reach.

theorem ESS.uc_move_center_integral_flatness (x₀ y₀ : CKN.Foundation.Parabolic.Vec3) (R T : ℝ) (hR : 0 < R) (hT : 0 < T) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → 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₀ R) (Set.Ioo 0 T)) MeasureTheory.volume) (hflat : UCIntegralFlatness x₀ R T w) (hgauss : ∃ (γ : ℝ) (C : ℝ), 0 < γ ∧ γ < 3 / 16 ∧ 0 < C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → t ≤ γ * T → CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ ucRadiusFraction * R → 16 / 100 * t ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ^ 2 → ∫ (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 ≤ C * ucLocalEnergy x₀ R T w Dw * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ^ 2 / (2 * t))) (hy : y₀ ∈ CKN.Foundation.Parabolic.vec3Ball x₀ (ucRadiusFraction * R)) : UCIntegralFlatness y₀ R T w

Gaussian box decay moves integral flatness from one center to every center in its inner output ball (thm:uc).