Blowup Time AE

Almost-everywhere time-slice bounds used in endpoint compactness.

theorem ESS.blowupPastInterval_subset_source (t₀ r a : ℝ) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : 0 < r) (htime : r ^ 2 * -a < 3 / 4) : Set.Ioo a 0 ⊆ CKN.rescaledTime r t₀ (Set.Ioo (-1) 0)

A fixed past time interval remains in the original time interval after a sufficiently small positive rescaling.

theorem ESS.blowupTimeExtendedPressure_aestronglyMeasurable (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₁ : MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) : MeasureTheory.AEStronglyMeasurable (blowupTimeExtendedPressure p₁) MeasureTheory.volume

Zero extension in time preserves joint strong measurability of a whole-space pressure.

theorem ESS.blowupRieszPressure_aestronglyMeasurable (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₁ : MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) : MeasureTheory.AEStronglyMeasurable (blowupRieszPressure x₀ t₀ r p₁) MeasureTheory.volume

The rescaled whole-space pressure remains jointly strongly measurable.

theorem ESS.blowup_ae_time_pullback (r t₀ : ℝ) (hr : 0 < r) (I : Set ℝ) (hI : MeasurableSet I) (P : ℝ → Prop) (hP : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, P s) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (CKN.rescaledTime r t₀ I), P (CKN.scalingTime r t₀ t)

An almost everywhere source-time property pulls back through a positive parabolic time rescaling.

theorem ESS.blowup_ae_time_pullback_on (r t₀ : ℝ) (hr : 0 < r) (I J : Set ℝ) (hI : MeasurableSet I) (hJ : J ⊆ CKN.rescaledTime r t₀ I) (P : ℝ → Prop) (hP : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, P s) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, P (CKN.scalingTime r t₀ t)

The pulled-back property also holds on every smaller rescaled time interval.

theorem ESS.blowupRieszPressure_slice_bound_ae (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (J : Set ℝ) (hJmeas : MeasurableSet J) (hJ : J ⊆ CKN.rescaledTime r t₀ (Set.Ioo (-1) 0)) (M : ENNReal) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) (3 / 2) MeasureTheory.volume ≤ M) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => blowupRieszPressure x₀ t₀ r p₁ (x, t)) (3 / 2) MeasureTheory.volume ≤ M

A source-time uniform whole-space pressure bound persists on a rescaled past time interval contained in the source interval.

theorem ESS.blowupRieszPressure_time_threeHalves_bound (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (J : Set ℝ) (hJmeas : MeasurableSet J) (hJ : J ⊆ CKN.rescaledTime r t₀ (Set.Ioo (-1) 0)) (M : ENNReal) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) (3 / 2) MeasureTheory.volume ≤ M) : ∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => blowupRieszPressure x₀ t₀ r p₁ (x, t)) (3 / 2) MeasureTheory.volume ^ (3 / 2) ≤ MeasureTheory.volume J * M ^ (3 / 2)

A uniform source-time pressure bound controls the time-integrated rescaled L^(3/2) norm.

theorem ESS.blowupRieszPressure_spaceTime_mass_bound (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₁ : MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0))) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (J : Set ℝ) (hJmeas : MeasurableSet J) (hJ : J ⊆ CKN.rescaledTime r t₀ (Set.Ioo (-1) 0)) (M : ENNReal) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) (3 / 2) MeasureTheory.volume ≤ M) : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal |blowupRieszPressure x₀ t₀ r p₁ z| ^ (3 / 2) ∂(MeasureTheory.volume.restrict Set.univ).prod (MeasureTheory.volume.restrict J) ≤ MeasureTheory.volume J * M ^ (3 / 2)

The rescaled whole-space pressure has a uniform space-time L^(3/2) mass bound on a past time interval.