Blowup Ten Thirds Top

Space-time integrability of the rescaled velocity at exponent 10/3.

theorem ESS.blowup_eLpNorm_bound_to_time_zero (A : Set CKN.Foundation.Parabolic.Vec3) (hA : MeasurableSet A) (a : ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (p : NNReal) (hp : p ≠ 0) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a 0))) (K : ENNReal) (hK : K < ⊤) (hbound : ∀ b < 0, MeasureTheory.MemLp f (↑p) (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a b)) ∧ MeasureTheory.eLpNorm f (↑p) (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a b)) ^ ↑p ≤ K) : MeasureTheory.MemLp f (↑p) (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm f (↑p) (MeasureTheory.volume.restrict (A ×ˢ Set.Ioo a 0)) ^ ↑p ≤ K

A uniform Lᵖ bound on finite past cylinders extends to the open terminal-time cylinder.