Continuity of space-time Riesz pressure

Strong convergence of tensor components in space-time L^r passes through all nine double Riesz transforms and their measurable pressure representative.

theorem CKN.Leray.rieszPressureSpaceTime_eLpNorm_tendsto (r : ℝ) (hr : 1 < r) (F : ℕ → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (F n i j) (ENNReal.ofReal r) MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal r) MeasureTheory.volume) (hconv : ∀ (i j : Fin 3), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n i j - G i j) (ENNReal.ofReal r) MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (rieszPressureSpaceTime r hr (F n) ⋯ - rieszPressureSpaceTime r hr G hG) (ENNReal.ofReal r) MeasureTheory.volume) Filter.atTop (nhds 0)

Strong space-time L^r convergence of every tensor component implies strong L^r convergence of the canonical Riesz pressure representative.

theorem CKN.Leray.pressureLimit_holder_three_three_threeHalves : ENNReal.HolderTriple 3 3 (ENNReal.ofReal (3 / 2))

theorem CKN.Leray.rieszPressureSpaceTime_product_memLp_of_slab {s : Set (Foundation.Parabolic.Vec3 × ℝ)} (hs : MeasurableSet s) (v w : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i) 3 (MeasureTheory.volume.restrict s)) (hw : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => w z j) 3 (MeasureTheory.volume.restrict s)) (i j : Fin 3) : MeasureTheory.MemLp (s.indicator fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i * w z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

Products of two spatial vector fields in L³ have tensor components in L^(3/2), including after extension by zero from a measurable space-time set.

theorem CKN.Leray.rieszPressureSpaceTime_product_tendsto_of_Lthree {s : Set (Foundation.Parabolic.Vec3 × ℝ)} (hs : MeasurableSet s) (vseq wseq : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (v w : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hvseq : ∀ (n : ℕ), MeasureTheory.MemLp (vseq n) 3 (MeasureTheory.volume.restrict s)) (hwseq : ∀ (n : ℕ), MeasureTheory.MemLp (wseq n) 3 (MeasureTheory.volume.restrict s)) (hv : MeasureTheory.MemLp v 3 (MeasureTheory.volume.restrict s)) (hw : MeasureTheory.MemLp w 3 (MeasureTheory.volume.restrict s)) (hconvV : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (vseq n - v) 3 (MeasureTheory.volume.restrict s)) Filter.atTop (nhds 0)) (hconvW : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (wseq n - w) 3 (MeasureTheory.volume.restrict s)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (rieszPressureSpaceTime (3 / 2) rieszPressureSpaceTime_product_tendsto_of_Lthree._proof_1 (fun (i j : Fin 3) => s.indicator fun (z : Foundation.Parabolic.Vec3 × ℝ) => vseq n z i * wseq n z j) ⋯ - rieszPressureSpaceTime (3 / 2) rieszPressureSpaceTime_product_tendsto_of_Lthree._proof_1 (fun (i j : Fin 3) => s.indicator fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i * w z j) ⋯) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict s)) Filter.atTop (nhds 0)

The pressure of a tensor supported on a fixed measurable space-time set is continuous under strong L³ convergence of its two velocity factors.