Blowup Gradient Local

Gradient estimates for the rescaled sequence used in endpoint compactness.

theorem ESS.blowupGradient_eventually_bounded_all_upper_times (R a : ℝ) (hR : 0 < R) (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 → ℝ) (Bᵤ Bₚ : ENNReal) (hBᵤ : Bᵤ < ⊤) (hBₚ : Bₚ < ⊤) (hsuitable : ∀ᶠ (k : ℕ) in Filter.atTop, CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) 3 (u k) (Du k) (p k) 0) (hu : ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u k z)) 3 (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u k z)) 3 (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) ≤ Bᵤ) (hp : ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.MemLp (p k) (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) ∧ MeasureTheory.eLpNorm (p k) (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) ≤ Bₚ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (k : ℕ) in Filter.atTop, ∀ b < 0, 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq (u k) (Du k) z ≤ C

The same tail and numerical bound work for every upper endpoint below time zero.