Weighted Gaussian target box

Absorption, collar decay, and the vanishing initial time error yield a weighted estimate directly on the positive-time target box.

theorem ESS.uc_gaussian_weighted_target_box (c₁ : ℝ) (hc₁ : 0 ≤ c₁) : ∃ (c₀ : ℝ) (C₀ : ℝ), 0 < c₀ ∧ 0 < C₀ ∧ ∀ (ρ scale : ℝ), 4 ≤ ρ → 0 ≤ scale → scale ≤ 1 → c₀ * 54 * (c₁ * scale) ^ 2 ≤ 1 / 40 → ∀ (center : CKN.Foundation.Parabolic.Vec3), CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1) ⊆ ucInnerRegion ρ → ∀ (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dv D2v Dtv → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤ → (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) → UCIntegralFlatness 0 ρ 2 v → have a := 1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2))); ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1), ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z) ≤ C₀ * Real.exp (-ρ ^ 2 / 100) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z

A fixed Gaussian constant gives a uniform weighted target-box bound for every sufficiently small normalized lower order scale.