Blowup Riesz Near

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_rieszPressureSpaceTime_tendsto_of_tensor (F : ℕ → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (k : ℕ) (i j : Fin 3), MeasureTheory.MemLp (F k i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hconv : ∀ (i j : Fin 3), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => F k i j z - G i j z) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_tendsto_of_tensor._proof_1 (F k) ⋯ z - CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_tendsto_of_tensor._proof_1 G hG z) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) Filter.atTop (nhds 0)

Strong L^(3/2) convergence of all nine tensor components gives strong convergence of their whole-space pressures. This is the near-field step of prop:blowup-limit after restricting the tensors to a fixed ball.

theorem ESS.blowup_rieszPressureSpaceTime_near_tendsto (C : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (hC : MeasurableSet C) (v : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict C)) (hv : ∀ (k : ℕ), MeasureTheory.MemLp (v k) 3 (MeasureTheory.volume.restrict C)) (hconv : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v k z - u z) 3 (MeasureTheory.volume.restrict C)) Filter.atTop (nhds 0)) (hbound : ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (v k) 3 (MeasureTheory.volume.restrict C) ≤ B) : have F := fun (k : ℕ) (i j : Fin 3) => C.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v k z i * v k z j; have G := fun (i j : Fin 3) => C.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i * u z j; ∃ (hF : ∀ (k : ℕ) (i j : Fin 3), MeasureTheory.MemLp (F k i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_tendsto_of_tensor._proof_1 (F k) ⋯ z - CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_tendsto_of_tensor._proof_1 G hG z) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) Filter.atTop (nhds 0)

Strong local L³ velocity convergence controls the pressure of the tensor truncated to a fixed measurable space-time region.