Blowup Velocity Uniform

Velocity estimates for the rescaled sequence used in endpoint compactness.

theorem ESS.blowupRescaledVelocity_eventually_bounded_pastBox (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (M : ENNReal) (hM : M < ⊤) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, s))) 3 MeasureTheory.volume ≤ M) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) : ∃ B < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ (r k) u z)) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ B

A uniform source velocity slice bound gives a uniform local space-time L³ bound for every sufficiently small positive Navier–Stokes rescaling.