Blowup Pressure Decay #
Pressure bounds and convergence estimates for the rescaled sequence.
theorem
ESS.blowupHarmonicRemainder_mass_le
(f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(H : ℝ → ENNReal)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r S : ℝ)
(hr : 0 < r)
(hS : 0 < S)
(hball : CKN.Foundation.Parabolic.vec3Ball x₀ (r * S) ⊆ CKN.euclideanBall 0 (3 / 4))
(hf :
MeasureTheory.AEStronglyMeasurable f
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (r * S))))
(hbound :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - (r * S) ^ 2) t₀), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4)), ENNReal.ofReal |f (x, t)| ≤ H t)
:
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder 0 0 S, ENNReal.ofReal |parabolicRescalePressure x₀ t₀ r f z| ^ (3 / 2) ≤ ENNReal.ofReal (r * S ^ 3) * ENNReal.ofReal (Real.pi * 4 / 3) * ∫⁻ (t : ℝ), H t ^ (3 / 2)
The rescaled pressure has order-r critical mass on a fixed cylinder
when its unscaled slices have an integrable spatial supremum bound.
theorem
ESS.blowupHarmonicRemainder_mass_tendsto_zero
(f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(H : ℝ → ENNReal)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ S : ℝ)
(hS : 0 < S)
(r : ℕ → ℝ)
(hr : ∀ (k : ℕ), 0 < r k)
(hr0 : Filter.Tendsto r Filter.atTop (nhds 0))
(hH : ∫⁻ (t : ℝ), H t ^ (3 / 2) < ⊤)
(hball : ∀ᶠ (k : ℕ) in Filter.atTop, CKN.Foundation.Parabolic.vec3Ball x₀ (r k * S) ⊆ CKN.euclideanBall 0 (3 / 4))
(hf :
∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.AEStronglyMeasurable f
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ (r k * S))))
(hbound :
∀ᶠ (k : ℕ) in Filter.atTop, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - (r k * S) ^ 2) t₀), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4)), ENNReal.ofReal |f (x, t)| ≤ H t)
:
Filter.Tendsto
(fun (k : ℕ) =>
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder 0 0 S, ENNReal.ofReal |parabolicRescalePressure x₀ t₀ (r k) f z| ^ (3 / 2))
Filter.atTop (nhds 0)
The rescaled remainder vanishes in critical mass on each fixed cylinder when its source slices have a finite time-integrated supremum bound.
theorem
ESS.blowupRescaledPressure_aestronglyMeasurable
(f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r : ℝ)
(hr : 0 < r)
:
Positive parabolic rescaling preserves almost-everywhere strong measurability of a whole-space scalar pressure.