Blowup Riesz Far Tensor

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_velocity_tensor_memLp (v : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hv : MeasureTheory.MemLp v 3 MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z i * v z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

A whole-space space-time L³ velocity has an L^(3/2) quadratic tensor, the input to the canonical Riesz pressure.

theorem ESS.blowup_exterior_velocity_tensor_memLp (v : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (L a b : ℝ) (hv : MeasureTheory.MemLp v 3 (MeasureTheory.volume.restrict ((CKN.euclideanBall 0 L)ᶜ ×ˢ Set.Ioo a b))) (i j : Fin 3) : MeasureTheory.MemLp (((CKN.euclideanBall 0 L)ᶜ ×ˢ Set.Ioo a b).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z i * v z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

The tensor of an L³ velocity, truncated to an exterior spatial region and a time interval, belongs to whole-space space-time L^(3/2).

theorem ESS.blowup_exterior_velocity_tensor_slice_bound (v : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (L a b : ℝ) (N : ENNReal) (hN : N < ⊤) (hv : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => v (x, t)) 3 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v (x, t)) 3 MeasureTheory.volume ≤ N) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i j : Fin 3), MeasureTheory.lpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ((CKN.euclideanBall 0 L)ᶜ ×ˢ Set.Ioo a b).indicator (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z i * v z j) (x, t)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ N.toReal ^ 2

The exterior tensor slice has L^(3/2) norm at most the square of the whole-space L³ velocity-slice bound.