Blowup Riesz Far Uniform

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_rieszPressure_exterior_uniform_mass_small (F : ℕ → ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (n k : ℕ) (i j : Fin 3), MeasureTheory.MemLp (F n k i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (R a b M : ℝ) (hR : 0 < R) (hab : a < b) (hzero : ∀ (n k : ℕ) (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.1 ∈ CKN.euclideanBall 0 (↑n + 1) → F n k i j z = 0) (hinput : ∀ (n k : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i j : Fin 3), MeasureTheory.lpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F n k i j (x, t)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ M) (ε : ENNReal) : 0 < ε → ∃ (n : ℕ), ∀ (k : ℕ), ∫⁻ (z : CKN.Vec 3 × ℝ), ENNReal.ofReal |CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_exterior_uniform_mass_small._proof_1 (F n k) ⋯ z| ^ (3 / 2) ∂(MeasureTheory.volume.restrict (CKN.euclideanBall 0 R)).prod (MeasureTheory.volume.restrict (Set.Ioo a b)) ≤ ε

The far-field pressure estimate is uniform over a sequence of tensors with the same global slice bound.