Blowup Pressure Meas Source

Pressure bounds and convergence estimates for the rescaled sequence.

theorem ESS.blowupPressureExtension_aestronglyMeasurable_of_split (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₁ : MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2) - p₁ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) : MeasureTheory.AEStronglyMeasurable (goodPointDomain.indicator p) MeasureTheory.volume

The fixed pressure split makes the zero extension of the source pressure measurable on the whole spacetime domain.

theorem ESS.blowupPressure_aestronglyMeasurable_of_split (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₁ : MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2) - p₁ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) : MeasureTheory.AEStronglyMeasurable (blowupPressure x₀ t₀ r p) MeasureTheory.volume

The rescaled zero-extended pressure is measurable at every positive scale.