Finite time-slab rescaling for large Gaussian growth #
Equal short slabs give a finite covering of every time below one while keeping the rescaled growth exponent below the small-growth threshold.
theorem
ESS.bu_large_growth_from_small
(c₁ M : ℝ)
(hc₁ : 0 < c₁)
(hM : 1 / 10 ^ 12 < M)
(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))
(hinit : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0)
(hderiv : 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 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)))
(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))
(hsmall :
∀ (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),
ContinuousOn v ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) →
(∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → v (x, 0) = 0) →
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) v Dv D2v Dtv →
(∀ 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, ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv 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 fun (i : Fin 3) => Dtv z i + ∑ j : Fin 3, D2v z i j j) ≤ c₁ * (√(CKN.spatialGradientSq v Dv z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (v z))) →
(∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ≤ Real.exp (1 / 10 ^ 12 / 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) →
∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → ∀ (s : ℝ), 0 < s → s < 1 → v (x, s) = 0)
(x : CKN.Foundation.Parabolic.Vec3)
:
The large-growth case follows by a finite number of rescaled small-growth applications.