Blowup Riesz Far Velocity #
Pressure reconstruction and convergence bounds for the rescaled sequence.
theorem
ESS.blowup_riesz_far_velocity_uniform_mass_small
(v : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3)
(R a b : ℝ)
(hR : 0 < R)
(hab : a < b)
(N : ENNReal)
(hN : N < ⊤)
(hv :
∀ (n : ℝ) (k : ℕ),
MeasureTheory.MemLp (v k) 3 (MeasureTheory.volume.restrict ((CKN.euclideanBall 0 (n + 1))ᶜ ×ˢ Set.Ioo a b)))
(hslice :
∀ (k : ℕ),
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v k (x, t)) 3 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v k (x, t)) 3 MeasureTheory.volume ≤ N)
:
have F := fun (n k : ℕ) (i j : Fin 3) =>
((CKN.euclideanBall 0 (↑n + 1))ᶜ ×ˢ Set.Ioo a b).indicator fun (z : CKN.Vec 3 × ℝ) => v k z i * v k z j;
∃ (hF : ∀ (n k : ℕ) (i j : Fin 3), MeasureTheory.MemLp (F n k i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume),
∀ (ε : ENNReal),
0 < ε →
∃ (n : ℕ),
∀ (k : ℕ),
∫⁻ (z : CKN.Vec 3 × ℝ), ENNReal.ofReal
|CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_riesz_far_velocity_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)) ≤ ε
A sequence with uniformly bounded whole-space L³ velocity slices has
uniformly small exterior Riesz pressure on each fixed inner cylinder.