Blowup Gradient Rescale

Gradient estimates for the rescaled sequence used in endpoint compactness.

theorem ESS.blowupRescale_eventually_gradient_bound_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, ∀ b < 0, 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ (r k) u) (parabolicRescaleGradient x₀ t₀ (r k) Du) z ≤ C

Fixed local velocity and pressure norms give a scale-uniform gradient bound on each compactly contained past cylinder of the rescaled solution.