Blowup Energy Mass Bound

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

theorem ESS.blowupEnergyCutoff_gradient_bound_of_masses (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 → ℝ}, 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))) → 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq u Du z ≤ ((8 + 3 * C) * (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))).real Set.univ + (8 + 8 * C) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 3) + 4 * C * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0), |p z| ^ (3 / 2)

On a fixed past cylinder, the local gradient energy is bounded by the volume, the cubic velocity mass, and the pressure 3/2 mass.