Blowup Energy Norm Transfer

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

theorem ESS.blowupFields_eventually_energy_norms (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hvel : ∃ Bᵤ < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupVelocity x₀ t₀ (r k) u z)) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ Bᵤ) (hpress : ∃ Bₚ < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (blowupPressure x₀ t₀ (r k) p) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ Bₚ) : ∃ (Bᵤ : ENNReal) (Bₚ : ENNReal), Bᵤ < ⊤ ∧ Bₚ < ⊤ ∧ ∀ᶠ (k : ℕ) in Filter.atTop, (MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ (r k) u z)) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ (r k) u z)) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ Bᵤ) ∧ MeasureTheory.MemLp (parabolicRescalePressure x₀ t₀ (r k) p) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ∧ MeasureTheory.eLpNorm (parabolicRescalePressure x₀ t₀ (r k) p) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)) ≤ Bₚ

Local bounds for the zero-extended fields transfer to the ordinary rescaled fields entering the suitable local energy inequality.