Gaussian propagation from integral flatness

The normalized Carleman estimate and parabolic rescaling yield the positive-time Gaussian box estimate.

theorem ESS.uc_gaussian_box_estimate (R T c₁ : ℝ) (hR : 0 < R) (hT : 0 < T) (hT1 : T ≤ 1) (hc₁ : 0 < c₁) (x₀ : CKN.Foundation.Parabolic.Vec3) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hcont : ContinuousOn w (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ico 0 T)) (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T) w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))) (hflat : UCIntegralFlatness x₀ R T w) : ∃ (γ : ℝ) (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))

Integral vanishing at a center yields Gaussian decay on nearby positive-time boxes (lem:uc-gaussian).