Uniform short-time interval

The fixed Carleman constants and Gaussian threshold yield one time interval valid for every field with the prescribed growth rate.

theorem ESS.bu_short_uniform_from_density_provider (c₁ γ : ℝ) (hc₁ : 0 < c₁) (hγ : 0 < γ) (hγsmall : γ < 1 / 12) (hDensity : ∀ (M scale : ℝ), 0 < M → M ≤ 1 / 10 ^ 12 → 1 / 10 ^ 12 / 2 ≤ M → 0 < scale → scale ^ 2 ≤ γ → ∀ (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 ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) → (∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) → CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw → (∀ 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 < ⊤) → (∀ᵐ (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))) → (∀ 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)) → MeasureTheory.IntegrableOn (buShortTangentialDensity scale w Dw) (buShortWideGapRegion scale) MeasureTheory.volume ∧ ∀ (a : ℝ), 0 ≤ a → MeasureTheory.IntegrableOn (buShortWeightedPolynomialDensity scale a w Dw) (buShortHighStrip scale) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (buShortWeightedDensity scale a w Dw) (buShortHighStrip scale) MeasureTheory.volume) : ∃ (γ₁ : ℝ), 0 < γ₁ ∧ γ₁ ≤ γ / 2 ∧ ∀ (A : ℝ), 0 ≤ A → A ≤ 1 / 10 ^ 12 → ∀ (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 ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) → (∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) → CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw → (∀ 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 < ⊤) → (∀ᵐ (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))) → (∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (A * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) → ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → ∀ (t : ℝ), 0 < t → t < γ₁ → w (x, t) = 0

Uniform short-time vanishing follows when the three Gaussian energy densities are integrable below the Gaussian time threshold (lem:bu-small-time).