Blowup Riesz Far Bound

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_rieszPressure_exterior_mass_bound : ∃ C < ⊤, ∀ (F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (L R a b M : ℝ), 0 < L → 0 < R → R ≤ 3 * L / 4 → a < b → (∀ (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ), z.1 ∈ CKN.euclideanBall 0 L → F i j z = 0) → (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i j : Fin 3), MeasureTheory.lpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F i j (x, t)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ M) → ∫⁻ (z : CKN.Vec 3 × ℝ), ENNReal.ofReal |CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressure_exterior_mass_bound._proof_1 F hF z| ^ (3 / 2) ∂(MeasureTheory.volume.restrict (CKN.euclideanBall 0 R)).prod (MeasureTheory.volume.restrict (Set.Ioo a b)) ≤ MeasureTheory.volume (Set.Ioo a b) * (C * ENNReal.ofReal (L ^ 2)⁻¹ * ENNReal.ofReal (CKN.Leray.rieszPressureOperatorBound (3 / 2) blowup_rieszPressure_exterior_mass_bound._proof_1 * (9 * M)) * MeasureTheory.volume (CKN.euclideanBall 0 R) ^ (2 / 3)) ^ (3 / 2)

Exterior support and a uniform tensor-slice bound give the quantitative far-field pressure estimate on a bounded past cylinder.