Blowup Energy Majorant

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

theorem ESS.blowupEnergyMajorant_integrable {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (U p : α → ℝ) (hU : MeasureTheory.MemLp U 3 μ) (hp : MeasureTheory.MemLp p (3 / 2) μ) (C : ℝ) : MeasureTheory.Integrable (fun (z : α) => (8 + 3 * C) * U z ^ 2 + 3 * C * U z ^ 3 + 6 * C * |p z| * U z) μ

The three terms in the cutoff energy bound are integrable under the velocity L³ and pressure L^(3/2) assumptions on a finite region.

theorem ESS.blowupEnergyOuter_finiteMeasure (R a : ℝ) (hR : 0 < R) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0)))

A bounded spatial ball and a finite past time interval have finite space-time volume.

theorem ESS.blowupEnergyMajorant_le_cubic_pressure (C U p : ℝ) (hC : 0 ≤ C) (hU : 0 ≤ U) : (8 + 3 * C) * U ^ 2 + 3 * C * U ^ 3 + 6 * C * |p| * U ≤ 8 + 3 * C + (8 + 8 * C) * U ^ 3 + 4 * C * |p| ^ (3 / 2)

The energy majorant is bounded by a constant, cubic velocity mass, and pressure 3/2 mass.