The Gaussian average estimate for backward uniqueness

The cutoff equals the translated field on the normalized averaging box in lem:bu-gaussian.

theorem ESS.bu_gaussian_average_uniform (c₁ : ℝ) (hc₁ : 0 < c₁) : ∃ (γ : ℝ), 0 < γ ∧ γ < 1 / 12 ∧ ∀ (A : ℝ), 0 ≤ A → A ≤ 1 / 10 ^ 12 → ∃ (C : ℝ), 0 < C ∧ ∀ (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), ContinuousOn w (buHalfSpace ×ˢ Set.Ico 0 1) → (∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) → CKN.HasSpaceTimeWeakDerivs buHalfSpace (Set.Ioo 0 1) w Dw D2w Dtw → (∀ S ⊆ buHalfCylinder, Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) → (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict buHalfCylinder, (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z))) → (∀ z ∈ buHalfCylinder, CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (A * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) → ∀ (x : CKN.Foundation.Parabolic.Vec3), 2 < x 2 → ∀ (t : ℝ), 0 < t → t < γ → t ^ (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball x √(3 * t)) (Set.Ioo t (5 * t / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 ≤ C * Real.exp (8 * max A (1 / 10 ^ 12 / 2) * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2) * Real.exp (-(1 / 10 ^ 6 * x 2 ^ 2) / (12 * t))

Gaussian decay of the normalized space-time averages in lem:bu-gaussian.