Short-time densities from Gaussian averages

The Gaussian estimate for the physical field controls the three weighted densities of its short-time affine rescaling.

theorem ESS.bu_short_densities_from_gaussian (M scale γ C c₁ a : ℝ) (hMmax : M ≤ 1 / 10 ^ 12) (hMbar : 1 / 10 ^ 12 / 2 ≤ M) (hscale : 0 < scale) (hscaleγ : scale ^ 2 ≤ γ) (hγsmall : γ < 1 / 12) (hC : 0 < C) (hc₁ : 0 < c₁) (ha : 0 ≤ a) (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 ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z))) (hgrowth : ∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) (hGaussian : ∀ (X : CKN.Foundation.Parabolic.Vec3), 2 < X 2 → ∀ (t : ℝ), 0 < t → t < γ → t.rpow (-(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 M (1 / 10 ^ 12 / 2) * CKN.Foundation.Parabolic.vec3EuclideanNorm X ^ 2) * Real.exp (-(1 / 10 ^ 6 * X 2 ^ 2 / (12 * t)))) : MeasureTheory.IntegrableOn (buShortTangentialDensity scale w Dw) (buShortHighStrip scale) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (buShortWeightedPolynomialDensity scale a w Dw) (buShortHighStrip scale) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (buShortWeightedDensity scale a w Dw) (buShortHighStrip scale) MeasureTheory.volume

The physical Gaussian average estimate makes the tangential and two fixed Carleman densities integrable above the lower normal cutoff (lem:bu-small-time).