Blowup Gradient Top #
Gradient estimates for the rescaled sequence used in endpoint compactness.
theorem
ESS.blowup_nonnegative_integral_bound_to_time_zero
(A : Set CKN.Foundation.Parabolic.Vec3)
(hA : MeasurableSet A)
(a C : ℝ)
(f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hf : ∀ b < 0, MeasureTheory.IntegrableOn f (A ×ˢ Set.Ioo a b) MeasureTheory.volume)
(hnonneg : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ f z)
(hbound : ∀ b < 0, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in A ×ˢ Set.Ioo a b, f z ≤ C)
:
MeasureTheory.IntegrableOn f (A ×ˢ Set.Ioo a 0) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in A ×ˢ Set.Ioo a 0, f z ≤ C
Uniform bounds on past subcylinders extend to the open terminal time.
theorem
ESS.blowupGradient_integrableOn_inner_pastBox
(R a b : ℝ)
(hR : 0 < R)
(hb : b < 0)
{q : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hsol : CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0)
:
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq u Du z)
(CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b)) MeasureTheory.volume
The suitable energy on a finite past cylinder is integrable on each smaller cylinder whose upper time is negative.
theorem
ESS.blowupGradient_bound_to_time_zero
(R a C : ℝ)
(hR : 0 < R)
{q : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hsol : CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0)
(hbound :
∀ b < 0,
2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq u Du z ≤ C)
:
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq u Du z)
(CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0)) MeasureTheory.volume ∧ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0), CKN.spatialGradientSq u Du z ≤ C
A uniform energy estimate below time zero includes the full open past cylinder up to time zero.
theorem
ESS.blowupRescale_eventually_gradient_bound_to_time_zero_of_local_norms
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hSuitable : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ : ℝ)
(r : ℕ → ℝ)
(hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2)))
(ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0)
(hr : ∀ (k : ℕ), 0 < r k)
(hr0 : Filter.Tendsto r Filter.atTop (nhds 0))
(R a : ℝ)
(hR : 0 < R)
(ha : a < 0)
(hvel :
∃ Bᵤ < ⊤,
∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupVelocity x₀ t₀ (r k) u z))
3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (R + 1) ×ˢ Set.Ioo (a - 2) 0)) ≤ Bᵤ)
(hpress :
∃ Bₚ < ⊤,
∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (blowupPressure x₀ t₀ (r k) p) (3 / 2)
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (R + 1) ×ˢ Set.Ioo (a - 2) 0)) ≤ Bₚ)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) z)
(CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0)) MeasureTheory.volume ∧ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a 0), CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du)
z ≤ C
The same scale tail controls the gradient energy on the full open past cylinder up to time zero.