Blowup Energy Pressure Integral

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

theorem ESS.blowup_energyPressure_integral_bound (R a : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (Cg Cp : ℝ) (hgInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq v Dv z) (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0) MeasureTheory.volume) (hgBound : 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0, CKN.spatialGradientSq v Dv z ≤ Cg) (hpMem : MeasureTheory.MemLp p (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) (hpBound : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0, |p z| ^ (3 / 2) ≤ Cp) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => |p z| ^ (3 / 2) + CKN.spatialGradientSq v Dv z) (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0) MeasureTheory.volume ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0, |p z| ^ (3 / 2) + CKN.spatialGradientSq v Dv z ≤ Cp + Cg

Pressure mass and twice the Dirichlet energy bound the integral of their sum on the same open past cylinder.