Blowup Energy Lp Bound

Local energy bounds for the rescaled sequence in the endpoint regularity argument.

theorem ESS.blowupEnergyCutoff_gradient_bound_of_lp (R : ℝ) (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ), 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 → ℝ} (M : ℝ), CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0 → MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)) 3 (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) → MeasureTheory.MemLp p (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), (8 + 3 * C) * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 + 3 * C * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 3 + 6 * C * |p z| * CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ M → 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq u Du z ≤ M

Uniform L³ velocity and L^(3/2) pressure data make the local-energy bound applicable on a fixed past cylinder.